mkSharedCirclePair
plain-language theorem explainer
mkSharedCirclePair builds a SharedCircleFamilyPair by combining a zero-charge carrier phase family from regular factors with a charged defect phase family from the meromorphic reciprocal, both on the same sequence of shrinking circles. Number theorists pursuing the Riemann hypothesis via cost-budget contradictions cite this construction to set up the paired sampling. The definition works by explicit structure assembly using the regular factor phase constructor and the genuine zeta phase family, with equalities proved by reflexivity.
Claim. Given a defect sensor with charge $m$ and a quantitative local factorization of order $-m$, the paired families on shared circles consist of a carrier phase family with zero charge constructed from the regular factor phase at radii $r_0/(n+1)$ and a defect phase family derived from the meromorphic phase, sharing the same witness radius.
background
A SharedCircleFamilyPair is a structure that records a carrier sampled family paired with a defect family on the same concentric circles around a common center, allowing direct comparison of their annular costs. The carrier family is built from the Euler carrier, which is holomorphic and nonvanishing on Re(s) > 1/2 and therefore carries zero charge. The defect family comes from the reciprocal of zeta, which has a pole or zero of order m at the hypothetical point and therefore carries nonzero charge. This module formalizes the carrier-defect budget comparison strategy for the RH closure plan: on identical circles the carrier excess remains bounded while the defect topological floor diverges.
proof idea
The definition directly assembles the SharedCircleFamilyPair record. The carrierPhaseFamily field is populated by a sensor with charge reset to zero together with a phaseAtLevel function that invokes regularFactorPhaseFromWitness at each scaled radius and extracts the continuous phase data; charge_uniform is discharged by the same construction. The defectPhaseFamily field is obtained by calling genuineZetaDerivedPhaseFamily. The three equality fields (carrier_sensor_charge_zero, defect_sensor_eq, shared_radius) are filled by reflexivity.
why it matters
This definition supplies the concrete shared-circle object required by the downstream theorem carrier_defect_comparison_rh, which shows that the defect cost exceeds any finite carrier budget for sufficiently large refinement depth. It thereby instantiates the abstract budget-transfer argument of the module: carrier excess is bounded while defect floor grows as Theta(m^2 log N). The construction closes one step in Phase 4a of the RH closure plan by making the paired sampling available for the contradiction argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.