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

canonicalDefectSampledFamily

show as:
view Lean formalization →

The canonical sampled family for a defect sensor with nonzero charge is obtained by converting the chosen phase family into a realized annular mesh family. Analysts attacking Axiom 2 in the Recognition Science framework cite this construction when establishing cost bounds for hypothetical zeta defects. The definition is a direct one-line wrapper applying the toSampledFamily conversion to the phase family chosen via Classical.choose.

claimLet $S$ be a defect sensor with nonzero charge. The canonical sampled family attached to $S$ is the family of annular meshes obtained by realizing the chosen phase family for $S$.

background

DefectSampledFamily is a structure consisting of a sensor, a map from natural numbers to AnnularMesh, and a charge specification ensuring each mesh carries the sensor charge. DefectSensor is a structure recording the charge (multiplicity of the zeta zero), real part, and location in the right half of the critical strip. The module sets up realized annular meshes for the phase-sampling construction of zeta inverse near a hypothetical defect, after Axiom 1 is eliminated and the remaining bottleneck is Axiom 2. chosenDefectPhaseFamily selects one such phase family using the strengthened existential package defect_phase_family_with_perturbation_exists.

proof idea

This definition is a one-line wrapper that applies the toSampledFamily method of DefectPhaseFamily to the result of chosenDefectPhaseFamily sensor hm.

why it matters in Recognition Science

This definition supplies the concrete object needed for the inconsistency theorems in EulerInstantiation such as defect_annular_cost_bounded_inconsistent. It realizes the phase-sampling construction for the zeta defect in the refined Axiom 2 argument. It connects directly to the annular coercivity and cost bounds in the NumberTheory layer, feeding the excess-bounded and ring-regular-error-bound packages.

scope and limits

Lean usage

theorem example (s : DefectSensor) (h : s.charge ≠ 0) : (canonicalDefectSampledFamily s h).sensor = s := canonicalDefectSampledFamily_sensor s h

formal statement (Lean)

  96noncomputable def canonicalDefectSampledFamily (sensor : DefectSensor)
  97    (hm : sensor.charge ≠ 0) : DefectSampledFamily :=

proof body

Definition body.

  98  (chosenDefectPhaseFamily sensor hm).toSampledFamily
  99
 100/-- The canonical sampled family remembers the requested sensor. -/

used by (12)

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

depends on (7)

Lean names referenced from this declaration's body.