lambda_one_is_unique_fixpoint
plain-language theorem explainer
The positive real λ satisfying λ = λ^{-1} equals 1. Researchers on the Aczél family cosh(λt) or zero-parameter calibration in Recognition Science cite the result to force the structural constant. The tactic proof multiplies the given equation by λ to reach λ² = 1 then applies nlinarith to the non-negative square (λ - 1)².
Claim. Let λ be a positive real number. If λ equals its reciprocal, then λ equals 1.
background
The theorem belongs to the SubstitutivityForcing module, which closes Gap 3 of the axiom-closure plan by treating substitutivity as a ledger field (cost_sufficient) and calibration as a normalization absorbed into the Regularity Axiom. The reciprocal automorphism from CostAlgebra supplies the inversion map used in the hypothesis. The module imports LedgerCanonicality and LedgerForcing, whose reciprocal lemma supplies the algebraic identity λ · λ^{-1} = 1 for positive λ.
proof idea
The tactic proof introduces the positive real lam together with the two hypotheses. It derives lam · lam = 1 by rewriting the given equality into mul_inv_cancel₀ and then applies nlinarith to the non-negative quantity (lam - 1)².
why it matters
The result is invoked verbatim by the downstream theorem calibration_forced_from_fixpoint, which states that λ = 1 is forced for the Aczél family under the zero-parameter posture requiring O(1) Kolmogorov complexity. It supplies the unique positive fixpoint of the inversion map needed for calibration in the ledger structure of Gap 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.