ringCost_le_topologicalFloor_add_linear_quadratic_error
plain-language theorem explainer
The theorem supplies a perturbative upper bound showing that ring cost on an annular sample stays at most the topological floor plus explicit linear and quadratic sums in the deviations, whenever each phase increment deviates from the uniform winding value by at most 1 in log-φ units. Number theorists formalizing the Recognition Science cost-covering bridge cite it when bounding excess in sampled defect traces. The proof applies the local quadratic upper bound for phiCost to each increment, sums the resulting inequalities, and rewrites the base
Claim. Let $n$ be a positive integer and let $s$ be an annular ring sample consisting of $8n$ real increments summing to $-2π$ times its winding integer $m$. Set $u = -2π m/(8n)$. If every deviation satisfies $|(log φ)·(increment_j - u)| ≤ 1$, then the ring cost (sum of phiCost over the increments) satisfies ringCost(s) ≤ topologicalFloor(n, m) + phiCostLinearCoeff(|u|) · ∑|increment_j - u| + phiCostQuadraticCoeff(|u|) · ∑(increment_j - u)^2.
background
The AnnularCost module develops the φ-weighted cost function and annular sampling machinery for the RS topological cost-covering bridge. phiCost u is defined as cosh((log φ)·u) − 1, equivalently J(φ^u) where J is the uniqueness function from the forcing chain. An AnnularRingSample n is the structure whose increments field supplies 8n real numbers summing to −2π·winding and whose winding field records the net topological charge.
proof idea
The proof sets u to the mean increment −(2π winding)/(8n). For each j it invokes phiCost_add_le_phiCost_add_linear_quadratic (with the smallness hypothesis on the deviation) to bound phiCost(increment_j) by phiCost(u) plus the linear and quadratic error terms. Summing over the Fin (8n) indices, the constant part becomes (8n)·phiCost(u) which is rewritten as topologicalFloor n winding by definition, while the error sums are collected with the respective coefficients via Finset.sum_add_distrib and sum_const.
why it matters
This bound supplies the quantitative control needed for the RingRegularErrorBound structure and the ringRegularErrorBound_of_ringPerturbationControl definition in DefectSampledTrace, which together prove bounded annular excess. It completes one concrete step in the annular topological floor and excess decomposition layer described in the module documentation. Within the Recognition Science framework it supports the cost-covering argument that links the eight-tick octave and J-uniqueness to concrete mass and charge spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.