`honestPhaseFamily_charge_zero_of_costBounded`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge
domain: NumberTheory
line: 219 · 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 219.

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

 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. -/
 219theorem honestPhaseFamily_charge_zero_of_costBounded
 220    (zfd : ZetaPhaseFamilyData)
 221    (hcost : RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily)) :
 222    zfd.sensor.charge = 0 := by
 223  have hzero :=
 224    (realizedDefectCostBounded_iff_charge_zero_and_excessBounded
 225      (zfd.phaseFamily.toSampledFamily)).mp hcost
 226  simpa [DefectPhaseFamily.toSampledFamily, zfd.family_sensor] using hzero.1
 227
 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.