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

MockModularDefect

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)

 111structure MockModularDefect where
 112  /-- The defect magnitude (how far from perfect modularity) -/
 113  magnitude : ℝ
 114  /-- Non-negative -/
 115  magnitude_nonneg : 0 ≤ magnitude
 116  /-- Zero iff perfectly modular -/
 117  zero_iff_modular : magnitude = 0 ↔ True  -- Simplified; full version needs modular form definition
 118
 119/-- The Phantom Balance: RS analog of the mock modular defect.
 120
 121    When an 8-tick window is partially filled, the unfilled portion
 122    must compensate. The magnitude of this compensation requirement
 123    is the Phantom Balance. -/

used by (2)

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

depends on (13)

Lean names referenced from this declaration's body.