`honestPhaseFamily_excess_bounded`

proved

show as: view math explainer →

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

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

 206has bounded annular excess. The remaining analytic gap is no longer the
 207perturbation witness itself, but upgrading this excess control to the charge-zero
 208conclusion required by `AnalyticTrace`. -/
 209theorem honestPhaseFamily_excess_bounded
 210    (zfd : ZetaPhaseFamilyData) :
 211    RealizedDefectAnnularExcessBounded (zfd.phaseFamily.toSampledFamily) := by
 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. -/
 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

papers checked against this theorem

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