@[reducible, inline]

abbrev Hqiv.Physics.FanoVertex : Type

Fano-plane vertex index: 0 for EM/lepton axis, 1..6 for quark lines.

Equations

• Hqiv.Physics.FanoVertex = Fin 7

inductive Hqiv.Physics.LadderDirection : Type

Resonance ladder orientation on a given vertex.

• internal : LadderDirection
• reverse : LadderDirection

instance Hqiv.Physics.instDecidableEqLadderDirection : DecidableEq LadderDirection

Equations

• Hqiv.Physics.instDecidableEqLadderDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Hqiv.Physics.instReprLadderDirection : Repr LadderDirection

Equations

• Hqiv.Physics.instReprLadderDirection = { reprPrec := Hqiv.Physics.instReprLadderDirection.repr }

def Hqiv.Physics.instReprLadderDirection.repr : LadderDirection → ℕ → Std.Format

Equations

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

structure Hqiv.Physics.ResonanceAxis : Type

Shared metadata for a resonance axis on one Fano vertex.

• vertex : FanoVertex
• anchorShell : ℕ
• direction : LadderDirection
• hyperchargeSign : ℤ

  Integer hypercharge sign witness (+1 or -1).

@[reducible, inline]

abbrev Hqiv.Physics.ResonanceGeneration : Type

Generation index (.two heavy, .one middle, .zero light).

Equations

• Hqiv.Physics.ResonanceGeneration = Fin 3

def Hqiv.Physics.shellSurface (m : ℕ) : ℝ

Discrete shell surface leading term shared by lepton/quark ladders.

Equations

• Hqiv.Physics.shellSurface m = (↑m + 1) * (↑m + 2)

noncomputable def Hqiv.Physics.c_rindler_shared : ℝ

Shared Rindler detuning coefficient (c = γ/2).

Equations

• Hqiv.Physics.c_rindler_shared = Hqiv.gamma_HQIV / 2

noncomputable def Hqiv.Physics.rindlerDetuningShared (x : ℝ) : ℝ

Rindler detuning factor used by resonance surfaces.

Equations

• Hqiv.Physics.rindlerDetuningShared x = 1 + Hqiv.Physics.c_rindler_shared * x

noncomputable def Hqiv.Physics.detunedShellSurface (m : ℕ) : ℝ

Detuned surface evaluated on the shell index itself.

Equations

• Hqiv.Physics.detunedShellSurface m = Hqiv.Physics.shellSurface m / Hqiv.Physics.rindlerDetuningShared ↑m

theorem Hqiv.Physics.detunedShellSurface_pos (m : ℕ) : 0 < detunedShellSurface m

Positivity of the detuned shell surface.

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

Resonance step as a quotient of detuned shell surfaces.

Equations

• Hqiv.Physics.geometricResonanceStep m_from m_to = Hqiv.Physics.detunedShellSurface m_from / Hqiv.Physics.detunedShellSurface m_to

theorem Hqiv.Physics.geometricResonanceStep_pos (m_from m_to : ℕ) : 0 < geometricResonanceStep m_from m_to

Positive geometric resonance step.

def Hqiv.Physics.resonanceProductFromSteps (k21 k10 : ℝ) (gen : ResonanceGeneration) : ℝ

Generic 3-generation resonance product. k21 is the heavy→middle step, k10 is the middle→light step.

Equations

• Hqiv.Physics.resonanceProductFromSteps k21 k10 ⟨2, isLt⟩ = 1
• Hqiv.Physics.resonanceProductFromSteps k21 k10 ⟨1, isLt⟩ = k21
• Hqiv.Physics.resonanceProductFromSteps k21 k10 ⟨0, isLt⟩ = k21 * k10

theorem Hqiv.Physics.exactly_three_generations_fano : ¬∃ (fourthGen : ResonanceGeneration), fourthGen ≠ ⟨0, ⋯⟩ ∧ fourthGen ≠ ⟨1, ⋯⟩ ∧ fourthGen ≠ ⟨2, ⋯⟩

Any Fin-3 based axis has exactly three generations and no fourth.

def Hqiv.Physics.leptonAxis (anchorShell : ℕ) : ResonanceAxis

Canonical lepton (EM) axis metadata.

Equations

• Hqiv.Physics.leptonAxis anchorShell = { vertex := ⟨0, Hqiv.Physics.leptonAxis._proof_1⟩, anchorShell := anchorShell, direction := Hqiv.Physics.LadderDirection.reverse, hyperchargeSign := 1 }

def Hqiv.Physics.upQuarkAxis (vertex : Fin 3) (anchorShell : ℕ) : ResonanceAxis

Canonical up-type quark axis metadata.

Equations

• Hqiv.Physics.upQuarkAxis vertex anchorShell = { vertex := ⟨↑vertex + 1, ⋯⟩, anchorShell := anchorShell, direction := Hqiv.Physics.LadderDirection.internal, hyperchargeSign := 1 }

def Hqiv.Physics.downQuarkAxis (vertex : Fin 3) (anchorShell : ℕ) : ResonanceAxis

Canonical down-type quark axis metadata.

Equations

• Hqiv.Physics.downQuarkAxis vertex anchorShell = { vertex := ⟨↑vertex + 4, ⋯⟩, anchorShell := anchorShell, direction := Hqiv.Physics.LadderDirection.internal, hyperchargeSign := -1 }