def definition def or abbrev

`honestPhaseFamily_perturbationWitness`

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

formal statement (Lean)

 192noncomputable def honestPhaseFamily_perturbationWitness
 193    (zfd : ZetaPhaseFamilyData) :
 194    DefectPhasePerturbationWitness zfd.phaseFamily :=

proof body

Definition body.

 195  zfd.perturbationWitness
 196
 197/-- The sampled family attached to honest phase data has zero annular excess on
 198every mesh depth. -/

depends on (5)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
DefectPhasePerturbationWitness in IndisputableMonolith.NumberTheory.MeromorphicCircleOrder decl_use
ZetaPhaseFamilyData in IndisputableMonolith.NumberTheory.MeromorphicCircleOrder decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use