ledger_recognition_work_constraint
plain-language theorem explainer
For any strictly positive weight on primitive distinctions, the free defect ledger admits a recognition-work constraint certificate (dichotomy, independent additivity, empty cost zero). Foundation authors closing the T0/T-1 kernel and cokernel audit gaps cite this to place the ledger inside CostFromDistinction. The proof is a one-line wrapper applying the general recognition-work constraint theorem to the ledger cost function.
Claim. Let $I$ be a type of primitive distinctions and let $w : I \to \mathbb{R}$ satisfy $w(i) > 0$ for all $i$. Then the free defect ledger (finitely supported multiplicities $I \to_0 \mathbb{N}$) carries a nonempty recognition-work constraint certificate: there is a cost function on that ledger obeying dichotomy and independent additivity, with empty configuration cost zero and positive cost exactly on inconsistent configurations.
background
The module answers two genuine gaps from the T-1/T0 audit (the Anil critique): the kernel gap (observable equivalence should be the kernel of the cost, not an external setoid) and the cokernel gap (independent defects must accumulate additively with multiplicity). Both are handled by one carrier, the free commutative monoid on primitive distinctions $I$, written as finitely supported maps $I \to_0 \mathbb{N}$.
A cost function on a configuration space is required to satisfy dichotomy (cost zero iff consistent) and independent additivity (cost adds over joins of configurations that share no predicates). The recognition-work constraint certificate packages such a cost with its immediate consequences: empty cost zero, positivity exactly on inconsistent states, and calibrated additivity on independent extensions.
Upstream, any cost function yields a nonempty certificate via the recognition-work constraint theorem. In this module the ledger cost under a strictly positive weight is assembled into a genuine cost function with universal independence, so the general theorem applies directly.
proof idea
One-line term wrapper. Instantiate the general recognition-work constraint theorem at the ledger cost function built from the given strictly positive weight $w$. That cost function already supplies non-negativity, dichotomy, and independent additivity on the free ledger; the theorem only packages those data into a nonempty certificate.
why it matters
This is the headline that the free ledger sits inside the CostFromDistinction abstraction with multiplicity represented and independence universal, exactly as the module doc requires. It closes the cokernel gap (two independent copies of the same defect cost twice the weight) and the kernel gap (observable equivalence is the cost kernel) without restricted independence relations that previously dodged $1=2$.
In the broader Recognition chain it supplies the additive floor that the two-state Boolean T0 floor truncates under unit weight. No downstream consumers are wired yet in the graph; the declaration is the terminal assembly step of RecognitionLedgerFloor itself. It does not touch J-uniqueness (T5), phi forcing (T6), or the eight-tick octave (T7); those sit higher in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.