theorem proved tactic proof

`defect_bounded_impossible`

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

formal statement (Lean)

 862theorem defect_bounded_impossible (sensor : DefectSensor)
 863    (hm : sensor.charge ≠ 0)
 864    (hbound : RealizedDefectAnnularCostBounded
 865      (canonicalDefectSampledFamily sensor hm)) :
 866    False := by

proof body

Tactic-mode proof.

 867  let fam := canonicalDefectSampledFamily sensor hm
 868  have hfam : fam.sensor.charge ≠ 0 := by
 869    simpa [fam, canonicalDefectSampledFamily_sensor] using hm
 870  exact not_realizedDefectAnnularCostBounded fam hfam hbound
 871
 872/-! ### §8. The defect sensor for ζ -/
 873
 874/-- Given a hypothetical zero of ζ at s = ρ with Re(ρ) > 1/2
 875    and multiplicity m ≥ 1, construct the DefectSensor. -/

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
canonicalDefectSampledFamily in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
canonicalDefectSampledFamily_sensor in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
not_realizedDefectAnnularCostBounded in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
RealizedDefectAnnularCostBounded in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use