DefectPhaseFamily
plain-language theorem explainer
DefectPhaseFamily packages a DefectSensor, a positive witness radius, and a level-indexed family of ContinuousPhaseData objects whose charges are forced to match the sensor. Analytic number theorists working on the Recognition Science RH argument cite it when building annular meshes and sampled traces around defects. The definition is a plain record structure whose only non-data field is the charge-uniformity constraint.
Claim. A DefectPhaseFamily consists of a sensor $s$ (with associated charge), a positive real witness radius $r>0$, and a map sending each $n>0$ to a continuous phase datum $p_n$ such that the charge of every $p_n$ equals the charge of $s$.
background
The module MeromorphicCircleOrder bridges Mathlib meromorphic-order machinery to the RS annular-cost framework. A meromorphic function with order $n$ at a point factors locally as $(z-ρ)^n g(z)$ with $g$ analytic and non-vanishing; the phase charge contributed by the power term is $-n$ while the regular factor contributes zero charge. ContinuousPhaseData records a center, radius and integer charge on a circle; DefectSensor (imported from CostCoveringBridge) supplies the prescribed charge that the family must carry uniformly. Upstream, defect is identified with the J-cost functional, and the eight-tick phase supplies the discrete angular sampling used downstream.
proof idea
This is a structure definition (no proof body). It directly records the four fields sensor, witnessRadius, witnessRadius_pos, phaseAtLevel together with the single axiom charge_uniform that forces every level to inherit the sensor charge.
why it matters
DefectPhaseFamily supplies the constant-charge phase packages required by defectAnnularMesh and chosenDefectPhaseFamily in DefectSampledTrace, which in turn feed the honest-phase-cost bridge (HonestPhaseCostBridge_of_rh) and the shared-circle comparison (SharedCircleFamilyPair). It therefore closes the analytic route from meromorphic order to bounded annular cost under the RH hypothesis, linking directly to the Recognition Science forcing chain at T5 (J-uniqueness) and the phi-ladder mass formula. The structure is the precise object that lets nonzero-charge defects produce unbounded cost while zero-charge carriers remain bounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.