ledger_reconstruction
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.
claimGiven 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 in Recognition Science
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).
scope and limits
- Does not derive symmetry, normalization, or regularity of $J$ from first principles.
- Does not guarantee uniqueness of the induced ledger.
- Does not apply to frameworks admitting continuous moduli.
- Does not compute explicit values on the phi-ladder or coupling constants.
formal statement (Lean)
118noncomputable def ledger_reconstruction
119 (F : ClosedObservableFramework)
120 (J : ℝ → ℝ)
121 (hJ_sym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
122 (hJ_unit : J 1 = 0)
123 (hJ_reg : FiniteDescriptionRegularity J)
124 (hJ_suff : ∀ (x₁ x₂ y : ℝ), 0 < x₁ → 0 < x₂ →
125 J x₁ = J x₂ → 0 < y →
126 J (x₁ * y) + J (x₁ / y) = J (x₂ * y) + J (x₂ / y)) :
127 ZeroParameterComparisonLedger :=
proof body
Definition body.
128 let hJ_legacy := hJ_reg.toRegularityCert
129 let ⟨hJ_cont, hJ_conv, hJ_cal⟩ := hJ_legacy
130 { Carrier := F.S
131 carrier_nonempty := by obtain ⟨s₁, _, _⟩ := F.nontrivial; exact ⟨s₁⟩
132 carrier_countable := F.S_countable
133 cost :=
134 { J := J
135 reciprocal_sym := hJ_sym
136 unit_norm := hJ_unit
137 strict_convex := hJ_conv
138 continuous := hJ_cont
139 calibration := hJ_cal }
140 charge :=
141 { charge := F.charge
142 charge_conserved := fun _ _ _ => trivial }
143 no_free_knobs := F.no_continuous_moduli
144 cost_sufficient := hJ_suff
145 has_composition := fun x y hx hy =>
146 ⟨fun a _ => J (x * y) + J (x / y), rfl⟩
147 composition_continuous := fun x y hx hy =>
148 ⟨fun a _ => J (x * y) + J (x / y), continuous_const, rfl⟩ }
149
150end ClosedFramework
151end Foundation
152end IndisputableMonolith