SharedCircleFamilyPair
plain-language theorem explainer
SharedCircleFamilyPair records a zero-charge carrier phase family paired with a nonzero-charge defect phase family on identical concentric circles around one sensor. Researchers closing the Riemann hypothesis via annular-cost divergence cite this record to enable direct comparison of bounded carrier excess against diverging defect floor. The declaration is a six-field structure definition enforcing shared radius and the carrier charge-zero condition.
Claim. Let $S$ be a defect sensor. A shared-circle pair consists of a carrier phase family $C$ satisfying $C$.sensor.charge $= 0$, a defect phase family $D$ with $D$.sensor $= S$, and equal witness radii for $C$ and $D$, so that annular costs on the same circles may be compared directly.
background
The module develops the carrier-defect budget comparison strategy (Phase 4a of the RH closure plan). On circles centered at a hypothetical zero of zeta, the carrier family is the holomorphic Euler factor $C(s) = det_2(I-A(s))^2$ with charge zero, so its topological floor vanishes and sampled cost equals excess. The defect family is the reciprocal zeta with charge $m ≠ 0$, so its floor grows as Θ(m² log N). Both families sample the identical geometric circles, allowing the bounded carrier excess to be transferred against the diverging defect total cost.
proof idea
This is a structure definition. It introduces the type SharedCircleFamilyPair with fields sensor, carrierPhaseFamily, defectPhaseFamily together with the three equality constraints carrier_sensor_charge_zero, defect_sensor_eq, and shared_radius.
why it matters
The structure supplies the common data type for the module's comparison theorems. It is used directly by carrier_cost_bounded_of_shared_pair to obtain bounded carrier cost, by defect_cost_unbounded_of_shared_pair to obtain unbounded defect cost when charge is nonzero, and by defect_cost_exceeds_carrier_budget to derive the contradiction that forces the charge to vanish. It thereby fills the local factorization step of the RH closure argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.