module module

`IndisputableMonolith.NumberTheory.CostCoveringBridge`

show as: view Lean formalization →

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

generate prose now

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.AnalyticTrace module_import
IndisputableMonolith.NumberTheory.ArgumentPrincipleProved module_import
IndisputableMonolith.NumberTheory.CarrierBudgetComparison module_import
IndisputableMonolith.NumberTheory.ContourWinding module_import
IndisputableMonolith.NumberTheory.DefectSampledTrace module_import
IndisputableMonolith.NumberTheory.EulerInstantiation module_import
IndisputableMonolith.NumberTheory.MeromorphicCircleOrder module_import
IndisputableMonolith.NumberTheory.SampledTrace module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.NumberTheory.AnnularCost module_import

declarations in this module (15)

def uniformRingSample L61
def uniformChargeMesh L69
structure EulerCarrier L79
def zetaCarrier L92
structure DefectSensor L103
structure CostCoveringPackage L118
def DefectTopologicalFloorCovered L123
theorem uniformRingSample_cost_eq_topologicalFloor L129
theorem uniformChargeMesh_excess_zero L135
theorem defect_cost_unbounded L147
theorem defect_topological_floor_unbounded L195
theorem not_DefectTopologicalFloorCovered L216
theorem rh_from_cost_covering L234
theorem riemann_hypothesis_conditional L247
structure CostCoveringCert L255