`honestPhaseFamily_cost_bounded_iff_charge_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge
domain: NumberTheory
line: 231 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge on GitHub at line 231.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 228/-- For the current honest phase package, bounded total cost is equivalent to
 229zero charge. The perturbation/excess part is already proved; only the bounded-cost
 230upgrade remains genuinely open. -/
 231theorem honestPhaseFamily_cost_bounded_iff_charge_zero
 232    (zfd : ZetaPhaseFamilyData) :
 233    RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily) ↔
 234      zfd.sensor.charge = 0 := by
 235  constructor
 236  · intro hcost
 237    exact honestPhaseFamily_charge_zero_of_costBounded zfd hcost
 238  · intro hzero
 239    have hzero' : (zfd.phaseFamily.toSampledFamily).sensor.charge = 0 := by
 240      simpa [DefectPhaseFamily.toSampledFamily, zfd.family_sensor] using hzero
 241    exact realizedDefectCostBounded_of_charge_zero_and_excessBounded
 242      (zfd.phaseFamily.toSampledFamily) hzero'
 243      (honestPhaseFamily_excess_bounded zfd)
 244
 245end
 246
 247end NumberTheory
 248end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.