Foundation Recognition Ledger Floor Ledger Recognition Work Constraint

The work constraint

A ledger, in this framework, is a discrete record of events, each event being a primitive distinction with a multiplicity. The declaration ledger_recognition_work_constraint is a theorem in the framework's machine-checked library of formal theorems. It states that for any ledger whose weights are all strictly positive, the cost function derived from that ledger satisfies a recognition work constraint. This constraint is a certificate: it certifies that the cost function meets a required structural condition, and the theorem proves this certificate exists for every such ledger.

The theorem is not an isolated claim. It is built from a chain of results about the ledger's cost. The cost of a ledger entry is the sum of its multiplicities times their weights. Two independent copies of the same defect genuinely cost twice as much as one copy, a fact the framework proves as two_independent_same_defects. The cost of an empty ledger is zero, and the cost of a nonempty ledger is strictly positive when all weights are positive. The recognition work constraint theorem packages these facts into a single certificate, which the framework's CostFunction abstraction requires for any valid cost function.

What the theorem does not claim is just as important. It does not assert that any particular ledger is the one reality uses. It does not fix the weights, nor does it say which primitive distinctions exist. It only says: given any ledger with positive weights, the recognition work constraint holds. The theorem also does not claim that the constraint is unique or that it is the only condition a cost function must satisfy. It is one structural guarantee among others, derived from the ledger's definition, not an empirical statement about the world.

The practical consequence is that the framework's foundational floor, the two-state Boolean ledger, is a special case of this more general construction. The Boolean floor is the truncation of the full ledger to multiplicities of zero or one under unit weight. The recognition work constraint theorem applies to that floor as well, since it applies to every ledger with positive weights. This means the framework's basic recognition ledger is not a hand-picked exception; it is one instance of a general structural fact.

/-- The free ledger satisfies the recognition-work constraint theorem of
`CostFromDistinction`, with multiplicity represented and independence universal. -/
theorem ledger_recognition_work_constraint (w : I → ℝ) (hw : ∀ i, 0 < w i) :
    Nonempty (CostFunction.RecognitionWorkConstraintCert (DefectLedger I)) :=
  CostFunction.recognition_work_constraint_theorem (ledgerCostFunction w hw)

/-- The free ledger satisfies the recognition-work constraint theorem of
`CostFromDistinction`, with multiplicity represented and independence universal. -/
theorem ledger_recognition_work_constraint (w : I → ℝ) (hw : ∀ i, 0 < w i) :
    Nonempty (CostFunction.RecognitionWorkConstraintCert (DefectLedger I)) :=
  CostFunction.recognition_work_constraint_theorem (ledgerCostFunction w hw)

/-- **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 identify which ledger reality uses. The theorem does not fix the weights or the set of primitive distinctions. The theorem does not assert that the recognition work constraint is the only condition a cost function must satisfy.

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: