IndisputableMonolith.RecogSpec.MassLawFromLedger

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.RSLedger
   3import IndisputableMonolith.RecogSpec.ObservablePayloads
   4import IndisputableMonolith.Constants
   5
   6/-!
   7# Mass Law from Ledger Tiers
   8
   9Derives the canonical mass-ratio payload `LeptonMassRatios` from `RSLedger`
  10tier structure.
  11
  12## Canonical semantics
  13
  14  massRatios = { mu_over_e := φ^{11}, tau_over_e := φ^{17}, tau_over_mu := φ^{6} }
  15
  16These are inter-generation mass ratios in the lepton sector, derived from the
  17torsion differences {0, 11, 17} forced by cube geometry.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace RecogSpec
  22
  23open Constants
  24
  25noncomputable section
  26
  27/-- Mass ratios derived from ledger tier structure.
  28
  29Uses `massRatioFromRungs` to compute φ-powers from rung differences
  30rather than defining them as literal φ-formulas. -/
  31def massRatiosFromTiers (L : RSLedger) (φ : ℝ) : LeptonMassRatios :=
  32  ⟨ massRatioFromRungs L φ .leptons .second .first,
  33    massRatioFromRungs L φ .leptons .third .first,
  34    massRatioFromRungs L φ .leptons .third .second ⟩
  35
  36/-- For any ledger with canonical torsion {0,11,17}, the derived mass-ratio
  37    payload equals the φ-power triple. -/
  38theorem massRatiosFromTiers_canonical (L : RSLedger) (φ : ℝ)
  39    (hL : L.torsion = generationTorsion) :
  40    massRatiosFromTiers L φ = ⟨φ ^ (11 : ℤ), φ ^ (17 : ℤ), φ ^ (6 : ℤ)⟩ := by
  41  simp only [massRatiosFromTiers]
  42  rw [massRatio_21_canonical L φ .leptons hL,
  43      massRatio_31_canonical L φ .leptons hL,
  44      massRatio_32_canonical L φ .leptons hL]
  45
  46/-- The canonical ledger produces the canonical mass-ratio payload. -/
  47theorem canonical_massRatiosFromTiers (φ : ℝ) :
  48    massRatiosFromTiers canonicalRSLedger φ =
  49      ⟨φ ^ (11 : ℤ), φ ^ (17 : ℤ), φ ^ (6 : ℤ)⟩ :=
  50  massRatiosFromTiers_canonical canonicalRSLedger φ canonicalRSLedger_torsion
  51
  52/-- All entries in the canonical mass-ratio payload are positive when φ > 0. -/
  53theorem massRatiosFromTiers_pos (L : RSLedger) (φ : ℝ) (hφ : 0 < φ)
  54    (hL : L.torsion = generationTorsion) :
  55    (massRatiosFromTiers L φ).Forall (0 < ·) := by
  56  rw [massRatiosFromTiers_canonical L φ hL]
  57  exact ⟨zpow_pos hφ 11, zpow_pos hφ 17, zpow_pos hφ 6⟩
  58
  59end
  60
  61end RecogSpec
  62end IndisputableMonolith
  63