IndisputableMonolith.NumberTheory.ArgumentPrincipleProved
This module proves Axiom 1 of the RH formalization is trivially satisfied. An AnnularMesh exists whose charge equals the sensor charge because the uniformChargeMesh meets the condition definitionally. Researchers formalizing the Riemann Hypothesis in Recognition Science cite the result to confirm the axiom count reduces to one. The argument proceeds by direct definitional verification using the imported annular mesh constructions.
claimExistence of an annular mesh $m$ such that the charge of $m$ equals the charge of the sensor holds definitionally for the uniform charge mesh.
background
The module sits inside the annular J-cost framework. AnnularCost defines phiCost u := cosh((log φ)·u) − 1 = J(φ^u). CostCoveringBridge packages the three-layer RS cost-covering architecture for RH once the budget interface is realizable. DefectSampledTrace supplies realized annular meshes attached to phase-sampling for a hypothetical zeta defect. EulerInstantiation shows that the Euler product of ζ(s) instantiates the abstract carrier/sensor framework from AnnularCost and CostCoveringBridge.
proof idea
The module contains argument_principle_trivial as a one-line wrapper that applies uniformChargeMesh N m to satisfy the charge equality definitionally. argument_principle_honest and rh_from_single_axiom extend the same definitional check to the honest and single-axiom cases. The structure imports AnnularCost, CostCoveringBridge, DefectSampledTrace and EulerInstantiation to supply the mesh objects and charge predicates without further hypotheses.
why it matters in Recognition Science
This module feeds AnalyticTrace, which assembles the full RH bridge after former axioms are eliminated, and ArgumentPrincipleSensor, which packages the phase-lift stack as the explicit certificate for the RH-from-RCL route. By discharging Axiom 1 it leaves only the Axiom 2 bottleneck noted in DefectSampledTrace. The doc-comment states: 'This means the RH formalization has exactly ONE genuine axiom, not two.'
scope and limits
- Does not resolve the second axiom in the RH formalization.
- Does not compute explicit numerical values for mesh charge beyond definitional equality.
- Does not extend the argument to non-uniform charge meshes.
- Does not address stability under perturbation of the phase sampling.