Foundation Recognition Ledger Floor

The defect ledger

A defect ledger is a bookkeeping table. It records, for each kind of flaw in a system, how many times that flaw has appeared. The table is finite: only finitely many flaws have occurred so far. The cost of a ledger is the weighted sum of its entries: each flaw of kind i has a positive weight w(i), and the cost is the sum over all flaws of (number of occurrences) times (weight). This is the free commutative monoid on the set of flaw kinds, written DefectLedger I.

The ledger answers two problems that an earlier two-state model left open. First, the earlier model had to impose an external rule saying which flaws are independent. The ledger needs no such rule: the cost of two ledgers added together is always the sum of their costs, unconditionally. Second, the earlier model could not represent two independent copies of the same flaw; it treated them as one. The ledger represents multiplicity directly: two copies of the same flaw cost exactly twice its weight, proved as two_independent_same_defects.

In the ledger, two ledgers are observably the same when they have the same cost. This equivalence is not imposed from outside; it is the kernel of the cost function itself, proved as observableSetoid and ledgerCost_constant_on_classes. The floor, the fact that some ledgers are observably different, is non-vacuous exactly when at least one weight is positive, proved as observable_floor_iff_pos_weight. If all weights are zero, every ledger has cost zero and the floor collapses.

In Recognition Science, this ledger is the foundation: it is the free additive cost floor. The earlier two-state Boolean floor is the special case where each flaw appears at most once and all weights are one, proved as boolean_floor_is_truncation. The ledger assembles into the framework's standard cost function abstraction with the universal independence relation, proved as ledgerCostFunction. The module closes the two genuine mathematical gaps identified in the May 2026 audit: the kernel gap and the cokernel gap. It does so with 0 sorry and 0 new axioms.

The consequence is that the framework's cost structure now has a clean, unconditional base. Additivity is not a concession to a restricted independence relation; it is a theorem about the ledger. Multiplicity is not dodged; it is represented. The floor is not assumed; it is derived from the positivity of weights. This is the ground on which the framework's further structure, the forcing chain and its constants, can stand.

/-- **Unconditional additivity.** The free ledger needs no restriction of the
independence relation: the cost of a sum is always the sum of the costs. -/
theorem ledgerCost_add (w : I → ℝ) (Γ Δ : DefectLedger I) :
    ledgerCost w (Γ + Δ) = ledgerCost w Γ + ledgerCost w Δ := by
  unfold ledgerCost
  refine Finsupp.sum_add_index' ?_ ?_
  · intro i; simp
  · intro i a b; push_cast; ring

/-- **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

/-- **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 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 ledger does not itself derive the golden ratio or any physical constant; it only establishes the additive cost floor. The ledger does not impose a restricted independence relation; additivity is unconditional, not a special case. The module does not prove the full forcing chain; it closes two specific gaps identified in an audit.

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: