argument_principle_trivial
plain-language theorem explainer
The declaration shows that for any defect sensor an annular mesh of arbitrary size N exists with matching charge. Researchers formalizing the Riemann hypothesis in Recognition Science cite it to reduce the axiom count to one genuine condition. The argument is a one-line wrapper that invokes the uniform charge mesh constructor and reflexivity on the charge field.
Claim. Let $S$ be a defect sensor. For every natural number $N$ there exists an annular mesh of order $N$ such that its charge equals the charge of $S$.
background
The module treats argument principle sampling as a proved elimination of the legacy existence axiom from EulerInstantiation. DefectSensor carries a charge value while AnnularMesh N records a mesh over the annulus whose charge field sums the defects. uniformChargeMesh from CostCoveringBridge populates every mesh point with the supplied charge by definition, so the equality holds definitionally.
proof idea
The proof is a one-line wrapper. It applies the uniformChargeMesh constructor to the supplied N and sensor charge, then uses reflexivity to confirm the charge equality.
why it matters
This step reduces the Riemann hypothesis formalization axiom inventory from two to one by discharging the trivial existence claim. It clears the path for the honest argument principle phase family that builds meshes from witnessed zeta inverse phase data. The reduction aligns with the primitive distinction result that collapses seven axioms to four structural conditions plus definitional facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.