ModelLayer

formal source

  89/-! ## Formal Layer Definitions -/
  90
  91/-- Model layer enumeration -/
  92inductive ModelLayer
  93  | Core         -- Parameter-free derived from geometry
  94  | Hypothesis   -- Phenomenological, not yet derived
  95  | Empirical    -- Directly from experiment
  96  deriving Repr, DecidableEq
  97
  98/-- Convention identifier -/
  99inductive Convention
 100  | IntegerRung    -- Convention A: integer rungs, sector yardsticks
 101  | QuarterLadder  -- Convention B: quarter rungs, electron mass base
 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 -/