IndisputableMonolith.Foundation.MaximalForcing.RSSelectionExample

   1import IndisputableMonolith.Foundation.MaximalForcing.RSPhiUniverse
   2
   3/-!
   4# Maximal Forcing: a genuine Selected claim and its drainage (Phase 4)
   5
   6The other layers exercise the `Forced` branch (cost, phi, dimension, alpha) and
   7the `Independent` branch (the mass yardstick). This module exercises the third
   8branch, `Selected`, honestly.
   9
  10Consider the class `Lgolden` of ratios satisfying the golden constraint
  11`r^2 = r + 1`, but WITHOUT a positivity requirement. Over this class:
  12
  13* "r = phi" is **not forced**: the conjugate root ψ = (1 - √5)/2 satisfies the
  14  same constraint and differs from phi. (So independence is also provable here;
  15  `Selected` is the honest interim tag because a named principle resolves it.)
  16* a named **selection principle** governs it: positivity (the physical scale ratio
  17  is the expanding root, > 1).
  18
  19That is exactly `Selected`. Crucially, `Selected` is not an endpoint. Its drainage
  20is explicit: adopting positivity as a tightening (`Lgolden → LphiGold`) promotes
  21the claim to `Forced`, which is `forced_isPhi`. This module shows both the tag and
  22its resolution, so the third branch is never a place a claim goes to die.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Foundation
  27namespace MaximalForcing
  28
  29open IndisputableMonolith.Foundation.PhiForcing
  30
  31/-- The conjugate root of the golden constraint. -/
  32noncomputable def psi : ℝ := (1 - Real.sqrt 5) / 2
  33
  34/-- The conjugate root satisfies the golden constraint `r^2 = r + 1`. -/
  35theorem psi_golden : satisfies_golden_constraint psi := by
  36  unfold satisfies_golden_constraint psi
  37  have hs : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num)
  38  linear_combination (1 / 4 : ℝ) * hs
  39
  40/-- The conjugate root differs from phi (it is the contracting root). -/
  41theorem psi_ne_phi : psi ≠ φ := by
  42  have h5 : 0 < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num)
  43  have hlt : psi < φ := by
  44    simp only [psi, φ]
  45    linarith [h5]
  46  exact ne_of_lt hlt
  47
  48/-- The golden-constraint class, without positivity. This is strictly looser than
  49`LphiGold`, which also requires `0 < r`. -/
  50def Lgolden : AdmissibilityClass ℝ where
  51  admissible := { r | satisfies_golden_constraint r }
  52  label := "golden-constraint ratios (no positivity)"
  53
  54/-- `LphiGold` is a tightening of `Lgolden` by adding positivity. -/
  55def tighten_Lgolden_LphiGold : Tightening Lgolden LphiGold where
  56  subset := by
  57    intro r hr
  58    exact hr.2
  59  strict_witness := True
  60
  61/-- "r = phi" is **not forced** over the golden-only class: the conjugate root is
  62an admissible counterexample. -/
  63theorem isPhi_not_forced_over_Lgolden : ¬ Forced Lgolden.admissible isPhiClaim := by
  64  intro hF
  65  have hpsi : psi = φ := hF psi psi_golden
  66  exact psi_ne_phi hpsi
  67
  68/-- The named selection principle: positivity picks the expanding root. -/
  69def positivitySelection : SelectionPrinciple Lgolden.admissible isPhiClaim where
  70  label := "positivity: the physical scale ratio is the expanding (> 1) root"
  71  applies := 0 < φ
  72
  73/-- **"r = phi" is Selected over the golden-only class.** Not forced, but governed
  74by the positivity selection principle. This is the third branch of the trichotomy,
  75reached honestly. -/
  76theorem isPhi_selected_over_Lgolden : Selected Lgolden.admissible isPhiClaim :=
  77  ⟨isPhi_not_forced_over_Lgolden, ⟨positivitySelection⟩⟩
  78
  79/-- **Drainage of the Selected tag.** Selected is not an endpoint: adopting the
  80positivity principle as a tightening (`Lgolden → LphiGold`) promotes the claim to
  81`Forced`. The promotion is exactly `forced_isPhi`. So this Selected entry has a
  82proved resolution, not a perpetual hold. -/
  83theorem positivity_promotes_selected_to_forced :
  84    Selected Lgolden.admissible isPhiClaim ∧
  85    Nonempty (Tightening Lgolden LphiGold) ∧
  86    Forced LphiGold.admissible isPhiClaim :=
  87  ⟨isPhi_selected_over_Lgolden, ⟨tighten_Lgolden_LphiGold⟩, forced_isPhi⟩
  88
  89/-! ## A universe exercising all three branches in one closure
  90
  91`triUniverse` collects, over the golden-only class, the phi claim (Selected) and a
  92trivially-forced tautology, plus an independent claim, so its certificate uses all
  93three constructors. This is the witness that the maximal-forcing machinery is
  94complete: it can land a claim in any of the three buckets. -/
  95
  96/-- A trivially forced claim (holds in every realization). -/
  97def trivialClaim : RealityClaim ℝ where
  98  label := "True (forced everywhere)"
  99  holds := fun _ => True
 100
 101/-- A claim that is independent over the golden-only class: "r = phi" is replaced
 102by "r > 0", which phi satisfies and psi does not. -/
 103def positiveClaim : RealityClaim ℝ where
 104  label := "0 < r"
 105  holds := fun r => 0 < r
 106
 107theorem trivialClaim_forced : Forced Lgolden.admissible trivialClaim := by
 108  intro _ _; trivial
 109
 110theorem positiveClaim_independent : Independent Lgolden.admissible positiveClaim := by
 111  refine ⟨φ, psi, ?_, ?_, ?_, ?_⟩
 112  · show satisfies_golden_constraint φ
 113    exact phi_equation
 114  · show satisfies_golden_constraint psi
 115    exact psi_golden
 116  · show (0 : ℝ) < φ
 117    exact phi_pos
 118  · intro h
 119    have hpos : (0 : ℝ) < psi := h
 120    have h5 : (1 : ℝ) < Real.sqrt 5 := by
 121      have hlt : Real.sqrt 1 < Real.sqrt 5 := by
 122        apply Real.sqrt_lt_sqrt <;> norm_num
 123      simpa using hlt
 124    have hneg : psi < 0 := by simp only [psi]; linarith
 125    linarith
 126
 127/-- The universe exercising all three branches in one closure. -/
 128def triUniverse : ClaimUniverse where
 129  Realization := ℝ
 130  admissibility := Lgolden
 131  claims := { trivialClaim, isPhiClaim, positiveClaim }
 132
 133/-- Independence witness for `positiveClaim` over `triUniverse`. -/
 134noncomputable def positiveIndepWitness : IndependenceWitness triUniverse positiveClaim where
 135  yes_model := φ
 136  no_model := psi
 137  yes_admissible := phi_equation
 138  no_admissible := psi_golden
 139  yes_holds := phi_pos
 140  no_fails := by
 141    intro h
 142    have hpos : (0 : ℝ) < psi := h
 143    have h5 : (1 : ℝ) < Real.sqrt 5 := by
 144      have hlt : Real.sqrt 1 < Real.sqrt 5 := by
 145        apply Real.sqrt_lt_sqrt <;> norm_num
 146      simpa using hlt
 147    have hneg : psi < 0 := by simp only [psi]; linarith
 148    linarith
 149
 150/-- **All three branches in one certificate.** Over the golden-only class, the
 151trivial claim is `forced`, the phi claim is `selected` (by positivity), and the
 152positivity claim is `independent` (phi vs psi). The classifier uses every
 153constructor of `ClaimClassification`. -/
 154theorem triUniverse_classifier :
 155    ∀ C : RealityClaim triUniverse.Realization,
 156      InClosure Primitive.lawOfLogic triUniverse C → ClaimClassification triUniverse C := by
 157  intro C hC
 158  have hmem : C ∈ triUniverse.claims := hC
 159  simp only [triUniverse, Set.mem_insert_iff, Set.mem_singleton_iff] at hmem
 160  rcases hmem with h | h | h
 161  · subst h; exact ClaimClassification.forced trivialClaim_forced
 162  · subst h; exact ClaimClassification.selected isPhi_selected_over_Lgolden
 163  · subst h; exact ClaimClassification.independent positiveIndepWitness
 164
 165/-- A real certificate for the three-branch universe. -/
 166def triUniverseCert : MaximalClosureCert Primitive.lawOfLogic triUniverse where
 167  classifies := triUniverse_classifier
 168
 169/-- **The maximal-forcing machinery is complete and non-degenerate.** A single
 170closure realizes all three branches of the trichotomy with proofs: one forced, one
 171selected, one independent. This rules out the failure mode where the classifier is
 172secretly always-forced or always-independent. -/
 173theorem all_three_branches_realized :
 174    Forced Lgolden.admissible trivialClaim ∧
 175    Selected Lgolden.admissible isPhiClaim ∧
 176    Independent Lgolden.admissible positiveClaim :=
 177  ⟨trivialClaim_forced, isPhi_selected_over_Lgolden, positiveClaim_independent⟩
 178
 179end MaximalForcing
 180end Foundation
 181end IndisputableMonolith
 182