Global Rindler detuning (shared across resonance ladders)

This module packages the scalar shift δ in the denominator 1 + (γ/2)·m + δ used for δ-corrected detuned shell surfaces and a global hypothesis λ · obs reused on every ladder that shares the same stars-and-bars numerator (m+1)(m+2).

Used by:

• LeptonResonanceGlobalDetuning (charged leptons),
• QuarkLadderGlobalDetuning (internal quark steps),
• HarmonicLadderGlobalDetuning (link to the same shell index m as phi_of_shell).

Identification: GlobalDetuningHypothesis.fromLapseScalars sets obs := Φ + φ·t, i.e. the increment of HQVM_lapse above 1 (same combination as in the metric story). This is pure algebra in Lean — no claim that a particular observer datum equals a PDG ratio.

δ-corrected surfaces and geometric steps

noncomputable def Hqiv.Physics.rindlerDenWithDelta (δ : ℝ) (m : ℕ) : ℝ

Equations

• Hqiv.Physics.rindlerDenWithDelta δ m = 1 + Hqiv.Physics.c_rindler_shared * ↑m + δ

theorem Hqiv.Physics.rindlerDenWithDelta_eq_rindler_plus_delta (δ : ℝ) (m : ℕ) : rindlerDenWithDelta δ m = rindlerDetuningShared ↑m + δ

theorem Hqiv.Physics.rindlerDenWithDelta_zero (m : ℕ) : rindlerDenWithDelta 0 m = rindlerDetuningShared ↑m

noncomputable def Hqiv.Physics.effCorrected (δ : ℝ) (m : ℕ) : ℝ

Equations

• Hqiv.Physics.effCorrected δ m = Hqiv.Physics.shellSurface m / Hqiv.Physics.rindlerDenWithDelta δ m

def Hqiv.Physics.RindlerDenDeltaPos (δ : ℝ) (m : ℕ) : Prop

Equations

• Hqiv.Physics.RindlerDenDeltaPos δ m = (0 < Hqiv.Physics.rindlerDenWithDelta δ m)

theorem Hqiv.Physics.effCorrected_pos (δ : ℝ) (m : ℕ) (h : RindlerDenDeltaPos δ m) : 0 < effCorrected δ m

theorem Hqiv.Physics.effCorrected_zero_eq_detunedShellSurface (m : ℕ) : effCorrected 0 m = detunedShellSurface m

theorem Hqiv.Physics.c_rindler_shared_eq_one_fifth : c_rindler_shared = 1 / 5

theorem Hqiv.Physics.effCorrected_succ_lt {δ : ℝ} (hδ : 0 ≤ δ) (m : ℕ) : effCorrected δ m < effCorrected δ m.succ

For nonnegative global shift δ, the δ-corrected effective surface strictly increases with shell index.

theorem Hqiv.Physics.effCorrected_lt_add_dist {δ : ℝ} (hδ : 0 ≤ δ) (m k : ℕ) : effCorrected δ m < effCorrected δ (m + k + 1)

effCorrected δ m < effCorrected δ (m + k + 1) for every k (with 0 ≤ δ).

theorem Hqiv.Physics.effCorrected_strictMono_nat {δ : ℝ} (hδ : 0 ≤ δ) {m n : ℕ} (hmn : m < n) : effCorrected δ m < effCorrected δ n

For 0 ≤ δ and m < n, effCorrected δ is strictly monotone in the shell index.

theorem Hqiv.Physics.effCorrected_lt_of_lt_delta {δ1 δ2 : ℝ} (m : ℕ) (hδ : δ1 < δ2) (h1 : RindlerDenDeltaPos δ1 m) (h2 : RindlerDenDeltaPos δ2 m) : effCorrected δ2 m < effCorrected δ1 m

At fixed shell m, larger additive shift δ lowers effCorrected (larger denominator).

noncomputable def Hqiv.Physics.geometricResonanceStepCorrected (δ : ℝ) (m_from m_to : ℕ) : ℝ

Corrected analogue of geometricResonanceStep (FanoResonance).

Equations

• Hqiv.Physics.geometricResonanceStepCorrected δ m_from m_to = Hqiv.Physics.effCorrected δ m_from / Hqiv.Physics.effCorrected δ m_to

theorem Hqiv.Physics.geometricResonanceStepCorrected_eq (δ : ℝ) (m_from m_to : ℕ) : geometricResonanceStepCorrected δ m_from m_to = effCorrected δ m_from / effCorrected δ m_to

theorem Hqiv.Physics.geometricResonanceStepCorrected_zero (m_from m_to : ℕ) : geometricResonanceStepCorrected 0 m_from m_to = geometricResonanceStep m_from m_to

Global hypothesis and unified effective surface

structure Hqiv.Physics.GlobalDetuningHypothesis : Type

• lambda : ℝ
• obs : ℝ

noncomputable def Hqiv.Physics.deltaGlobal (h : GlobalDetuningHypothesis) : ℝ

Equations

• Hqiv.Physics.deltaGlobal h = h.lambda * h.obs

noncomputable def Hqiv.Physics.deltaM (h : GlobalDetuningHypothesis) (_m : ℕ) : ℝ

Shell-independent shift δ(m) = λ · obs (placeholder; a richer model uses ℕ → ℝ).

Equations

• Hqiv.Physics.deltaM h _m = Hqiv.Physics.deltaGlobal h

noncomputable def Hqiv.Physics.effUnified (h : GlobalDetuningHypothesis) (m : ℕ) : ℝ

Equations

