pith. machine review for the scientific record. sign in
def definition def or abbrev high

RealizedDefectAnnularExcessBounded

show as:
view Lean formalization →

The definition states that annular excess for a realized sampled family of annular meshes remains uniformly bounded under arbitrary mesh refinement. Researchers working on zeta defect cost bounds cite it to separate the topological floor from the regular remainder in the defect-cost accounting. The declaration is introduced directly as an existential statement over a uniform real bound K applying to all refinement depths N.

claimFor a realized sampled family $fam$ of annular meshes attached to a defect sensor, there exists $K$ in the reals such that for every natural number $N$, the annular excess of the mesh at depth $N$ satisfies annularExcess$(fam.mesh N) ≤ K$.

background

The DefectSampledTrace module constructs realized annular meshes from phase-sampling of the inverse zeta function near a hypothetical defect. A DefectSampledFamily is a structure consisting of a defect sensor, a family of annular meshes indexed by refinement depth N, and the requirement that each mesh charge equals the sensor charge. This layer addresses the refined Axiom 2 after Axiom 1 is eliminated: the cost bound must be established for the canonical sampled family rather than for every possible mesh with the given charge.

proof idea

This declaration is a direct definition expressing uniform boundedness of annular excess over the refinement parameter N for a given sampled family.

why it matters in Recognition Science

This definition is invoked by canonicalDefectSampledFamily_excess_bounded and by honestPhase_routeC_bottleneck, which records the Route C bottleneck for zeta phase data. It supplies the quantitative input needed to prove bounded annular excess in the defect-cost story, separating the topological floor from the regular remainder. It touches the open question of upgrading bounded excess to zero charge for admissibility.

scope and limits

formal statement (Lean)

 125def RealizedDefectAnnularExcessBounded (fam : DefectSampledFamily) : Prop :=

proof body

Definition body.

 126  ∃ K : ℝ, ∀ N : ℕ, annularExcess (fam.mesh N) ≤ K
 127
 128/-! ### §3a. Ring-level regular-part error control -/
 129
 130/-- A ring-level regular-part error package for a realized sampled family.
 131
 132For each depth `N` and ring `n`, the sampled ring cost is bounded by the
 133topological floor for its charge sector plus an error term coming from the
 134regular factor in the local meromorphic factorization. The total error across
 135all rings is uniformly bounded in `N`.
 136
 137This is the exact quantitative input needed to prove bounded annular excess. -/

used by (11)

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

depends on (22)

Lean names referenced from this declaration's body.