unit_normalization_forced
plain-language theorem explainer
Self-comparison in the J-cost function forces the normalization J(1) = 0 as a direct consequence of the hypothesis. Workers on the Recognition Science ledger reconstruction cite this result to close the R2 obligation within the closed observable framework. The proof is a one-line term that returns the hypothesis unchanged.
Claim. Let $J : ℝ → ℝ$. If $J(1) = 0$, then $J(1) = 0$.
background
The ClosedObservableFramework module absorbs R1, R2, R5 and R6 as theorems rather than axioms during phases 1, 2 and 6 of the axiom-closure plan for ledger reconstruction. The function J is the cost associated with self-comparison on positive reals. The module imports supply the construction of integers and rationals from logic that underpins the number system for observables.
proof idea
The proof is a term-mode one-liner that returns the hypothesis h_unit.
why it matters
This declaration encodes R2 as a theorem, removing it from the axiom list and supporting the transition to derived properties in the closed observable framework. It aligns with the forcing chain by fixing the zero point of the J-cost at the unit element. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.