• Hqiv.Physics.effUnified h m = Hqiv.Physics.shellSurface m / (Hqiv.Physics.rindlerDetuningShared ↑m + Hqiv.Physics.deltaM h m)

theorem Hqiv.Physics.effUnified_eq_shell_over_det (h : GlobalDetuningHypothesis) (m : ℕ) : effUnified h m = shellSurface m / (1 + c_rindler_shared * ↑m + deltaM h m)

theorem Hqiv.Physics.deltaGlobal_eq_lambda_obs (h : GlobalDetuningHypothesis) : deltaGlobal h = h.lambda * h.obs

Cumulative rapidity budget (dynamic Rindler layer)

Small second-order correction β_cum · (φ·t) on top of deltaGlobal, using the same informational time track as timeAngle (HQVMetric). Lattice-only: no continuum chart.

noncomputable def Hqiv.Physics.phi_t_cum (φ t : ℝ) : ℝ

Cumulative rapidity budget: agrees with timeAngle φ t (φ·t).

Equations

• Hqiv.Physics.phi_t_cum φ t = φ * t

theorem Hqiv.Physics.phi_t_cum_eq_timeAngle (φ t : ℝ) : phi_t_cum φ t = timeAngle φ t

noncomputable def Hqiv.Physics.delta_auxiliary_phi_per_shell (h : GlobalDetuningHypothesis) (φ t β_cum : ℝ) : ℝ

One-line extension: global δ plus β_cum × cumulative rapidity (tightens detuning residuals).

Equations

• Hqiv.Physics.delta_auxiliary_phi_per_shell h φ t β_cum = Hqiv.Physics.deltaGlobal h + β_cum * Hqiv.Physics.phi_t_cum φ t

theorem Hqiv.Physics.delta_auxiliary_phi_per_shell_eq (h : GlobalDetuningHypothesis) (φ t β_cum : ℝ) : delta_auxiliary_phi_per_shell h φ t β_cum = deltaGlobal h + β_cum * phi_t_cum φ t

theorem Hqiv.Physics.delta_auxiliary_phi_per_shell_eq_delta_plus_beta_timeAngle (h : GlobalDetuningHypothesis) (φ t β_cum : ℝ) : delta_auxiliary_phi_per_shell h φ t β_cum = deltaGlobal h + β_cum * timeAngle φ t

noncomputable def Hqiv.Physics.rindlerDenWithDeltaRapidity (h : GlobalDetuningHypothesis) (φ t β_cum : ℝ) (m : ℕ) : ℝ

δ-corrected Rindler denominator using delta_auxiliary_phi_per_shell (includes rapidity budget).

Equations

• Hqiv.Physics.rindlerDenWithDeltaRapidity h φ t β_cum m = Hqiv.Physics.rindlerDenWithDelta (Hqiv.Physics.delta_auxiliary_phi_per_shell h φ t β_cum) m

theorem Hqiv.Physics.rindlerDenWithDeltaRapidity_eq (h : GlobalDetuningHypothesis) (φ t β_cum : ℝ) (m : ℕ) : rindlerDenWithDeltaRapidity h φ t β_cum m = 1 + c_rindler_shared * ↑m + deltaGlobal h + β_cum * phi_t_cum φ t

HQVM packaging (proved identification at the level of real scalars)

HQVM_lapse Φ φ t = 1 + Φ + φ·t and timeAngle φ t = φ·t (HQVMetric). We record the detuning λ * (Φ + φ·t) as λ times the lapse increment (N - 1).

noncomputable def Hqiv.Physics.GlobalDetuningHypothesis.fromLapseScalars (lam Φ φ t : ℝ) : GlobalDetuningHypothesis

Use obs := Φ + φ·t, i.e. HQVM_lapse Φ φ t - 1.

Equations

• Hqiv.Physics.GlobalDetuningHypothesis.fromLapseScalars lam Φ φ t = { lambda := lam, obs := Φ + φ * t }

theorem Hqiv.Physics.deltaGlobal_fromLapseScalars (lam Φ φ t : ℝ) : deltaGlobal (GlobalDetuningHypothesis.fromLapseScalars lam Φ φ t) = lam * (Φ + φ * t)

theorem Hqiv.Physics.deltaGlobal_eq_lambda_mul_lapseIncrement (lam Φ φ t : ℝ) : deltaGlobal (GlobalDetuningHypothesis.fromLapseScalars lam Φ φ t) = lam * (HQVM_lapse Φ φ t - 1)

theorem Hqiv.Physics.deltaGlobal_eq_lambda_mul_phi_plus_timeAngle (lam Φ φ t : ℝ) : deltaGlobal (GlobalDetuningHypothesis.fromLapseScalars lam Φ φ t) = lam * (Φ + timeAngle φ t)

theorem Hqiv.Physics.deltaGlobal_strictMono_in_t (lam Φ φ t1 t2 : ℝ) (h_lam : 0 < lam) (h_phi : 0 < φ) (h_t : t1 < t2) : deltaGlobal (GlobalDetuningHypothesis.fromLapseScalars lam Φ φ t1) < deltaGlobal (GlobalDetuningHypothesis.fromLapseScalars lam Φ φ t2)

δ_global = λ·(Φ + φ·t) is strictly increasing in t for λ > 0, φ > 0.

theorem Hqiv.Physics.physics_identification_global_detuning (lam Φ φ t : ℝ) : deltaGlobal (GlobalDetuningHypothesis.fromLapseScalars lam Φ φ t) = lam * (HQVM_lapse Φ φ t - 1)

Deprecated name: earlier stub; use deltaGlobal_eq_lambda_mul_lapseIncrement / fromLapseScalars.