IndisputableMonolith.Verification.WallpaperSufficiencyMassPath

   1import Mathlib
   2import IndisputableMonolith.Constants.AlphaDerivation
   3import IndisputableMonolith.Physics.MassTopology
   4import IndisputableMonolith.Physics.LeptonGenerations.Defs
   5import IndisputableMonolith.Verification.WallpaperEndogenousBridge
   6
   7/-!
   8# Wallpaper Sufficiency for the Mass Path
   9
  10This module formalizes the "sufficiency route" for O6 in the mass framework:
  11the canonical mass-path formulas are unchanged when the imported crystallographic
  12constant `wallpaper_groups` is replaced by the endogenous cube-derived
  13`W_from_cube = E_passive + F` (at `D=3`).
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Verification
  18namespace WallpaperSufficiencyMassPath
  19
  20open Constants.AlphaDerivation
  21open Physics.MassTopology
  22open Physics.LeptonGenerations
  23open WallpaperEndogenousBridge
  24
  25noncomputable section
  26
  27/-- Endogenous and imported `W` coincide on the canonical dimension. -/
  28theorem W_endogenous_eq_massTopology_W : W_from_cube = W := by
  29  simpa [W] using W_from_cube_eq_wallpaper_groups
  30
  31/-- The ledger-fraction formula is invariant under replacing `W` by `W_from_cube`. -/
  32theorem ledger_fraction_rewrite_endogenous :
  33    ledger_fraction = (W_from_cube + E_total) / (4 * E_passive) := by
  34  unfold ledger_fraction
  35  rw [W_endogenous_eq_massTopology_W]
  36
  37/-- The base shift is invariant under the endogenous replacement of `W`. -/
  38theorem base_shift_rewrite_endogenous :
  39    base_shift = 2 * (W_from_cube : ℝ) + ((W_from_cube + E_total) / (4 * E_passive) : ℚ) := by
  40  have hW : (W : ℝ) = (W_from_cube : ℝ) := by
  41    exact_mod_cast W_endogenous_eq_massTopology_W.symm
  42  calc
  43    base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by simp [base_shift]
  44    _ = 2 * (W_from_cube : ℝ) + ((W_from_cube + E_total) / (4 * E_passive) : ℚ) := by
  45          simp [hW, ledger_fraction_rewrite_endogenous]
  46
  47/-- The mu→tau step formula is invariant under the endogenous replacement of `W`. -/
  48theorem step_mu_tau_rewrite_endogenous :
  49    step_mu_tau = (cube_faces D : ℝ) - (2 * W_from_cube + D) / 2 * Constants.alpha := by
  50  have hW : wallpaper_groups = W_from_cube := by
  51    simpa [W] using W_endogenous_eq_massTopology_W.symm
  52  simp [step_mu_tau, hW]
  53
  54/-- Packaged mass-path closure: all canonical `W`-bearing formulas used in the
  55mass path are invariant under replacing imported `wallpaper_groups` with
  56endogenous `W_from_cube`. -/
  57theorem mass_path_endogenous_replacement_complete :
  58    W_from_cube = W ∧
  59    ledger_fraction = (W_from_cube + E_total) / (4 * E_passive) ∧
  60    base_shift = 2 * (W_from_cube : ℝ) + ((W_from_cube + E_total) / (4 * E_passive) : ℚ) ∧
  61    step_mu_tau = (cube_faces D : ℝ) - (2 * W_from_cube + D) / 2 * Constants.alpha := by
  62  refine ⟨W_endogenous_eq_massTopology_W, ledger_fraction_rewrite_endogenous,
  63    base_shift_rewrite_endogenous, step_mu_tau_rewrite_endogenous⟩
  64
  65end
  66end WallpaperSufficiencyMassPath
  67end Verification
  68end IndisputableMonolith
  69