pith. machine review for the scientific record. sign in
theorem proved term proof

honestPhaseFamily_excess_bounded

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)

 209theorem honestPhaseFamily_excess_bounded
 210    (zfd : ZetaPhaseFamilyData) :
 211    RealizedDefectAnnularExcessBounded (zfd.phaseFamily.toSampledFamily) := by

proof body

Term-mode proof.

 212  refine ⟨0, ?_⟩
 213  intro N
 214  rw [honestPhaseFamily_excess_zero zfd N]
 215
 216/-- If the sampled family attached to honest phase data also has bounded total
 217annular cost, then the corresponding sensor charge must vanish. This isolates
 218the remaining topological/budget upgrade needed by the analytic route. -/

used by (3)

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

depends on (11)

Lean names referenced from this declaration's body.