Charged-lepton resonance ladder, global-detuning obstruction

Independent of Triality / SO(8) Lie closure. Shared Rindler scaffolding lives in GlobalDetuning (effCorrected, effUnified, GlobalDetuningHypothesis, lapse bridge).

Shell anchors m_tau, m_mu, m_e match LeptonGenerationLockin — keep in sync (τ at lock-in; μ and e on larger shells).

HQVM packaging: see GlobalDetuningHypothesis.fromLapseScalars and deltaGlobal_eq_lambda_mul_lapseIncrement (proved).

No PDG closure.

A. Local ladder

def Hqiv.Physics.LeptonResonanceGlobalDetuning.m_tau : ℕ

τ / μ / e shells — must match LeptonGenerationLockin.

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.m_tau = 4

def Hqiv.Physics.LeptonResonanceGlobalDetuning.m_mu : ℕ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.m_mu = 81

def Hqiv.Physics.LeptonResonanceGlobalDetuning.m_e : ℕ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.m_e = 16336

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.eff (m : ℕ) : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.eff m = Hqiv.Physics.shellSurface m / Hqiv.Physics.rindlerDetuningShared ↑m

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.eff_eq_detunedShellSurface (m : ℕ) : eff m = detunedShellSurface m

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.eff_pos (m : ℕ) : 0 < eff m

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.eff_eq_effCorrected_zero (m : ℕ) : eff m = effCorrected 0 m

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.kTauMu : ℝ

μ–τ surface ratio (outer / inner); same direction as ChargedLeptonResonance.resonance_k_tau_mu.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.kMuE : ℝ

e–μ surface ratio (outer / inner); same direction as ChargedLeptonResonance.resonance_k_mu_e.

Equations

