IndisputableMonolith.NumberTheory.DefectSampledTrace
DefectSampledTrace constructs AnnularMesh objects from DefectPhaseFamily data by sampling each ring at the canonical 8n equispaced angles. Researchers closing the RS cost-covering bridge for the Riemann hypothesis cite it when realizing concrete defect traces on circles. The module consists entirely of definitions that link phase families to annular cost bounds via the imported AnnularCost and MeromorphicCircleOrder machinery.
claimFor a defect phase family $F$, the sampled trace yields an annular mesh by evaluating $F$ at the $8n$ equispaced angles $2k/8n$ on each ring of radius $r_n$.
background
The module operates inside the NumberTheory layer of Recognition Science and imports the annular J-cost framework, the cost-covering bridge, and meromorphic circle order. From AnnularCost the key object is phiCost u := cosh((log φ)·u) − 1 = J(φ^u). From MeromorphicCircleOrder a meromorphic function with order n at ρ factors locally as (z−ρ)^n g(z) with g analytic and g(ρ)≠0. The module supplies the concrete sampling step that turns an abstract DefectPhaseFamily into a realizable AnnularMesh for later budget comparisons.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the sampled defect data consumed by ArgumentPrincipleProved (eliminates argument_principle_sampling axiom), CarrierBudgetComparison (carrier-defect budget comparison on the same circles), EulerInstantiation (Euler product instantiation of the RS carrier/sensor framework), and HonestPhaseBudgetBridge (perturbation witness for honest phase families). It fills the canonical 8n sampling step required by the RS cost-covering architecture for RH.
scope and limits
- Does not prove any zero-free region or analytic continuation.
- Does not produce explicit numerical cost bounds.
- Does not address the carrier side of any budget comparison.
- Does not discharge the perturbation-witness requirement for phase families.
used by (4)
depends on (3)
declarations in this module (25)
-
def
defectAnnularMesh -
theorem
defectAnnularMesh_charge -
structure
DefectSampledFamily -
def
chosenDefectPhaseFamily -
theorem
chosenDefectPhaseFamily_sensor -
def
chosenDefectPhasePerturbationWitness -
def
canonicalDefectSampledFamily -
theorem
canonicalDefectSampledFamily_sensor -
theorem
canonicalDefectSampledFamily_charge -
def
RealizedDefectAnnularCostBounded -
def
RealizedDefectAnnularExcessBounded -
structure
RingRegularErrorBound -
def
realizedRingPerturbationError -
structure
RingPerturbationControl -
def
ringRegularErrorBound_of_ringPerturbationControl -
theorem
annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError -
theorem
realizedDefectAnnularExcessBounded_of_ringRegularErrorBound -
theorem
realizedDefectAnnularExcessBounded_of_costBounded -
theorem
realizedDefectCostBounded_of_charge_zero_and_excessBounded -
theorem
realizedDefectCostBounded_iff_charge_zero_and_excessBounded -
def
canonicalDefectSampledFamily_ringPerturbationControl -
def
canonicalDefectSampledFamily_ringRegularErrorBound -
theorem
canonicalDefectSampledFamily_excess_bounded -
theorem
defectSampledFamily_unbounded -
theorem
not_realizedDefectAnnularCostBounded