BlockOffsets

formal source

  38inductive Block | s | p | d | f deriving DecidableEq, Repr
  39
  40/- Fixed φ‑packing offsets for blocks (no per‑element tuning). -/
  41class BlockOffsets where
  42  offset : Block → ℤ
  43
  44namespace BlockOffsets
  45/- Default φ‑packing offsets (audit subject to change): s=0, p=1, d=2, f=3. -/
  46def default : BlockOffsets :=
  47  { offset := fun b =>
  48      match b with
  49      | Block.s => 0
  50      | Block.p => 1
  51      | Block.d => 2
  52      | Block.f => 3 }
  53end BlockOffsets
  54
  55noncomputable section
  56
  57/-- Default instance: s=0, p=1, d=2, f=3 (no per‑element tuning). -/
  58instance : BlockOffsets := BlockOffsets.default
  59
  60/- Dimensionless shell rail multiplier (E_n/E_coh) at rail n: φ^{2n}. -/
  61def railFactor (n : ℤ) : ℝ :=
  62  Real.rpow IndisputableMonolith.Constants.phi ((2 : ℝ) * (n : ℝ))
  63
  64/- Predicted (dimensionless) band multiplier for block `b` on rail `n`.
  65     Uses fixed φ‑packing offsets from `BlockOffsets`. -/
  66def blockFactor (n : ℤ) (b : Block) [B : BlockOffsets] : ℝ :=
  67  let exp : ℝ := (2 : ℝ) * (n : ℝ) + (B.offset b : ℝ)
  68  Real.rpow IndisputableMonolith.Constants.phi exp
  69
  70/-- Rail energy (dimensionful): E_n = E_coh · φ^{2n}. -/
  71def railEnergy (n : ℤ) : ℝ :=