def definition def or abbrev

`annularTopologicalFloor`

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

formal statement (Lean)

 464noncomputable def annularTopologicalFloor (N : ℕ) (m : ℤ) : ℝ :=

proof body

Definition body.

 465  ∑ n : Fin N, topologicalFloor (n.val + 1) m
 466
 467/-- The excess cost above the topological floor for an annular mesh. -/

used by (16)

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

annularExcess in IndisputableMonolith.NumberTheory.AnnularCost decl_use
annularTopologicalFloor_le_annularCost in IndisputableMonolith.NumberTheory.AnnularCost decl_use
annularTopologicalFloor_nonneg in IndisputableMonolith.NumberTheory.AnnularCost decl_use
annularTopologicalFloor_one_pos_of_charge_ne_zero in IndisputableMonolith.NumberTheory.AnnularCost decl_use
annularTopologicalFloor_zero in IndisputableMonolith.NumberTheory.AnnularCost decl_use
carrier_defect_budget_contradiction in IndisputableMonolith.NumberTheory.CarrierBudgetComparison decl_use
defect_floor_exceeds_any_bound in IndisputableMonolith.NumberTheory.CarrierBudgetComparison decl_use
DefectTopologicalFloorCovered in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
defect_topological_floor_unbounded in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
uniformChargeMesh_excess_zero in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
realizedDefectAnnularExcessBounded_of_costBounded in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
realizedDefectCostBounded_of_charge_zero_and_excessBounded in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
zetaDerivedPhaseFamily_excess_zero in IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge decl_use
sampledTraceToAnnularTrace_excess_zero in IndisputableMonolith.NumberTheory.SampledTrace decl_use
not_costDivergent_of_charge_zero in IndisputableMonolith.Unification.UnifiedRH decl_use

depends on (4)

Lean names referenced from this declaration's body.

cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
topologicalFloor in IndisputableMonolith.NumberTheory.AnnularCost decl_use