`convention_layer`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.QuarkCoordinateReconciliation
domain: Physics
line: 105 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.QuarkCoordinateReconciliation on GitHub at line 105.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 102  deriving Repr, DecidableEq
 103
 104/-- Formal assignment of conventions to layers -/
 105def convention_layer : Convention → ModelLayer
 106  | .IntegerRung   => .Core
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.