class definition def or abbrev

`BlockOffsets`

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

formal statement (Lean)

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

used by (5)

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

bandEnergy in IndisputableMonolith.Chemistry.PeriodicTable decl_use
bandMultiplier in IndisputableMonolith.Chemistry.PeriodicTable decl_use
blockFactor in IndisputableMonolith.Chemistry.PeriodicTable decl_use
default in IndisputableMonolith.Chemistry.PeriodicTable decl_use
railFactor in IndisputableMonolith.Chemistry.PeriodicTable decl_use

depends on (1)

Lean names referenced from this declaration's body.

Block in IndisputableMonolith.Chemistry.PeriodicTable decl_use