defectSampledFamily_unbounded
plain-language theorem explainer
Nonzero charge on a defect sensor forces the annular costs of its realized sampled family of meshes to diverge to infinity. Researchers refining Axiom 2 in the Recognition Science zeta analysis cite this to obtain the contradiction with any assumed uniform cost bound. The proof is a direct specialization of the general defect_cost_unbounded lemma to the meshes of one fixed family, using the charge_spec to match windings on each ring.
Claim. Let fam be a DefectSampledFamily. If the charge of fam.sensor is nonzero, then for every real number $B$ there exists a natural number $N$ such that $B < $ annularCost(fam.mesh $N$).
background
A DefectSampledFamily packages a DefectSensor with a map sending each natural number $N$ to an AnnularMesh $N$ whose charge equals the sensor charge; the construction comes from phase-sampling the inverse zeta function near a hypothetical defect rather than from arbitrary synthetic meshes. The module supplies the realized family needed once Axiom 1 is eliminated, so that the remaining bottleneck (refined Axiom 2) can be stated for the canonical sampled family instead of for every possible mesh with the given charge. AnnularCost is the total cost on an annular mesh, built from the J-cost of the underlying recognition events.
proof idea
Introduce the arbitrary bound $B$. Obtain $N$ and the witness $hN$ by applying defect_cost_unbounded to the sensor and the nonzero-charge hypothesis. Construct the auxiliary fact that every ring of fam.mesh $N$ carries exactly the sensor charge, using the uniform_charge property of the mesh together with the family's charge_spec. Apply $hN$ to the concrete mesh and the verified charge equality.
why it matters
The result feeds directly into not_realizedDefectAnnularCostBounded, which derives the inconsistency of the deprecated axiom defect_annular_cost_bounded, and into defect_cost_exceeds_carrier_budget and the collapse-boundary statement in UnifiedRH. It supplies the machine-checked bridge for the refined Axiom 2 by showing that any realized sampled family with nonzero charge must have unbounded annular cost, consistent with the divergence forced by the Recognition Composition Law and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.