• One or more equations did not get rendered due to their size.

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.kTauMu_pos : 0 < kTauMu

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.kMuE_pos : 0 < kMuE

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.kTauMu_eq_eff_ratio : kTauMu = eff m_mu / eff m_tau

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.kMuE_eq_eff_ratio : kMuE = eff m_e / eff m_mu

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.kTauMu_eq_geometricResonanceStep : kTauMu = geometricResonanceStep m_mu m_tau

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.kMuE_eq_geometricResonanceStep : kMuE = geometricResonanceStep m_e m_mu

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.kTauMuCorrected (δ : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.kMuECorrected (δ : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

Algebraic obstruction

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.tau_mu_ratio_iff_delta_linear (δ r₁ Sτ Sμ τ μ : ℝ) (hSμ : Sμ ≠ 0) (hDτ : 1 + c_rindler_shared * τ + δ ≠ 0) (hDμ : 1 + c_rindler_shared * μ + δ ≠ 0) : Sτ / (1 + c_rindler_shared * τ + δ) / (Sμ / (1 + c_rindler_shared * μ + δ)) = r₁ ↔ δ * (Sτ - r₁ * Sμ) = r₁ * Sμ * (1 + c_rindler_shared * τ) - Sτ * (1 + c_rindler_shared * μ)

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.mu_tau_ratio_iff_delta_linear (δ r₁ Sτ Sμ τ μ : ℝ) (hSτ : Sτ ≠ 0) (hDμ : 1 + c_rindler_shared * μ + δ ≠ 0) (hDτ : 1 + c_rindler_shared * τ + δ ≠ 0) : Sμ / (1 + c_rindler_shared * μ + δ) / (Sτ / (1 + c_rindler_shared * τ + δ)) = r₁ ↔ δ * (Sμ - r₁ * Sτ) = r₁ * Sτ * (1 + c_rindler_shared * μ) - Sμ * (1 + c_rindler_shared * τ)

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.mu_e_ratio_iff_delta_linear (δ r₂ Sμ Se μ e : ℝ) (hSe : Se ≠ 0) (hDμ : 1 + c_rindler_shared * μ + δ ≠ 0) (hDe : 1 + c_rindler_shared * e + δ ≠ 0) : Sμ / (1 + c_rindler_shared * μ + δ) / (Se / (1 + c_rindler_shared * e + δ)) = r₂ ↔ δ * (Sμ - r₂ * Se) = r₂ * Se * (1 + c_rindler_shared * μ) - Sμ * (1 + c_rindler_shared * e)

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.e_mu_ratio_iff_delta_linear (δ r₂ Sμ Se μ e : ℝ) (hSμ : Sμ ≠ 0) (hDe : 1 + c_rindler_shared * e + δ ≠ 0) (hDμ : 1 + c_rindler_shared * μ + δ ≠ 0) : Se / (1 + c_rindler_shared * e + δ) / (Sμ / (1 + c_rindler_shared * μ + δ)) = r₂ ↔ δ * (Se - r₂ * Sμ) = r₂ * Sμ * (1 + c_rindler_shared * e) - Se * (1 + c_rindler_shared * μ)

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.Sτ : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.Sτ = Hqiv.Physics.shellSurface Hqiv.Physics.LeptonResonanceGlobalDetuning.m_tau

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.Sμ : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.Sμ = Hqiv.Physics.shellSurface Hqiv.Physics.LeptonResonanceGlobalDetuning.m_mu

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.Se : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.Se = Hqiv.Physics.shellSurface Hqiv.Physics.LeptonResonanceGlobalDetuning.m_e

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.τr : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.τr = ↑Hqiv.Physics.LeptonResonanceGlobalDetuning.m_tau

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.μr : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.μr = ↑Hqiv.Physics.LeptonResonanceGlobalDetuning.m_mu

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.er : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.er = ↑Hqiv.Physics.LeptonResonanceGlobalDetuning.m_e

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.shellSurface_ne_zero (m : ℕ) : shellSurface m ≠ 0

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.δNumTauMu (r₁ : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.δDenTauMu (r₁ : ℝ) : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.δDenTauMu r₁ = Hqiv.Physics.LeptonResonanceGlobalDetuning.Sμ - r₁ * Hqiv.Physics.LeptonResonanceGlobalDetuning.Sτ

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.δNumMuE (r₂ : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.δDenMuE (r₂ : ℝ) : ℝ

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.δDenMuE r₂ = Hqiv.Physics.LeptonResonanceGlobalDetuning.Se - r₂ * Hqiv.Physics.LeptonResonanceGlobalDetuning.Sμ

noncomputable def Hqiv.Physics.LeptonResonanceGlobalDetuning.singleDeltaCompatResidual (r₁ r₂ : ℝ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.kTauMuCorrected_eq_iff_delta_linear (δ r₁ : ℝ) (hDτ : rindlerDenWithDelta δ m_tau ≠ 0) (hDμ : rindlerDenWithDelta δ m_mu ≠ 0) : kTauMuCorrected δ = r₁ ↔ δ * (Sμ - r₁ * Sτ) = δNumTauMu r₁

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.kMuECorrected_eq_iff_delta_linear (δ r₂ : ℝ) (hDμ : rindlerDenWithDelta δ m_mu ≠ 0) (hDe : rindlerDenWithDelta δ m_e ≠ 0) : kMuECorrected δ = r₂ ↔ δ * (Se - r₂ * Sμ) = δNumMuE r₂

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.single_delta_both_ratios_implies_compat_aux (δ r₁ r₂ : ℝ) (h₁ : δ * (Sμ - r₁ * Sτ) = δNumTauMu r₁) (h₂ : δ * (Se - r₂ * Sμ) = δNumMuE r₂) : singleDeltaCompatResidual r₁ r₂ = 0

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.both_ratios_implies_compat_residual_zero (δ r₁ r₂ : ℝ) (hDτ : rindlerDenWithDelta δ m_tau ≠ 0) (hDμ : rindlerDenWithDelta δ m_mu ≠ 0) (hDe : rindlerDenWithDelta δ m_e ≠ 0) (hkm : kTauMuCorrected δ = r₁) (hke : kMuECorrected δ = r₂) : singleDeltaCompatResidual r₁ r₂ = 0

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.necessary_compat_of_single_delta (δ r₁ r₂ : ℝ) (hDτ : rindlerDenWithDelta δ m_tau ≠ 0) (hDμ : rindlerDenWithDelta δ m_mu ≠ 0) (hDe : rindlerDenWithDelta δ m_e ≠ 0) (hkm : kTauMuCorrected δ = r₁) (hke : kMuECorrected δ = r₂) : singleDeltaCompatResidual r₁ r₂ = 0

theorem Hqiv.Physics.LeptonResonanceGlobalDetuning.compat_residual_eq_zero_iff_deltaEq (r₁ r₂ : ℝ) (hden1 : Sμ - r₁ * Sτ ≠ 0) (hden2 : Se - r₂ * Sμ ≠ 0) : singleDeltaCompatResidual r₁ r₂ = 0 ↔ δNumTauMu r₁ / (Sμ - r₁ * Sτ) = δNumMuE r₂ / (Se - r₂ * Sμ)

Open problem (documentation)

def Hqiv.Physics.LeptonResonanceGlobalDetuning.OpenProblem : Prop

Equations

• Hqiv.Physics.LeptonResonanceGlobalDetuning.OpenProblem = True