IndisputableMonolith.NumberTheory.DefectSampledTrace
This module assembles annular meshes for defect phase families by sampling each ring at 8n equispaced angles. Researchers closing the Riemann hypothesis via the RS cost-covering bridge cite it to convert abstract phase data into concrete sampled traces. The module is a definition module whose objects are built directly from the imported AnnularCost and MeromorphicCircleOrder primitives.
claimGiven a defect phase family $F$ on rings of radius $r_n$, the sampled trace produces an annular mesh whose nodes are the values $F(r_n, heta_k)$ at angles $\theta_k = 2\pi k/(8n)$ for $k=0,\dots,8n-1$.
background
The module sits inside the NumberTheory layer that realizes the RS cost-covering architecture. Upstream, AnnularCost supplies the $\phi$-weighted cost function $\mathrm{phiCost}(u) := \cosh((\log\phi)\cdot u)-1 = J(\phi^u)$ together with the annular sampling machinery. CostCoveringBridge packages the three-layer proof architecture that turns realizable budgets into RH contradictions. MeromorphicCircleOrder bridges Mathlib meromorphic-order data to the annular framework by supplying the local factorization $f(z)=(z-\rho)^n g(z)$ with $g(\rho)\ne0$.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the concrete sampled traces required by ArgumentPrincipleProved (which eliminates the argument_principle_sampling axiom), CarrierBudgetComparison (which compares carrier and defect budgets on the same circles), EulerInstantiation (which instantiates the Euler product inside the RS carrier/sensor framework), and HonestPhaseBudgetBridge (which turns perturbation witnesses into bounded annular excess data). It therefore closes the sampling step that converts abstract phase families into the witnessed cost bounds needed for the RH closure plan.
scope and limits
- Does not prove the Riemann hypothesis.
- Does not supply continuous rather than discrete angular sampling.
- Does not compute numerical values of the sampled costs.
- Does not address non-meromorphic 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