IndisputableMonolith.Verification.QuarkCoordinateUnification

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Quark Coordinate Unification (Pass 2)
   6
   7This module proves a key structural fact:
   8
   9The two quark mass coordinate conventions are mathematically equivalent
  10representations of the same positive mass law once a reference mass is fixed.
  11
  12## Conventions
  13
  141. **Core form** (integer-rung architecture):
  15   `m = A_sector * φ^(r - 8 + gap)`
  16
  172. **Quarter/Residue form** (reference-mass coordinates):
  18   `m = m_ref * φ^R`
  19
  20The map between them is explicit:
  21`R = log_φ(A_sector / m_ref) + (r - 8 + gap)`.
  22
  23So the quarter coordinate is not a second physical law; it is a reparameterization
  24of the same multiplicative φ-ladder once a reference mass is chosen.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Verification
  29namespace QuarkCoordinateUnification
  30
  31open Constants
  32
  33noncomputable section
  34
  35/-- The core exponent in the integer-rung architecture. -/
  36def coreExponent (r : ℤ) (gap : ℝ) : ℝ :=
  37  (r : ℝ) - 8 + gap
  38
  39/-- Core mass law shape (sector yardstick form). -/
  40def coreMass (A_sector : ℝ) (r : ℤ) (gap : ℝ) : ℝ :=
  41  A_sector * phi ^ (coreExponent r gap)
  42
  43/-- Residue/quarter coordinate mass law shape (reference mass form). -/
  44def residueMass (m_ref : ℝ) (R : ℝ) : ℝ :=
  45  m_ref * phi ^ R
  46
  47/-- Coordinate transform from core parameters to residue coordinate. -/
  48def residueFromCore (A_sector m_ref : ℝ) (r : ℤ) (gap : ℝ) : ℝ :=
  49  Real.logb phi (A_sector / m_ref) + coreExponent r gap
  50
  51/-- Coordinate transform from residue coordinate to a core yardstick at fixed `(r,gap)`. -/
  52def yardstickFromResidue (m_ref : ℝ) (R : ℝ) (r : ℤ) (gap : ℝ) : ℝ :=
  53  m_ref * phi ^ (R - coreExponent r gap)
  54
  55/-- Core form equals residue form under the explicit coordinate transform. -/
  56theorem core_eq_residue_of_positive
  57    {A_sector m_ref : ℝ} {r : ℤ} {gap : ℝ}
  58    (hA : 0 < A_sector) (hm : 0 < m_ref) :
  59    coreMass A_sector r gap = residueMass m_ref (residueFromCore A_sector m_ref r gap) := by
  60  unfold coreMass residueMass residueFromCore coreExponent
  61  have hratio : 0 < A_sector / m_ref := div_pos hA hm
  62  have hpow : A_sector / m_ref = phi ^ (Real.logb phi (A_sector / m_ref)) :=
  63    (Real.rpow_logb phi_pos phi_ne_one hratio).symm
  64  calc
  65    A_sector * phi ^ ((r : ℝ) - 8 + gap)
  66        = (m_ref * (A_sector / m_ref)) * phi ^ ((r : ℝ) - 8 + gap) := by
  67            field_simp [hm.ne']
  68    _ = m_ref * ((A_sector / m_ref) * phi ^ ((r : ℝ) - 8 + gap)) := by ring
  69    _ = m_ref * (phi ^ (Real.logb phi (A_sector / m_ref)) * phi ^ ((r : ℝ) - 8 + gap)) := by
  70          congr 1
  71          exact congrArg (fun t => t * phi ^ ((r : ℝ) - 8 + gap)) hpow
  72    _ = m_ref * phi ^ (Real.logb phi (A_sector / m_ref) + ((r : ℝ) - 8 + gap)) := by
  73          rw [← Real.rpow_add phi_pos]
  74
  75/-- Residue form equals core form under the explicit inverse transform. -/
  76theorem residue_eq_core
  77    {m_ref : ℝ} {R : ℝ} {r : ℤ} {gap : ℝ} :
  78    residueMass m_ref R = coreMass (yardstickFromResidue m_ref R r gap) r gap := by
  79  unfold residueMass coreMass yardstickFromResidue coreExponent
  80  let E : ℝ := (r : ℝ) - 8 + gap
  81  have hpow : phi ^ R = phi ^ (R - E) * phi ^ E := by
  82    have h := (Real.rpow_add phi_pos (R - E) E)
  83    have hsum : (R - E) + E = R := by ring
  84    simpa [hsum] using h
  85  calc
  86    m_ref * phi ^ R
  87        = m_ref * (phi ^ (R - E) * phi ^ E) := by rw [hpow]
  88    _ = (m_ref * phi ^ (R - E)) * phi ^ E := by ring
  89    _ = (m_ref * phi ^ (R - ((r : ℝ) - 8 + gap))) * phi ^ ((r : ℝ) - 8 + gap) := by
  90          simp [E]
  91
  92/-- Recover residue coordinate from a residue-form mass exactly. -/
  93theorem recover_residue_coordinate
  94    {m_ref : ℝ} {R : ℝ}
  95    (hm : 0 < m_ref) :
  96    Real.logb phi (residueMass m_ref R / m_ref) = R := by
  97  unfold residueMass
  98  have hdiv : (m_ref * phi ^ R) / m_ref = phi ^ R := by
  99    field_simp [hm.ne']
 100  rw [hdiv]
 101  exact Real.logb_rpow phi_pos phi_ne_one
 102
 103/-- Structural interpretation: once a positive reference mass is fixed,
 104the two coordinate systems are equivalent (up to explicit transforms). -/
 105theorem coordinate_systems_equivalent :
 106    ∀ {A_sector m_ref : ℝ} {r : ℤ} {gap : ℝ},
 107      0 < A_sector → 0 < m_ref →
 108      ∃ R : ℝ,
 109        coreMass A_sector r gap = residueMass m_ref R := by
 110  intro A_sector m_ref r gap hA hm
 111  refine ⟨residueFromCore A_sector m_ref r gap, ?_⟩
 112  exact core_eq_residue_of_positive hA hm
 113
 114end
 115
 116end QuarkCoordinateUnification
 117end Verification
 118end IndisputableMonolith
 119