pith. machine review for the scientific record. sign in
structure definition def or abbrev high

DefectPhaseFamily

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 118structure DefectPhaseFamily where
 119  sensor : DefectSensor
 120  witnessRadius : ℝ
 121  witnessRadius_pos : 0 < witnessRadius
 122  phaseAtLevel : (n : ℕ) → 0 < n → ContinuousPhaseData
 123  charge_uniform : ∀ n hn, (phaseAtLevel n hn).charge = sensor.charge
 124
 125/-- A constant-radius phase package carrying the prescribed defect charge. -/

used by (26)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.