lambda_one_is_unique_fixpoint
The theorem proves that 1 is the only positive real satisfying λ = λ^{-1}. Researchers closing the substitutivity and calibration step in Recognition Science cite it to force the Aczél family parameter under the zero-parameter posture. The tactic proof first rewrites the reciprocal hypothesis into λ² = 1 via cancellation, then applies non-linear arithmetic on the square (λ - 1)² to reach the conclusion.
claimFor any real number $λ > 0$, if $λ = λ^{-1}$, then $λ = 1$.
background
The declaration belongs to the SubstitutivityForcing module, which completes Gap 3 of the axiom-closure plan by deriving ledger consistency, substitutivity, and calibration from the Regularity Axiom alone. Substitutivity enters as the cost_sufficient field of the ledger structure; calibration is absorbed as a normalization convention that keeps structural constants at O(1) Kolmogorov complexity. The Aczél family cosh(λt) supplies the concrete setting in which the inversion map must fix a unique positive value.
proof idea
The tactic proof introduces lam together with the positivity and reciprocal hypotheses. It derives lam * lam = 1 by rewriting the given equality into the cancellation identity mul_inv_cancel₀. The final nlinarith step invokes the non-negativity of (lam - 1)² to obtain the required equality.
why it matters in Recognition Science
The result is invoked directly by calibration_forced_from_fixpoint, which forces λ = 1 for the Aczél family under the zero-parameter posture. It supplies the uniqueness step required for Phase 4 of the Gap 3 closure, aligning with the framework demand that all structural constants possess low Kolmogorov complexity. The parent theorem in the same module absorbs this uniqueness into the overall substitutivity forcing.
scope and limits
- Does not treat negative reals or complex numbers.
- Does not establish uniqueness inside larger function families.
- Does not incorporate physical constants or empirical calibration data.
Lean usage
theorem calibration_forced_from_fixpoint (lam : ℝ) (hlam_pos : 0 < lam) (hlam_inv : lam = lam⁻¹) : lam = 1 := lambda_one_is_unique_fixpoint lam hlam_pos hlam_invformal statement (Lean)
32theorem lambda_one_is_unique_fixpoint :
33 ∀ lam : ℝ, 0 < lam → lam = lam⁻¹ → lam = 1 := by
proof body
Tactic-mode proof.
34 intro lam hlam_pos hlam_eq
35 have h1 : lam * lam = 1 := by
36 have : lam * lam⁻¹ = 1 := mul_inv_cancel₀ (ne_of_gt hlam_pos)
37 rw [← hlam_eq] at this; exact this
38 nlinarith [sq_nonneg (lam - 1)]
39
40/-- **Theorem**: Among the Aczél family cosh(λt), λ = 1 is the unique
41positive real that equals its own reciprocal. Since the zero-parameter
42posture requires all structural constants to have O(1) Kolmogorov
43complexity, and λ = 1 is the unique positive fixpoint of the inversion
44map, calibration is forced. -/