ledger_reconstruction
plain-language theorem explainer
Closed observable frameworks equipped with a symmetric unit-normalized J-cost and finite-description regularity reconstruct a zero-parameter comparison ledger whose carrier is the framework state space. Researchers closing the Recognition Science axiom system cite this to absorb R1, R2, R5, R6 as definitions. The definition converts the split regularity into a legacy certificate and assembles the ledger fields by direct substitution from the framework and the supplied J.
Claim. Given a closed observable framework $F$ with state space $S$, transition map, positive ratio function, nontriviality, countability, no continuous moduli, and conserved charge, together with a function $J : (0,∞) → ℝ$ satisfying $J(x) = J(x^{-1})$, $J(1) = 0$, finite-description regularity (continuity, strict convexity, calibration), and the composition-sufficiency identity, the construction yields a zero-parameter comparison ledger with carrier $S$, cost function $J$, and the conserved charge of $F$.
background
ClosedObservableFramework is a structure with type $S$ of states, transition $T$, positive ratio $r$, nontriviality witness, countability of $S$, absence of continuous moduli, and conserved charge. FiniteDescriptionRegularity splits the regularity requirement into continuity from finite description, strict convexity from closure, and calibration from unit choice; its toRegularityCert folds these back into the legacy bundle. ZeroParameterComparisonLedger packages a nonempty countable carrier, admissible cost, and conserved charge.
proof idea
The definition first applies toRegularityCert to FiniteDescriptionRegularity to obtain the legacy continuity, convexity, and calibration fields. It then builds the ZeroParameterComparisonLedger record by setting Carrier to $F.S$, populating the cost record with the supplied $J$ and its symmetry, unit, convexity, continuity, and calibration properties, the charge record with $F.charge$, and the remaining fields (nonempty, countable, no free knobs, cost sufficient, composition) directly from $F$ and the hypotheses.
why it matters
This definition completes the reconstruction step in Gap 1 of the axiom-closure plan, absorbing R1, R2, R5, R6 as structure fields rather than axioms and isolating the remaining Regularity Axiom to three explicit finite-description obligations. It bridges ClosedObservableFramework to ZeroParameterComparisonLedger in the foundation module, supporting the transition to the unconditional theorem and the phi-ladder structure of the Recognition Science forcing chain (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.