epsilon_log_phi_small
plain-language theorem explainer
The bound |log φ ⋅ ε| ≤ 1 holds for each sampled phase increment ε drawn from the regular factor of a quantitative local factorization at refinement depth n. Analysts closing perturbation estimates for meromorphic phase families in the Recognition Science zeta application cite it to control the log-φ scale error in annular cost calculations. The proof first invokes the regime condition M R ≤ 1 to reduce |ε| below 1 via arc-length estimates, then uses the supplied bounds 1.5 < φ < 1.62 to obtain log φ < 1 and concludes the product is at most 1.
Claim. Let $M$ be the uniform bound on the logarithmic derivative of the regular factor and $R$ its radius in a quantitative local factorization. For positive integer $n$ and sample index $j$ among the $8n$ points on the circle of radius $R/(n+1)$, the regular-factor phase increment satisfies $|log φ ⋅ ε_j| ≤ 1$.
background
A quantitative local factorization augments a local meromorphic witness with a uniform bound $M$ on |g'/g| for the regular factor g together with the regime condition M R ≤ 1. This supplies the analytic control on phase perturbations ε_j sampled at angular spacing 2π/(8n) on circles of radius R/(n+1). The module develops meromorphic-order machinery to connect to the Recognition Science annular-cost framework, separating the winding contribution of the pole part from the zero-charge regular factor whose increments must remain small in the log φ scale.
proof idea
The tactic proof records n ≥ 1, pulls the perturbation regime, and applies the absolute increment bound from the log-derivative estimate. It establishes positivity and the strict inequality log φ < 1 by comparing φ to e using the supplied constants φ > 1.5 and φ < 1.62. The main calculation then chains the regime bound through ring and field simplifications to reach |ε| ≤ π/(4n(n+1)) < 1, whence multiplication by log φ < 1 yields the claimed product bound ≤ 1.
why it matters
The result is invoked by the carrier-excess theorem for shared-circle pairs and by the genuine zeta-derived phase perturbation witness. It supplies the uniform smallness of regular-factor perturbations required to close the linear and quadratic error estimates inside the DefectPhasePerturbationWitness structure. Within the Recognition framework it supports the transition from meromorphic factorization to controlled phi-cost increments on the eight-tick octave sampling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.