lambda_one_is_unique_fixpoint

formal source

  29  L.cost_sufficient x₁ x₂ y hx₁ hx₂ hJ_eq hy
  30
  31/-- `λ = 1` is the unique positive real satisfying `λ = λ⁻¹`. -/
  32theorem lambda_one_is_unique_fixpoint :
  33    ∀ lam : ℝ, 0 < lam → lam = lam⁻¹ → lam = 1 := by
  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. -/
  45theorem calibration_forced_from_fixpoint
  46    (lam : ℝ) (hlam_pos : 0 < lam) (hlam_inv : lam = lam⁻¹) :
  47    lam = 1 :=
  48  lambda_one_is_unique_fixpoint lam hlam_pos hlam_inv
  49
  50end SubstitutivityForcing
  51end Foundation
  52end IndisputableMonolith