argument_principle_sampling
Any DefectSensor admits, for every natural number N, an AnnularMesh N whose charge equals the sensor charge exactly. Researchers instantiating the Euler product of zeta into the Recognition Science annular cost framework would cite it when linking meromorphic sampling to the abstract carrier/sensor layer. The proof is a direct term construction that applies uniformChargeMesh to the sensor charge and closes by reflexivity.
claimFor any defect sensor with charge $m$, and for every natural number $N$, there exists an annular mesh of level $N$ such that the mesh charge equals $m$.
background
The EulerInstantiation module instantiates the abstract RS cost structure from AnnularCost and CostCoveringBridge by means of the Euler product of the zeta function. Core objects include PrimeSum as the real part of the prime zeta function, HilbertSchmidtNorm as the squared HS norm of the associated operator, carrierLogSeries, and carrierDerivBound. AnnularMesh and DefectSensor belong to the Layer 1 abstract cost framework; the former carries a charge (winding) and the latter supplies a sensor charge that the mesh must match. Upstream results include the Defect toy functional from CPM.LNALBridge, the cost induced by MultiplicativeRecognizerL4, and the J-cost of recognition events from ObserverForcing.
proof idea
The proof is a one-line term-mode wrapper. For each N the witness is constructed by applying uniformChargeMesh N to the sensor charge; equality holds by reflexivity.
why it matters in Recognition Science
The theorem supplies the concrete sampling step that lets the Euler product satisfy the EulerCarrier and RegularCarrier interfaces, thereby enabling the cost-covering axiom and the conditional RH route described in the module documentation. It is explicitly distinguished from RH itself and from the deprecated bounded-cost hypothesis; it remains available for the ontological exclusion path via UnifiedRH. The result touches the open formalization gap for contour integration in Mathlib.
scope and limits
- Does not prove the Riemann Hypothesis.
- Does not supply contour integration for the argument principle.
- Does not bound annular cost for nonzero charge.
- Does not rely on the deprecated bounded-cost axiom.
formal statement (Lean)
786theorem argument_principle_sampling (sensor : DefectSensor) :
787 ∀ N : ℕ, ∃ mesh : AnnularMesh N,
788 mesh.charge = sensor.charge :=
proof body
Term-mode proof.
789 fun N => ⟨uniformChargeMesh N sensor.charge, rfl⟩
790
791/- **Axiom 2 (Defect Annular Cost Bounded)** — DEPRECATED RH-equivalent boundary.
792
793⚠ **DEPRECATED.** This axiom is logically inconsistent with the proved
794`not_realizedDefectAnnularCostBounded` (which shows unbounded cost for any
795nonzero-charge sensor). It remains in the codebase as the formal boundary
796marker for the legacy analytic route.
797
798**Preferred routes:**
799- **Ontology**: `UnifiedRH.ontological_exclusion` (admissibility architecture)
800- **Analytic**: `AnalyticTrace.ZeroFreeCriterion` (direct zero-free target)
801
802**RH-equivalence.** Asserting bounded cost for nonzero charge immediately
803contradicts `defectSampledFamily_unbounded`, yielding `False` = RH.
804
805**Why not directly provable.** The topological floor diverges
806as `Θ(m² log N)` for nonzero charge `m` (proved:
807`defect_topological_floor_unbounded`). Since `annularCost = floor + excess`
808and the floor diverges, total cost diverges even when excess is bounded.
809This axiom is RH stated in cost language; it forces charge = 0 by
810contradiction. -/
811/-- Deprecated bounded-cost hypothesis for the legacy analytic route.
812
813This is a proposition, not an axiom. The theorem below proves that any witness
814of this proposition contradicts the already-proved unboundedness theorem. -/