IndisputableMonolith.Foundation.MaximalForcing.RSPhiUniverse

   1import IndisputableMonolith.Foundation.MaximalForcing.RealityClosure
   2import IndisputableMonolith.Foundation.PhiForcing
   3
   4/-!
   5# Maximal Forcing: the phi-layer realization (Phase 2 expansion, T6)
   6
   7Second concrete instantiation. It shows the forced-register pattern generalizes
   8beyond the cost layer to the next link of the chain (T6: phi forced by
   9self-similarity).
  10
  11* The realization carrier is a candidate scale ratio `r : ℝ`.
  12* The loose class `Lphi0` is just the positive reals.
  13* The gate class `LphiGold` adds the golden constraint `r^2 = r + 1`.
  14* The claim under closure is "r equals the golden ratio phi."
  15
  16Over `LphiGold`, "r = phi" is forced (wrapping `PhiForcing.phi_unique_self_similar`).
  17Over `Lphi0`, it is independent (phi satisfies it, but `r = 1` is a positive
  18candidate that does not). So the golden-constraint tightening does real work, the
  19same legitimacy evidence the cost layer produced for the gate conditions.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Foundation
  24namespace MaximalForcing
  25
  26open IndisputableMonolith.Foundation.PhiForcing
  27
  28/-- Admissibility for the phi layer: a positive candidate ratio satisfying the
  29golden constraint `r^2 = r + 1`. -/
  30def PhiAdmissible (r : ℝ) : Prop :=
  31  0 < r ∧ satisfies_golden_constraint r
  32
  33/-- Loosest phi class `Lphi0`: positive candidate ratios. -/
  34def Lphi0 : AdmissibilityClass ℝ where
  35  admissible := { r | 0 < r }
  36  label := "positive candidate ratios"
  37
  38/-- Gate-tightened phi class `LphiGold`: positive ratios satisfying the golden
  39constraint. -/
  40def LphiGold : AdmissibilityClass ℝ where
  41  admissible := { r | PhiAdmissible r }
  42  label := "positive ratios with golden constraint r^2 = r + 1"
  43
  44/-- `LphiGold` is a tightening of `Lphi0`. -/
  45def tighten_Lphi0_LphiGold : Tightening Lphi0 LphiGold where
  46  subset := by
  47    intro r hr
  48    exact hr.1
  49  strict_witness := True
  50
  51/-- The forced claim of the phi layer: `r` equals the golden ratio. -/
  52def isPhiClaim : RealityClaim ℝ where
  53  label := "r = φ"
  54  holds := fun r => r = φ
  55
  56/-- The phi-layer claim universe. -/
  57def phiUniverse : ClaimUniverse where
  58  Realization := ℝ
  59  admissibility := LphiGold
  60  claims := { isPhiClaim }
  61
  62/-- **T6 as a forced invariant.** Over the gate class, "r = phi" is forced. Wraps
  63`PhiForcing.phi_unique_self_similar` with no new content. -/
  64theorem forced_isPhi : Forced LphiGold.admissible isPhiClaim := by
  65  intro r hr
  66  obtain ⟨hpos, hgold⟩ := hr
  67  exact phi_unique_self_similar hpos hgold
  68
  69/-- The claim `isPhiClaim` is in the closure of the phi universe. -/
  70theorem isPhiClaim_in_closure :
  71    InClosure Primitive.lawOfLogic phiUniverse isPhiClaim := by
  72  show isPhiClaim ∈ phiUniverse.claims
  73  exact Set.mem_singleton _
  74
  75/-- Forced-register entry for T6. -/
  76def isPhiForcedInvariant : ForcedInvariant Primitive.lawOfLogic phiUniverse where
  77  claim := isPhiClaim
  78  in_closure := isPhiClaim_in_closure
  79  forced := forced_isPhi
  80
  81/-- The phi-layer universe is fully classified. -/
  82theorem phiUniverse_classifier :
  83    ∀ C : RealityClaim phiUniverse.Realization,
  84      InClosure Primitive.lawOfLogic phiUniverse C → ClaimClassification phiUniverse C := by
  85  intro C hC
  86  have hCeq : C = isPhiClaim := Set.mem_singleton_iff.mp hC
  87  subst hCeq
  88  exact ClaimClassification.forced forced_isPhi
  89
  90/-- A real `MaximalClosureCert` for the phi-layer universe. -/
  91def phiUniverseCert : MaximalClosureCert Primitive.lawOfLogic phiUniverse where
  92  classifies := phiUniverse_classifier
  93
  94/-! ## The golden-constraint tightening does real work -/
  95
  96/-- Over the loose class `Lphi0`, "r = phi" is independent: `phi` is a positive
  97candidate that satisfies it, and `1` is a positive candidate that does not. -/
  98theorem isPhi_independent_over_Lphi0 : Independent Lphi0.admissible isPhiClaim := by
  99  refine ⟨φ, 1, ?_, ?_, ?_, ?_⟩
 100  · show (0 : ℝ) < φ
 101    exact phi_pos
 102  · show (0 : ℝ) < 1
 103    norm_num
 104  · rfl
 105  · intro h
 106    have h1 : (1 : ℝ) = φ := h
 107    exact (ne_of_lt phi_gt_one) h1
 108
 109/-- **The golden-constraint tightening is legitimate, not cheap.** `isPhiClaim`
 110is independent over `Lphi0` but forced over `LphiGold`. -/
 111theorem tightening_Lphi0_LphiGold_effective :
 112    Independent Lphi0.admissible isPhiClaim ∧ Forced LphiGold.admissible isPhiClaim :=
 113  ⟨isPhi_independent_over_Lphi0, forced_isPhi⟩
 114
 115end MaximalForcing
 116end Foundation
 117end IndisputableMonolith
 118