IndisputableMonolith.Support.RungFractions

   1import Mathlib
   2
   3/-!
   4# Fractional φ-Ladder Rungs (Convention / Reporting Seam)
   5
   6This file provides a minimal, *type-light* representation for fractional rungs on the φ‑ladder.
   7
   8Why it exists:
   9- The **core** mass model layer uses integer rungs (`ℤ`) for maximal rigidity.
  10- Some physics modules (quark masses, neutrino deep ladder refinements) explore **fractional**
  11  placements (e.g. quarter-ladder) to capture observed ratios.
  12
  13This is **not** (yet) a proof that fractional rungs are canonical. It is a *representation seam*:
  14we make the convention explicit and mechanically uniform across modules.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Support
  19namespace RungFractions
  20
  21/-- A (possibly fractional) rung on the φ‑ladder. -/
  22abbrev Rung := ℚ
  23
  24/-- Embed an integer rung into a rational rung. -/
  25@[simp] def ofInt (z : ℤ) : Rung := (z : ℚ)
  26
  27/-- The quarter‑ladder embedding: `k ↦ k/4`. -/
  28@[simp] def quarter (k : ℤ) : Rung := (k : ℚ) / 4
  29
  30/-- The half‑ladder embedding: `k ↦ k/2`. -/
  31@[simp] def half (k : ℤ) : Rung := (k : ℚ) / 2
  32
  33/-- Convert a rational rung to a real exponent (for `Real.rpow`). -/
  34@[simp] def toReal (r : Rung) : ℝ := (r : ℝ)
  35
  36theorem quarter_eq (k : ℤ) : quarter k = (k : ℚ) / 4 := rfl
  37theorem half_eq (k : ℤ) : half k = (k : ℚ) / 2 := rfl
  38
  39end RungFractions
  40end Support
  41end IndisputableMonolith
  42