argument_principle_honest
plain-language theorem explainer
The declaration establishes that any defect sensor with nonzero charge admits an annular mesh of arbitrary ring count N whose total charge matches the sensor. Analysts working the analytic route to the Riemann hypothesis cite this to replace uniform synthetic meshes with ones built from witnessed phase samples of zeta inverse. The short term proof obtains a defect phase family from the existence lemma and applies the defect annular mesh constructor.
Claim. Let $s$ be a defect sensor with charge $m$ satisfying $m ≠ 0$. For every natural number $N$, there exists an annular mesh $M$ of $N$ rings such that the charge of $M$ equals $m$.
background
In the Argument Principle Sampling module the legacy axiom requiring existence of an annular mesh with prescribed charge is replaced by a theorem. A DefectSensor encodes a hypothetical zero of zeta via the pole order of zeta inverse, recording the multiplicity as charge together with the real part of the location. An AnnularMesh N is a structure of N concentric ring samples whose windings are uniform and sum to the declared charge field. The honest route proceeds through the phase-lift stack (CirclePhaseLift to MeromorphicCircleOrder) rather than the uniformChargeMesh construction that satisfies the claim by definition. Upstream, defect_phase_family_exists supplies a DefectPhaseFamily carrying actual phase samples near the zero, while defectAnnularMesh samples each ring at the canonical 8n equispaced angles.
proof idea
The term proof introduces the ring count N. It obtains a defect phase family dpf together with a reflexivity equality from the defect_phase_family_exists lemma applied to the given sensor and the nonzero charge hypothesis. It then directly returns the pair consisting of defectAnnularMesh dpf N and the reflexivity proof that the resulting mesh charge equals the sensor charge.
why it matters
This supplies the honest analytic sampling step that feeds direct_rh_from_honestPhaseCostBridge in AnalyticTrace and thereby the unified_rh result. It advances the Recognition Science analytic route by replacing the deprecated uniform construction with phase data that tracks the J-cost and defectDist structure. The declaration touches the open question of discharging the sorrys inherited from the complex-analysis layer in MeromorphicCircleOrder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.