calibration_forced_from_fixpoint
plain-language theorem explainer
The result shows that the only positive real λ equal to its reciprocal is λ = 1, which enforces calibration of the structural constant in the Aczél family cosh(λt) under the zero-parameter posture of Recognition Science. Workers on the ledger consistency axiom closure would reference it to absorb the normalization into the Regularity Axiom. The argument reduces immediately to the uniqueness of the inversion fixpoint.
Claim. Let $λ ∈ ℝ$ satisfy $λ > 0$ and $λ = λ^{-1}$. Then $λ = 1$.
background
This declaration sits in the module on Gap 3 of the axiom-closure plan, where ledger consistency forces substitutivity and calibration with zero additional axioms. The local setting absorbs calibration as a normalization convention into the Regularity Axiom, treating substitutivity as a field of the ledger structure. The upstream result states that λ = 1 is the unique positive real satisfying λ = λ^{-1}, shown by rewriting the reciprocal condition into λ ⋅ λ = 1 via cancellation.
proof idea
The proof is a one-line wrapper that applies the upstream uniqueness theorem directly to the supplied positivity and reciprocal hypotheses on λ.
why it matters
This theorem closes the calibration step in the substitutivity forcing chain, ensuring the structural constant takes the value 1 to keep Kolmogorov complexity O(1). It supports ledger consistency results and aligns with the J-uniqueness step of the forcing chain by selecting the fixed point of the inversion map. The result feeds the broader derivation of physics constants from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.