theorem proved term proof

`canonicalDefectSampledFamily_excess_bounded`

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

formal statement (Lean)

 438theorem canonicalDefectSampledFamily_excess_bounded (sensor : DefectSensor)
 439    (hm : sensor.charge ≠ 0) :
 440    RealizedDefectAnnularExcessBounded
 441      (canonicalDefectSampledFamily sensor hm) := by

proof body

Term-mode proof.

 442  exact realizedDefectAnnularExcessBounded_of_ringRegularErrorBound _
 443    (canonicalDefectSampledFamily_ringRegularErrorBound sensor hm)
 444
 445/-- Nonzero charge forces the realized sampled family cost to exceed any bound.
 446
 447This is just `defect_cost_unbounded` specialized to the meshes of one realized
 448family. The theorem is completely unconditional. -/

depends on (22)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
forces in IndisputableMonolith.Foundation.MagnitudeOfMismatch decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
defect_cost_unbounded in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
canonicalDefectSampledFamily in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
canonicalDefectSampledFamily_ringRegularErrorBound in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
RealizedDefectAnnularExcessBounded in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
realizedDefectAnnularExcessBounded_of_ringRegularErrorBound in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use