annularTopologicalFloor_le_annularCost
plain-language theorem explainer
The inequality shows that the topological lower bound on annular cost for N rings with uniform charge c is respected by the summed phi-weighted ring costs. Researchers on the RS cost-covering bridge cite it when decomposing annular excess into floor plus nonnegative remainder. The term-mode proof unfolds both sides, applies Finset.sum_le_sum, and reduces each term to the per-ring bound after rewriting uniform charge.
Claim. Let $M$ be an annular mesh of $N$ rings with uniform winding number $c$. The topological floor for this configuration satisfies topological floor$(N,c) ≤ ∑ ring costs of the $N$ rings in $M$.
background
The module develops the annular J-cost framework inside Recognition Science. phiCost u is cosh((log φ)·u) − 1, which equals J(φ^u). An AnnularMesh N is a structure containing N ring samples, an integer charge c, and the axiom that every ring has winding number exactly c. annularCost is the sum of ringCost over the rings; the topological floor is the matching lower-bound function of N and c. This layer certifies the cost-covering bridge that links nonzero winding to quadratic growth via Jensen coercivity.
proof idea
The term proof unfolds annularTopologicalFloor and annularCost, then applies Finset.sum_le_sum. For each ring index n it invokes ringCost_ge_topologicalFloor on Nat.succ n.val and the ring sample, rewrites the uniform_charge hypothesis into the winding number, and closes with simpa.
why it matters
The lemma is invoked directly by annularExcess_nonneg (same module) via linarith and by annularCost_nonneg in UnifiedRH via transitivity with floor nonnegativity. It closes the required step in the annular cost-covering bridge, supporting the Jensen coercivity that forces Θ(m² log N) cost from nonzero winding. The result is consistent with the eight-tick octave and the derivation of D = 3 spatial dimensions from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.