RealizedDefectAnnularCostBounded
The definition states that for any realized sampled family of annular meshes attached to a defect sensor there exists a uniform real bound K such that the annular cost at every refinement depth N stays at most K. Analysts refining the zeta-defect statement in Recognition Science cite it to replace an overly strong universal quantification over all admissible meshes with a concrete phase-sampled family. The declaration is a direct existential encoding of boundedness applied to the family mesh function.
claimLet $fam$ be a realized sampled family of annular meshes attached to one defect sensor. Then there exists a real number $K$ such that for every natural number $N$, the annular cost of the mesh at level $N$ satisfies annularCost$(fam.mesh(N)) ≤ K$.
background
The Defect Sampled Trace module addresses the remaining bottleneck after Axiom 1 is eliminated: Axiom 2 must now bound cost for the canonical sampled family arising from the phase of ζ^{-1} near a hypothetical defect, rather than for every admissible AnnularMesh. A DefectSampledFamily packages a defect sensor, a mesh map from ℕ to AnnularMesh N, and the charge specification that each mesh carries exactly the sensor charge; it is obtained by converting a DefectPhaseFamily via defectAnnularMesh. Upstream, the annular cost is the derivedCost of a multiplicative recognizer comparator, while the defect functional equals J(x) for positive x.
proof idea
This is a definition, not a derived theorem. It directly encodes the boundedness property as an existential quantifier over K applied to the annularCost of each mesh N in the family.
why it matters in Recognition Science
The definition supplies the cost-bounded hypothesis required by the HonestPhaseCostBridge structure, which in turn feeds charge_zero_of_honest_phase_of_costBridge and the honestPhase_routeC_bottleneck theorem. It refines the defect-cost story by restricting attention to the realizable sampled family, supporting the transition from bounded excess to zero charge. In the Recognition framework it closes the gap between the abstract annular coercivity statement and the concrete phase-sampling construction for the zeta defect.
scope and limits
- Does not assert bounded cost for arbitrary AnnularMesh families.
- Does not supply an explicit numerical value for the bound K.
- Does not prove that any particular family satisfies the property.
- Does not address the separate excess component of the cost.
formal statement (Lean)
118def RealizedDefectAnnularCostBounded (fam : DefectSampledFamily) : Prop :=
proof body
Definition body.
119 ∃ K : ℝ, ∀ N : ℕ, annularCost (fam.mesh N) ≤ K
120
121/-- The annular excess of a realized sampled family is bounded independently of
122mesh refinement. This is the quantitatively plausible part of the defect-cost
123story: after removing the topological floor, only the regular remainder should
124need analytic control. -/
used by (14)
-
charge_zero_of_honest_phase_of_costBridge -
HonestPhaseCostBridge -
honestPhase_routeC_bottleneck -
carrier_cost_bounded_of_shared_pair -
carrier_defect_comparison_rh -
defect_cost_unbounded_of_shared_pair -
not_realizedDefectAnnularCostBounded -
realizedDefectAnnularExcessBounded_of_costBounded -
realizedDefectCostBounded_iff_charge_zero_and_excessBounded -
realizedDefectCostBounded_of_charge_zero_and_excessBounded -
defect_bounded_impossible -
HonestPhaseAdmissible -
honestPhaseFamily_charge_zero_of_costBounded -
honestPhaseFamily_cost_bounded_iff_charge_zero