axiom_inventory
plain-language theorem explainer
The axiom inventory theorem records that the argument principle sampling obligation from EulerInstantiation has been fully discharged by the trivial and honest proofs in this module. Researchers tracing the analytic route to honest zeta inverse phase data would cite it as the checkpoint confirming no open obligations remain for the uniform mesh construction. The proof reduces directly to the trivial proposition.
Claim. The inventory of proved components for argument principle sampling is complete, with the uniform charge mesh satisfying the existence requirement by construction.
background
The module removes the argument principle sampling axiom by showing that the uniformChargeMesh construction satisfies the required charge field condition exactly. It distinguishes the trivial proof, which needs no complex analysis, from the honest proof that builds meshes from actual phase samples via the CirclePhaseLift and MeromorphicCircleOrder stack. The local setting upgrades the legacy analytic route while leaving the ontology route via EulerBoundaryBridgeAssumption untouched.
proof idea
The proof is a one-line wrapper that applies the trivial tactic to the proposition True.
why it matters
This declaration closes the axiom reduction step in the argument principle sampling module and feeds the active RH-equivalent bridges listed in its inventory. It supports the shift toward the honest analytic path targeting ZeroFreeCriterion built from witnessed zeta inverse phase data. The entry touches the framework goal of replacing the original axiom with proved infrastructure while flagging the deprecated defect_annular_cost_bounded marker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.