RealizedDefectAnnularExcessBounded
plain-language theorem explainer
The definition packages the predicate that annular excess for a realized sampled family of annular meshes stays below some fixed real K no matter how fine the mesh depth N becomes. Number theorists working on zeta-defect cost bounds cite it when separating topological floor from regular-part remainder in the refined Axiom 2 argument. It is introduced directly as an existential statement over K to serve as the target property in several downstream boundedness lemmas.
Claim. Let $fam$ be a realized sampled family of annular meshes attached to a defect sensor. The family has bounded annular excess when there exists $K ∈ ℝ$ such that for every natural number $N$ the annular excess of the mesh at depth $N$ satisfies annularExcess$(fam.mesh(N)) ≤ K$.
background
The Defect Sampled Trace module constructs realized annular meshes from the phase-sampling construction for a hypothetical zeta defect. After Axiom 1 is eliminated the remaining bottleneck is Axiom 2; the module therefore replaces quantification over all charge-correct AnnularMesh values with the concrete canonical sampled family that arises from the phase of ζ⁻¹ near the defect. A DefectSampledFamily is the structure carrying a DefectSensor, a mesh function indexed by depth N, and the charge-specification axiom that each mesh inherits the sensor charge.
proof idea
This is a definition that directly encodes the uniform bound on annular excess. Downstream lemmas such as realizedDefectAnnularExcessBounded_of_ringRegularErrorBound obtain the predicate by extracting the total_error_bounded field of a RingRegularErrorBound hypothesis and re-packaging it as the required existential K.
why it matters
The definition supplies the bounded-excess predicate used in honestPhase_routeC_bottleneck, which records that honest zeta phase data already satisfies bounded excess while bounded total cost is equivalent to zero charge. It is also invoked in carrier_cost_bounded_of_shared_pair and in the canonicalDefectSampledFamily_excess_bounded theorem. Within the Recognition framework it supplies the analytic control step that follows the eight-tick octave and phi-ladder constructions, leaving open the upgrade from excess bound to charge-zero admissibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.