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

canonicalDefectSampledFamily_ringPerturbationControl

show as:
view Lean formalization →

This definition equips the canonical defect-sampled family attached to a nonzero-charge sensor with a ring-perturbation control package. It certifies that every realized increment lies inside the unit-scale regime of the phi-cost function and that the total linear-plus-quadratic error sum remains bounded independently of mesh depth. Construction proceeds by factoring each increment into a pure winding term plus a small regular perturbation and invoking separate boundedness results for the linear and quadratic coefficients.

claimLet $S$ be a defect sensor with nonzero charge. Let $F$ be the canonical sampled family of realized annular meshes attached to the phase of $S$. Then $F$ admits a perturbation control: for all refinement depths $N$, ring indices $n$, and increment indices $j$, $|log phi · (Δ_j − (−2π · charge(F)/(8(n+1))))| ≤ 1, and there exists $K$ such that the summed realized ring perturbation errors over all rings at depth $N$ is at most $K$.

background

In the Defect Sampled Trace module the remaining obstacle after Axiom 1 is Axiom 2, which requires bounding the cost of the canonical sampled family coming from the phase of ζ⁻¹ near a hypothetical defect. The module packages this family via defectAnnularMesh and canonicalDefectSampledFamily. RingPerturbationControl is the structure that quantifies the deviation of realized increments from the pure topological winding term, using the linear and quadratic coefficients of the phi-cost function on [−A,A]. Upstream results supply the canonical arithmetic object, the universal forcing self-reference, and the non-resonant schedule, together with the explicit expressions for the linear and quadratic perturbation coefficients.

proof idea

The definition lets dpf be the chosen defect phase family and hw the chosen perturbation witness. It refines the small field by applying the regular perturbation smallness lemma to the decomposed increment pure + epsilon, after simplifying the pure term to the explicit winding formula. For the total_bounded field it obtains separate bounds on the linear and quadratic terms from the witness, then assembles the error sum by substituting the decomposition and applying sum-congruence to isolate the epsilon sums.

why it matters in Recognition Science

This definition supplies the perturbation-control package that is fed directly into canonicalDefectSampledFamily_ringRegularErrorBound, which in turn yields the regular-error bound needed for bounded annular excess. It forms the quantitative target for the Axiom 2 attack: once the complex-analysis stack proves the required factorization and log-derivative bound on the regular factor, the present construction shows that Axiom 2 reduces exactly to forcing zero charge. The construction relies on the eight-tick octave structure implicit in the annular sampling and on the phi-cost expansion.

scope and limits

Lean usage

exact ringRegularErrorBound_of_ringPerturbationControl _ (canonicalDefectSampledFamily_ringPerturbationControl sensor hm)

formal statement (Lean)

 322noncomputable def canonicalDefectSampledFamily_ringPerturbationControl
 323    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
 324    RingPerturbationControl (canonicalDefectSampledFamily sensor hm) := by

proof body

Definition body.

 325  let dpf := chosenDefectPhaseFamily sensor hm
 326  let hw := chosenDefectPhasePerturbationWitness sensor hm
 327  refine { small := ?_, total_bounded := ?_ }
 328  · intro N n j
 329    have hsmall := regular_perturbation_small hw (n.val + 1) (Nat.succ_pos n.val) j
 330    have hinc :
 331        (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
 332          defectPhasePureIncrement dpf (n.val + 1) +
 333            hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
 334      simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
 335        defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
 336        regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
 337    have hpure :
 338        defectPhasePureIncrement dpf (n.val + 1) =
 339          -(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
 340            (8 * (n.val + 1) : ℝ) := by
 341      simp [defectPhasePureIncrement, canonicalDefectSampledFamily_charge,
 342        chosenDefectPhaseFamily_sensor, dpf]
 343    rw [hinc, hpure]
 344    simpa using hsmall
 345  obtain ⟨K₁, hK₁⟩ := regular_perturbation_linear_term_bounded hw
 346  obtain ⟨K₂, hK₂⟩ := regular_perturbation_quadratic_term_bounded hw
 347  refine ⟨K₁ + K₂, ?_⟩
 348  intro N
 349  have hlin := hK₁ N
 350  have hquad := hK₂ N
 351  have hterm :
 352      ∀ n : Fin N,
 353        realizedRingPerturbationError (canonicalDefectSampledFamily sensor hm) N n =
 354          phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 355            ∑ j : Fin (8 * (n.val + 1)),
 356              |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| +
 357          phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 358            ∑ j : Fin (8 * (n.val + 1)),
 359              (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
 360    intro n
 361    dsimp [realizedRingPerturbationError]
 362    have hpure :
 363        defectPhasePureIncrement dpf (n.val + 1) =
 364          -(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
 365            (8 * (n.val + 1) : ℝ) := by
 366      simp [defectPhasePureIncrement, canonicalDefectSampledFamily_charge,
 367        chosenDefectPhaseFamily_sensor, dpf]
 368    rw [hpure]
 369    have hlinSum :
 370        ∑ j : Fin (8 * (n.val + 1)),
 371          |(((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j -
 372            (-(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
 373              (8 * (n.val + 1) : ℝ))| =
 374        ∑ j : Fin (8 * (n.val + 1)),
 375          |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| := by
 376      apply Finset.sum_congr rfl
 377      intro j _
 378      have hinc :
 379          (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
 380            defectPhasePureIncrement dpf (n.val + 1) +
 381              hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
 382        simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
 383          defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
 384          regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
 385      rw [hinc, hpure]
 386      ring_nf
 387    have hquadSum :
 388        ∑ j : Fin (8 * (n.val + 1)),
 389          ((((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j -
 390            (-(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
 391              (8 * (n.val + 1) : ℝ))) ^ 2 =
 392        ∑ j : Fin (8 * (n.val + 1)),
 393          (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
 394      apply Finset.sum_congr rfl
 395      intro j _
 396      have hinc :
 397          (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
 398            defectPhasePureIncrement dpf (n.val + 1) +
 399              hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
 400        simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
 401          defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
 402          regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
 403      rw [hinc, hpure]
 404      ring_nf
 405-- ... 28 more lines elided ...

used by (1)

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

depends on (21)

Lean names referenced from this declaration's body.