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

DefectPhasePerturbationWitness

show as:
view Lean formalization →

DefectPhasePerturbationWitness packages the regular-factor perturbation data for any defect phase family. Downstream results in HonestPhaseBudgetBridge and CarrierBudgetComparison cite it to obtain bounded annular excess. The structure records the decomposition of each sampled increment into pure winding plus epsilon, enforces the unit bound on log-phi scaled epsilon, and requires uniform bounds on the summed linear and quadratic phi-cost contributions over all refinement depths.

claimFor a defect phase family $dpf$, the witness supplies a map $epsilon$ such that the sampled increment at level $n$ equals the pure winding increment plus $epsilon(n,hn,j)$, with $|log varphi cdot epsilon| leq 1$, and the summed $phi$-cost linear and quadratic terms over the first $N$ levels remain bounded by constants independent of $N$.

background

The module bridges Mathlib meromorphic-order machinery to the RS annular-cost framework. A meromorphic function admits local factorization $f(z)=(z-rho)^n g(z)$ with $g$ analytic and nonvanishing at $rho$; the phase charge of the pole part is $-n$ while the regular factor contributes zero charge. DefectPhaseFamily is the sibling structure that packages a constant-radius phase package carrying a prescribed defect charge, with phaseAtLevel supplying ContinuousPhaseData at each refinement level. phiCostLinearCoeff(A) equals $log varphi cdot sinh(log varphi cdot A)$ and phiCostQuadraticCoeff(A) supplies the corresponding quadratic coefficient; both appear in the linear and quadratic budget fields of the witness.

proof idea

This is a structure definition that directly encodes the four required fields: the epsilon map, the increment decomposition equation, the smallness bound, and the two existential budget bounds. No tactics or lemmas are applied inside the declaration itself.

why it matters in Recognition Science

It supplies the concrete data needed to build RingPerturbationControl and thereby prove RealizedDefectAnnularExcessBounded for any sampled family attached to a defect phase family. The structure is invoked by phaseFamily_excess_bounded_of_perturbationWitness and by the honest zeta-derived specialization, closing the analytic step from meromorphic factorization of zeta to uniform annular-cost control. It touches the open question of explicit construction of the witness for arbitrary defect sensors.

scope and limits

formal statement (Lean)

 167structure DefectPhasePerturbationWitness (dpf : DefectPhaseFamily) where
 168  epsilon : (n : ℕ) → 0 < n → Fin (8 * n) → ℝ
 169  increment_eq : ∀ n hn j,
 170    (dpf.phaseAtLevel n hn).sampleIncrements n j =
 171      defectPhasePureIncrement dpf n + epsilon n hn j
 172  small : ∀ n hn j,
 173    |Real.log Constants.phi * epsilon n hn j| ≤ 1
 174  linear_term_bounded : ∃ K : ℝ, ∀ N : ℕ,
 175    ∑ n : Fin N,
 176      phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 177        ∑ j : Fin (8 * (n.val + 1)),
 178          |epsilon (n.val + 1) (Nat.succ_pos n.val) j| ≤ K
 179  quadratic_term_bounded : ∃ K : ℝ, ∀ N : ℕ,
 180    ∑ n : Fin N,
 181      phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 182        ∑ j : Fin (8 * (n.val + 1)),
 183          (epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 ≤ K
 184
 185/-- Each sampled increment decomposes as the pure winding increment plus the
 186regular perturbation provided by the witness. -/

used by (15)

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

depends on (10)

Lean names referenced from this declaration's body.