realizedDefectAnnularExcessBounded_of_costBounded
plain-language theorem explainer
A uniform bound on annular cost for a realized defect sampled family yields a uniform bound on annular excess. Analysts refining Axiom 2 in the Recognition Science zeta-defect program cite this to isolate the regular error term after subtracting the topological floor. The proof is a direct term-mode extraction of the cost bound K followed by nonnegativity of the floor and linear arithmetic on the difference.
Claim. Let $fam$ be a realized sampled family of annular meshes attached to a defect sensor. If there exists $K$ such that the annular cost of each mesh satisfies $annularCost(fam.mesh N) ≤ K$ for all $N$, then there exists $K'$ such that the annular excess satisfies $annularExcess(fam.mesh N) ≤ K'$ for all $N$.
background
A DefectSampledFamily consists of a defect sensor together with a family of annular meshes whose charges match the sensor charge at every depth. RealizedDefectAnnularCostBounded asserts the existence of a uniform upper bound on annularCost across all refinements of this family. RealizedDefectAnnularExcessBounded asserts the same for annularExcess, which subtracts the nonnegative topological floor from the total cost. The module constructs these objects from the phase-sampling of a hypothetical zeta defect to replace an earlier over-strong quantification over arbitrary meshes. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost and derivedCost primitives used to define annularCost.
proof idea
The term proof obtains the witness K from the cost hypothesis, refines the goal to the excess predicate with the same K, then for arbitrary N unfolds annularExcess, invokes nonnegativity of annularTopologicalFloor, records the cost bound at that N, rewrites the charge via the family specification, and closes by linarith.
why it matters
This implication feeds the downstream equivalence realizedDefectCostBounded_iff_charge_zero_and_excessBounded, which states that a uniform cost bound on the realized family holds if and only if the sensor charge vanishes and the excess remains bounded. It therefore supplies the missing direction needed to reduce the refined Axiom 2 to a statement about regular-part error control on the canonical sampled family. The result sits inside the T5–T8 forcing chain by ensuring that cost bounds on phase-sampled meshes remain compatible with the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.