Foundation Recognition Ledger Floor Observable Floor Iff Pos Weight

The non-vacuous floor

A ledger is a discrete record of events, each entry carrying a number. The Recognition Science framework models the cost of maintaining such a record as a sum: the total cost is the number of entries of each kind, multiplied by that kind's weight, added across all kinds. The object in question, DefectLedger, is the free commutative monoid on a type of primitive distinctions: a finitely supported function from distinction types to natural numbers, recording how many times each distinction appears.

The framework proves a theorem about when this cost function has a non-vacuous floor, meaning when there exist two ledgers that are observably different: two records whose costs differ. The theorem, observable_floor_iff_pos_weight, states that such a pair exists if and only if at least one weight is strictly positive. In plain terms: the floor is meaningful exactly when recording some distinction costs something. If every weight is zero, every ledger costs zero, and no two records can be told apart by cost alone. The proof is machine-checked in the framework's library of formal theorems, with no unproved assumptions.

The theorem's force is structural. It derives the observable equivalence from the cost function itself, as its kernel, rather than imposing it from outside. Two ledgers are observably the same precisely when their costs are equal, and the theorem shows this equivalence is non-trivial exactly under the positivity condition. The framework also proves that two independent copies of the same defect cost twice the single copy's cost, so multiplicity is represented additively without any special independence relation. The earlier two-state Boolean floor appears as a truncation of this richer object, retaining only whether a count is zero or nonzero.

What the theorem does not claim is equally sharp. It does not assert that any particular weight is positive; it only states the equivalence. It does not say that the cost function is unique, nor that it is the only possible cost model. It does not claim that the ledger's cost function is the J-cost function derived elsewhere in the framework. The theorem is about the existence of a non-vacuous floor under a given weight assignment, not about which weight assignment is correct.

/-- **Non-vacuity of the observable floor.** The cost kernel is proper (there
exist observably distinct ledgers) exactly when some distinction carries
positive weight. With a constant-zero weight the kernel is everything, which is
the correct RS reading of the indiscrete gauge counterexample. -/
theorem observable_floor_iff_pos_weight (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) :
    (∃ Γ Δ : DefectLedger I, ¬ ObservablySame w Γ Δ) ↔ (∃ i, 0 < w i) := by
  constructor
  · rintro ⟨Γ, Δ, hne⟩
    by_contra hno
    push_neg at hno
    have hzero : ∀ i, w i = 0 := fun i => le_antisymm (hno i) (hw i)
    apply hne
    show ledgerCost w Γ = ledgerCost w Δ
    have hall : ∀ Θ : DefectLedger I, ledgerCost w Θ = 0 := by
      intro Θ
      unfold ledgerCost
      refine Finset.sum_eq_zero ?_
      intro i _
      simp [hzero i]
    rw [hall Γ, hall Δ]
  · rintro ⟨i, hi⟩
    refine ⟨Finsupp.single i 1, 0, ?_⟩
    intro hsame
    have h : ledgerCost w (Finsupp.single i 1) = ledgerCost w (0 : DefectLedger I) := hsame
    rw [ledgerCost_single, ledgerCost_zero] at h
    push_cast at h
    simp only [one_mul] at h
    exact hi.ne' h

/-- **The cokernel fix.** Two independent copies of the same defect cost `2 w i`,
not `w i`. Multiplicity is genuinely represented, so the free ledger needs no
restriction of independence to avoid `1 = 2`: on this carrier, `1 + 1 = 2`. -/
theorem two_independent_same_defects (w : I → ℝ) (i : I) :
    ledgerCost w (Finsupp.single i 1 + Finsupp.single i 1) = 2 * w i := by
  rw [ledgerCost_add, ledgerCost_single]
  push_cast
  ring

/-- The Boolean two-state floor of T0 is the unit-weight truncation of the
ledger: cost equals multiplicity, and the Boolean floor is the clamp to
`{0, 1}`. -/
theorem boolean_floor_is_truncation (i : I) (n : ℕ) :
    ledgerCost (fun _ => (1 : ℝ)) (Finsupp.single i n) = (n : ℝ) := by
  rw [ledgerCost_single]; ring

What this page does not claim

The theorem does not assert that any particular weight is positive, only the equivalence. The theorem does not claim the ledger cost function is the unique cost model or the J-cost function. The theorem does not establish that the ledger's observable equivalence matches any physical measurement.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/RecognitionLedgerFloor.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: