realizedDefectAnnularExcessBounded_of_costBounded
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that any such uniform cost bound exists.
- Does not apply to arbitrary annular meshes outside the realized sampled family.
- Does not address the case of nonzero sensor charge.
- Does not quantify the size of the excess bound relative to K.
Lean usage
theorem use_site (fam : DefectSampledFamily) (h : RealizedDefectAnnularCostBounded fam) : RealizedDefectAnnularExcessBounded fam := realizedDefectAnnularExcessBounded_of_costBounded fam hformal statement (Lean)
254theorem realizedDefectAnnularExcessBounded_of_costBounded
255 (fam : DefectSampledFamily)
256 (hcost : RealizedDefectAnnularCostBounded fam) :
257 RealizedDefectAnnularExcessBounded fam := by
proof body
Term-mode proof.
258 obtain ⟨K, hK⟩ := hcost
259 refine ⟨K, ?_⟩
260 intro N
261 unfold annularExcess
262 have hfloor : 0 ≤ annularTopologicalFloor N (fam.sensor.charge) :=
263 annularTopologicalFloor_nonneg N fam.sensor.charge
264 have hcostN : annularCost (fam.mesh N) ≤ K := hK N
265 rw [fam.charge_spec N]
266 linarith
267
268/-- If the sensor charge is zero, then bounded excess is equivalent to bounded
269total cost because the topological floor vanishes identically. -/