IndisputableMonolith.Foundation.MaximalForcing.RSMassLadderUniverse

   1import IndisputableMonolith.Foundation.MaximalForcing.RealityClosure
   2import IndisputableMonolith.Foundation.PhiForcing
   3
   4/-!
   5# Maximal Forcing: the mass-ladder layer (Phase 2 extension, forced scaling)
   6
   7Fifth concrete instantiation, and the first whose closure genuinely uses two
   8branches of the trichotomy.
   9
  10The RS mass law places masses on a phi-ladder: `m(rung) = yardstick · φ^rung`. The
  11honest separation the execution plan predicted is realized here in machine-checked
  12form:
  13
  14* the dimensionless scaling invariant (the ratio of adjacent rungs is `φ`) is
  15  **forced** over every yardstick, with no gate at all, because it is a structural
  16  property of the ladder; while
  17* the absolute yardstick is **independent**: it is a free coordinate, with an
  18  explicit countermodel pair.
  19
  20So this universe's closure contains one `Forced` claim and one `Independent`
  21claim. The classifier exercises both `ClaimClassification.forced` and
  22`ClaimClassification.independent`, proving the maximal-forcing machinery is not
  23trivially always-forced: it distinguishes invariants from coordinates.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Foundation
  28namespace MaximalForcing
  29
  30open IndisputableMonolith.Foundation.PhiForcing
  31
  32/-- A point on the phi-ladder: `ladderMass M0 r = M0 · φ^r`. The carrier is the
  33yardstick `M0`; the rung `r` is the index. -/
  34noncomputable def ladderMass (M0 : ℝ) (r : ℕ) : ℝ := M0 * φ ^ r
  35
  36/-- The only class needed: every candidate yardstick. The scaling invariant is
  37forced here without any tightening. -/
  38def Lmass0 : AdmissibilityClass ℝ where
  39  admissible := Set.univ
  40  label := "every candidate yardstick"
  41
  42/-- Forced claim: adjacent rungs differ by the factor `φ`. This is the
  43dimensionless scaling invariant, independent of the yardstick. -/
  44def isLadderRatioClaim : RealityClaim ℝ where
  45  label := "ladderMass M0 (r+1) = φ · ladderMass M0 r for all r"
  46  holds := fun M0 => ∀ r : ℕ, ladderMass M0 (r + 1) = φ * ladderMass M0 r
  47
  48/-- Independent claim: the yardstick equals one (an absolute-unit choice). -/
  49def isYardstickClaim : RealityClaim ℝ where
  50  label := "M0 = 1"
  51  holds := fun M0 => M0 = 1
  52
  53/-- The mass-ladder claim universe, carrying one forced and one independent claim. -/
  54def massUniverse : ClaimUniverse where
  55  Realization := ℝ
  56  admissibility := Lmass0
  57  claims := { isLadderRatioClaim, isYardstickClaim }
  58
  59/-- **The phi-ladder scaling invariant is forced over every yardstick.** No gate
  60is required: the recurrence is a structural identity of the ladder. -/
  61theorem forced_ladderRatio : Forced Lmass0.admissible isLadderRatioClaim := by
  62  intro M0 _ r
  63  show ladderMass M0 (r + 1) = φ * ladderMass M0 r
  64  unfold ladderMass
  65  rw [pow_succ]
  66  ring
  67
  68/-- **The yardstick is independent.** Two admissible yardsticks (1 and 2) disagree
  69on the claim `M0 = 1`. The absolute mass scale is a free coordinate, not a forced
  70invariant. -/
  71def yardstickIndepWitness : IndependenceWitness massUniverse isYardstickClaim where
  72  yes_model := (1 : ℝ)
  73  no_model := (2 : ℝ)
  74  yes_admissible := trivial
  75  no_admissible := trivial
  76  yes_holds := rfl
  77  no_fails := by
  78    intro h
  79    have h1 : (2 : ℝ) = 1 := h
  80    norm_num at h1
  81
  82/-- The yardstick claim is independent (Prop-level), via the witness. -/
  83theorem yardstick_independent : Independent Lmass0.admissible isYardstickClaim :=
  84  independent_of_witness yardstickIndepWitness
  85
  86/-- **Mixed classifier.** Every claim in the mass-ladder closure is classified:
  87the scaling invariant as `forced`, the yardstick as `independent`. This is the
  88first universe whose certificate uses both branches. -/
  89theorem massUniverse_classifier :
  90    ∀ C : RealityClaim massUniverse.Realization,
  91      InClosure Primitive.lawOfLogic massUniverse C → ClaimClassification massUniverse C := by
  92  intro C hC
  93  have hmem : C ∈ massUniverse.claims := hC
  94  simp only [massUniverse, Set.mem_insert_iff, Set.mem_singleton_iff] at hmem
  95  rcases hmem with h | h
  96  · subst h; exact ClaimClassification.forced forced_ladderRatio
  97  · subst h; exact ClaimClassification.independent yardstickIndepWitness
  98
  99/-- A real `MaximalClosureCert` for the mass-ladder universe (mixed
 100classification). -/
 101def massUniverseCert : MaximalClosureCert Primitive.lawOfLogic massUniverse where
 102  classifies := massUniverse_classifier
 103
 104/-- **Crown trichotomy on the mass-ladder universe.** Every closure claim is
 105`Forced`, `Independent`, or `Selected`. Here the closure splits into one forced
 106invariant and one independent coordinate, with `Selected` empty. -/
 107theorem massUniverse_trichotomy
 108    (C : RealityClaim massUniverse.Realization)
 109    (hC : InClosure Primitive.lawOfLogic massUniverse C) :
 110    Forced Lmass0.admissible C ∨ Independent Lmass0.admissible C ∨ Selected Lmass0.admissible C :=
 111  maximal_forcing_closure_trichotomy massUniverseCert C hC
 112
 113/-- The honest mass-layer summary: the scaling invariant is forced, the yardstick
 114is independent. Dimensionless structure is forced; absolute units are free. -/
 115theorem mass_scaling_forced_yardstick_free :
 116    Forced Lmass0.admissible isLadderRatioClaim ∧
 117    Independent Lmass0.admissible isYardstickClaim :=
 118  ⟨forced_ladderRatio, yardstick_independent⟩
 119
 120end MaximalForcing
 121end Foundation
 122end IndisputableMonolith
 123