calibration_forced_from_fixpoint
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.
claimLet $λ ∈ ℝ$ 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 in Recognition Science
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.
scope and limits
- Does not extend uniqueness to non-positive reals.
- Does not derive the Aczél family representation.
- Does not address calibration outside the real line or in discrete settings.
formal statement (Lean)
45theorem calibration_forced_from_fixpoint
46 (lam : ℝ) (hlam_pos : 0 < lam) (hlam_inv : lam = lam⁻¹) :
47 lam = 1 :=
proof body
Term-mode proof.
48 lambda_one_is_unique_fixpoint lam hlam_pos hlam_inv
49
50end SubstitutivityForcing
51end Foundation
52end IndisputableMonolith