IndisputableMonolith.Foundation.UniversalForcing.ReciprocalGenerator

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.PhiSupport.Lemmas
   4
   5/-!
   6# The reciprocal involution is the common generator of J and φ
   7
   8`OneLaw.lean` conjoins the cost-form theorem (J's shape) and the φ-forcing
   9theorem (the scale ratio). That conjunction is an *assembly*: its two halves
  10talk about two unrelated objects (`Cost.Jcost` and a `MinimalHierarchy`), and
  11neither is derived from the other.
  12
  13This module isolates the genuine structural unification that does sit beneath
  14both. The single object is the **reciprocal involution** `ι(x) = x⁻¹` on the
  15positive reals — the dual-recognition symmetry that exchanges a quantity with
  16its reciprocal. We prove two properties *of this one function*:
  17
  18* **Cost side.** `J` is exactly the `ι`-symmetric cost: `J ∘ ι = J`.
  19* **Scale side.** `φ` is the unique fixed point `> 1` of the `ι`-shift
  20  `g(x) = 1 + ι(x)`.
  21
  22Both conjuncts in the capstone quantify over the same `recip`. That is what
  23makes this a deduction about a shared generator rather than a glued pair of
  24independent facts: the reciprocal involution is logically upstream of both the
  25cost's symmetry axis and the golden ratio's defining equation.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Foundation
  30namespace UniversalForcing
  31namespace ReciprocalGenerator
  32
  33/-- The reciprocal involution on the positive reals, `ι(x) = x⁻¹`. This is the
  34dual-recognition symmetry the recognition framework is built on. -/
  35noncomputable def recip (x : ℝ) : ℝ := x⁻¹
  36
  37/-- `ι` is an involution on the positive reals. -/
  38theorem recip_involutive {x : ℝ} (_hx : 0 < x) : recip (recip x) = x := by
  39  simp [recip]
  40
  41/-- `ι` has a unique fixed point among positive reals, namely the unit `1`. -/
  42theorem recip_fixed_iff {x : ℝ} (hx : 0 < x) : recip x = x ↔ x = 1 := by
  43  unfold recip
  44  have hxne : x ≠ 0 := ne_of_gt hx
  45  constructor
  46  · intro h
  47    have hsq : x * x = 1 := by
  48      have hmul : x⁻¹ * x = x * x := by rw [h]
  49      rw [inv_mul_cancel₀ hxne] at hmul
  50      exact hmul.symm
  51    nlinarith [hsq, hx]
  52  · intro h; subst h; simp
  53
  54/-! ## Cost side: J is the ι-symmetric cost -/
  55
  56/-- `J` is invariant under the reciprocal involution: `J(ι x) = J(x)`. This is
  57`Cost.Jcost_symm`, here phrased as a property of `recip`. -/
  58theorem jcost_recip_symmetric {x : ℝ} (hx : 0 < x) :
  59    Cost.Jcost (recip x) = Cost.Jcost x := by
  60  unfold recip
  61  exact (Cost.Jcost_symm hx).symm
  62
  63/-- **The involution's fixed point is the cost's zero.** For positive `x`,
  64`ι x = x ↔ J x = 0` — both hold iff `x = 1`. So `ι`'s own fixed point is not
  65arbitrary: it is the unit, the unique point of zero recognition cost. This is
  66the sharp form of the cost side — not merely that `J` is `ι`-symmetric, but that
  67the symmetry axis of `ι` coincides with the null set of `J`. -/
  68theorem recip_fixed_iff_cost_zero {x : ℝ} (hx : 0 < x) :
  69    recip x = x ↔ Cost.Jcost x = 0 := by
  70  rw [recip_fixed_iff hx, Cost.Jcost_eq_zero_iff x hx]
  71
  72/-! ## Scale side: φ is the unique fixed point > 1 of the ι-shift -/
  73
  74/-- The reciprocal-shift map `g(x) = 1 + ι(x) = 1 + x⁻¹`. Its fixed-point
  75equation `g(x) = x` is the self-similarity constraint `x = 1 + 1/x`. -/
  76noncomputable def recipShift (x : ℝ) : ℝ := 1 + recip x
  77
  78/-- `φ` is a fixed point of the `ι`-shift. -/
  79theorem phi_is_recipShift_fixed : recipShift Constants.phi = Constants.phi := by
  80  unfold recipShift recip
  81  have h := PhiSupport.phi_fixed_point
  82  rw [one_div] at h
  83  exact h.symm
  84
  85/-- `φ` is the **unique** fixed point of the `ι`-shift among reals `> 1`. -/
  86theorem recipShift_fixed_iff {x : ℝ} (hx : 1 < x) :
  87    recipShift x = x ↔ x = Constants.phi := by
  88  unfold recipShift recip
  89  have hx0 : (0 : ℝ) < x := lt_trans one_pos hx
  90  have hxne : x ≠ 0 := ne_of_gt hx0
  91  constructor
  92  · intro h
  93    have hexp : (1 + x⁻¹) * x = x + 1 := by
  94      rw [add_mul, one_mul, inv_mul_cancel₀ hxne]
  95    have hmul : (1 + x⁻¹) * x = x * x := by rw [h]
  96    rw [hexp] at hmul
  97    have hsq : x ^ 2 = x + 1 := by rw [pow_two]; linarith [hmul]
  98    exact (PhiSupport.phi_unique_pos_root x).mp ⟨hsq, hx0⟩
  99  · intro h; subst h
 100    have h := PhiSupport.phi_fixed_point
 101    rw [one_div] at h
 102    exact h.symm
 103
 104/-! ## Capstone: one generator, two forced quantities -/
 105
 106/-- **The reciprocal involution generates both the cost and the scale.**
 107
 108The single function `recip = (·⁻¹)` is the structural object underneath both
 109sides of the math/physics bridge:
 110
 111* `J` is exactly the `ι`-symmetric cost: `∀ x > 0, J(ι x) = J(x)`.
 112* `φ` is the unique fixed point `> 1` of the `ι`-shift `1 + ι`.
 113
 114Both conjuncts quantify over the *same* `recip`. Unlike `OneLaw`'s assembly of
 115two facts about unrelated objects, this is a deduction about a shared
 116generator: the reciprocal involution is upstream of both the cost's symmetry
 117axis and the golden ratio's defining equation. -/
 118theorem recip_generates_cost_and_scale :
 119    (∀ x : ℝ, 0 < x → Cost.Jcost (recip x) = Cost.Jcost x)
 120    ∧ (∀ x : ℝ, 1 < x → (recipShift x = x ↔ x = Constants.phi)) :=
 121  ⟨fun _ hx => jcost_recip_symmetric hx,
 122   fun _ hx => recipShift_fixed_iff hx⟩
 123
 124/-- **One involution, two constants.** The reciprocal involution `ι` pins both
 125fundamental quantities of the framework through its fixed points:
 126
 127* the fixed point of `ι` itself is the unit `1`, which is exactly the zero of
 128  the recognition cost `J` (the no-cost point);
 129* the fixed point of the affine shift `1 + ι` is the golden ratio `φ`, the
 130  scale.
 131
 132This is the sharpest form of the bridge. The unit and the scale — the two
 133constants the whole framework is built from — are the two fixed points of one
 134involution family: `ι` fixes the unit (= `J`'s null point), and `1 + ι` fixes
 135`φ`. -/
 136theorem recip_pins_unit_and_scale :
 137    (∀ x : ℝ, 0 < x → (recip x = x ↔ Cost.Jcost x = 0))
 138    ∧ (∀ x : ℝ, 1 < x → (recipShift x = x ↔ x = Constants.phi)) :=
 139  ⟨fun _ hx => recip_fixed_iff_cost_zero hx,
 140   fun _ hx => recipShift_fixed_iff hx⟩
 141
 142/-- Certificate: the reciprocal involution is the common generator of `J` and
 143`φ`. Bundles the involution law, both downstream forcings, and the witness that
 144`φ` actually solves the `ι`-shift fixed-point equation. -/
 145structure ReciprocalGeneratorCert where
 146  involutive : ∀ x : ℝ, 0 < x → recip (recip x) = x
 147  cost_symmetric : ∀ x : ℝ, 0 < x → Cost.Jcost (recip x) = Cost.Jcost x
 148  unit_is_cost_zero : ∀ x : ℝ, 0 < x → (recip x = x ↔ Cost.Jcost x = 0)
 149  scale_unique : ∀ x : ℝ, 1 < x → (recipShift x = x ↔ x = Constants.phi)
 150  phi_solves : recipShift Constants.phi = Constants.phi
 151
 152/-- The certificate holds. -/
 153noncomputable def reciprocalGeneratorCert_holds : ReciprocalGeneratorCert where
 154  involutive := fun _ hx => recip_involutive hx
 155  cost_symmetric := fun _ hx => jcost_recip_symmetric hx
 156  unit_is_cost_zero := fun _ hx => recip_fixed_iff_cost_zero hx
 157  scale_unique := fun _ hx => recipShift_fixed_iff hx
 158  phi_solves := phi_is_recipShift_fixed
 159
 160end ReciprocalGenerator
 161end UniversalForcing
 162end Foundation
 163end IndisputableMonolith
 164