pith. machine review for the scientific record. sign in
def definition def or abbrev

default

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  46def default : BlockOffsets :=

proof body

Definition body.

  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}. -/

used by (20)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.