Reference · Non-negative rationals

rainbow.math.rational.nnrat.diagonal-spike

Non-negative rationals src/rainbow/math/rational/nnrat/diagonal_spike.clj3 definitions, 10 theorems

Canonical exact-rational diagonal spikes over duplicate-free finite carriers. A Boolean equality decision is supplied together with proofs that `true` reflects and is complete for propositional equality. The executable spike puts a row mass at its selected state and zero elsewhere. Duplicate freedom and membership of the selected state imply that its finite sum is exactly the supplied mass. A certified exhaustive carrier packages equality correctness with coverage of every ambient state, so downstream kernels need one coherent finite-state certificate rather than two unrelated premises. Native, kernel-checked, and axiom-free on D63.

Depends onmath.rational.nnrat.list-sum

finite/certified-equality-decision

DefinitionSource, line 153

finite/certified-equality-decision.{u} :
  (S : Type u) (decision : S → S → data/Bool)
  → Prop

finite/certified-exhaustive-carrier

DefinitionSource, line 171

finite/certified-exhaustive-carrier.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool)
  → Prop

Finset = finset-data/Finset

finite/nnrat-diagonal-spike

DefinitionSource, line 233

finite/nnrat-diagonal-spike.{u} :
  (S : Type u) (decision : S → S → data/Bool) (mass : S → ℚ≥0) (x₁ x₂ : S)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

finite/certified-equality-of-exhaustive-carrier

TheoremFor all inputsNo axiomsSource, line 191

finite/certified-equality-of-exhaustive-carrier.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool)
  (exhaustive : finite/certified-exhaustive-carrier S states decision)
  → finite/certified-equality-decision S decision

Finset = finset-data/Finset

finite/coverage-of-exhaustive-carrier

TheoremFor all inputsNo axiomsSource, line 212

finite/coverage-of-exhaustive-carrier.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool)
  (exhaustive : finite/certified-exhaustive-carrier S states decision) (state : S)
  → list/membership S (finset-data/enumeration S states) state

Finset = finset-data/Finset

finite/nnrat-diagonal-spike-zero-of-different

TheoremFor all inputsNo axiomsSource, line 253

finite/nnrat-diagonal-spike-zero-of-different.{u} :
  (S : Type u) (decision : S → S → data/Bool) (mass : S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (selected candidate : S)
  (different : selected = candidate → proposition/falsity)
  → finite/nnrat-diagonal-spike S decision mass selected candidate = 0

0 = nnrat/zero= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational

finite/equality-decidable-of-certified-decision

TheoremFor all inputsNo axiomsSource, line 296

finite/equality-decidable-of-certified-decision.{u} :
  (S : Type u) (decision : S → S → data/Bool)
  (certified : finite/certified-equality-decision S decision) (left right : S)
  → proposition/disjunction (left = right) (left = right → proposition/falsity)

= = equality/Eq

finite/nnrat-diagonal-spike-mass-of-equal

TheoremFor all inputsNo axiomsSource, line 344

finite/nnrat-diagonal-spike-mass-of-equal.{u} :
  (S : Type u) (decision : S → S → data/Bool) (mass : S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (selected candidate : S)
  (same : selected = candidate)
  → finite/nnrat-diagonal-spike S decision mass selected candidate = mass selected

= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational

finite/nnrat-diagonal-unit-spike-multiply

TheoremFor all inputsNo axiomsSource, line 387

finite/nnrat-diagonal-unit-spike-multiply.{u} :
  (S : Type u) (decision : S → S → data/Bool) (mass : S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (selected candidate : S)
  → finite/nnrat-diagonal-spike S decision (fun x₄ => 1) selected candidate · mass candidate = finite/nnrat-diagonal-spike S decision mass selected candidate

1 = nnrat/one= = nnrat/equivalent: equality of rational values· = nnrat/multiplyℚ≥0 = nnrat/NonnegativeRational

finite/nnrat-map-sum-diagonal-spike-zero-of-not-member

TheoremFor all inputsNo axiomsSource, line 460

finite/nnrat-map-sum-diagonal-spike-zero-of-not-member.{u} :
  (S : Type u) (decision : S → S → data/Bool) (mass : S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (items : List S)
  (selected : S) (not-member : list/membership S items selected → proposition/falsity)
  → nnrat/map-sum S (fun candidate => spike candidate) items = 0
  where spike := finite/nnrat-diagonal-spike S decision mass selected

0 = nnrat/zero= = nnrat/equivalent: equality of rational valuesList = data/Listℚ≥0 = nnrat/NonnegativeRational

finite/nnrat-map-sum-diagonal-spike-of-member-no-duplicates

TheoremFor all inputsNo axiomsSource, line 575

finite/nnrat-map-sum-diagonal-spike-of-member-no-duplicates.{u} :
  (S : Type u) (decision : S → S → data/Bool) (mass : S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (items : List S)
  (selected : S) (distinct : list/no-duplicates S items)
  (member : list/membership S items selected)
  → nnrat/map-sum S (fun candidate => spike candidate) items = mass selected
  where spike := finite/nnrat-diagonal-spike S decision mass selected

= = nnrat/equivalent: equality of rational valuesList = data/Listℚ≥0 = nnrat/NonnegativeRational

finite/nnrat-finset-diagonal-spike-total

TheoremFor all inputsNo axiomsSource, line 721

finite/nnrat-finset-diagonal-spike-total.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (mass : S → ℚ≥0)
  (certified : finite/certified-equality-decision S decision) (selected : S)
  (member : list/membership S (finset-data/enumeration S states) selected)
  → nnrat/map-sum S (fun candidate => spike candidate) (finset-data/enumeration S states) = mass selected
  where spike := finite/nnrat-diagonal-spike S decision mass selected

= = nnrat/equivalent: equality of rational valuesFinset = finset-data/Finsetℚ≥0 = nnrat/NonnegativeRational

finite/nnrat-finset-diagonal-spike-total-of-exhaustive-carrier

TheoremFor all inputsNo axiomsSource, line 757

finite/nnrat-finset-diagonal-spike-total-of-exhaustive-carrier.{u} :
  (S : Type u) (states : Finset S) (decision : S → S → data/Bool) (mass : S → ℚ≥0)
  (exhaustive : finite/certified-exhaustive-carrier S states decision) (selected : S)
  → nnrat/map-sum S (fun candidate => spike candidate) (finset-data/enumeration S states) = mass selected
  where spike := finite/nnrat-diagonal-spike S decision mass selected

= = nnrat/equivalent: equality of rational valuesFinset = finset-data/Finsetℚ≥0 = nnrat/NonnegativeRational