theorem
proved
core_uses_integer_rungs
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.QuarkCoordinateReconciliation on GitHub at line 110.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
107 | .QuarterLadder => .Hypothesis
108
109/-- The core model uses integer rungs -/
110theorem core_uses_integer_rungs :
111 convention_layer .IntegerRung = .Core := rfl
112
113/-- The quarter-ladder is a hypothesis, not core -/
114theorem quarter_ladder_is_hypothesis :
115 convention_layer .QuarterLadder = .Hypothesis := rfl
116
117/-! ## Key Definitions -/
118
119/-- The φ-ladder step for the quarter-ladder convention -/
120noncomputable def quarter_step : ℝ := phi ^ (1/4 : ℝ)
121
122/-- Convert quarter-ladder rung to equivalent real position on universal ladder -/
123def quarter_to_real (q : ℚ) : ℚ := q
124
125/-- Convert quarter-ladder position to the nearest integer rung -/
126def quarter_to_nearest_int (q : ℚ) : ℤ := ⌊(q + 1/2)⌋
127
128/-! ## Core Integer Rung Positions (from Masses/Anchor.lean) -/
129
130/-- Core model integer rungs for up-type quarks -/
131structure CoreUpQuarkRungs where
132 u : ℤ := 4
133 c : ℤ := 15 -- 4 + τ(1) = 4 + 11
134 t : ℤ := 21 -- 4 + τ(2) = 4 + 17
135
136/-- Core model integer rungs for down-type quarks -/
137structure CoreDownQuarkRungs where
138 d : ℤ := 4
139 s : ℤ := 15 -- 4 + τ(1) = 4 + 11
140 b : ℤ := 21 -- 4 + τ(2) = 4 + 17