Certified Trigonometric Envelopes and Phase Reduction

Abstract

Reusable certified-numerics infrastructure for the L2b layer of the G-c certificate: sharp trigonometric envelopes, exact golden floors, algorithmic phase reduction, and coordinatewise finite-sum bounds.

This is the L2b infrastructure layer preregistered in addendum thirty-four. It proves no numerical assertion about the candidate zero, and it makes no claim about the Riemann hypothesis.

Theorem 1.1 (Sharp any-order cosine envelope).

$$\forall x\in \mathbb{R},n\in \mathbb{N},\left|x\right|\le 1\Rightarrow \left|\cos \left(x\right)-\sum _{0\le k<n}\frac{(-1{)}^k\cdot x^{2\cdot k}}{(2\cdot k)!}\right|\le \frac{{\left|x\right|}^{2\cdot n}}{(2\cdot n)!}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.abs_cos_sub_partial_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every order n and every real x with absolute value at most one, the cosine Taylor error is bounded by the absolute value of the next term. This is the sharp alternating-series remainder, obtained from coefficient antitonicity and Mathlib’s alternating-series error theorem.

Theorem 1.2 (Sharp any-order sine envelope).

$$\forall x\in \mathbb{R},n\in \mathbb{N},\left|x\right|\le 1\Rightarrow \left|\sin \left(x\right)-\sum _{0\le k<n}\frac{(-1{)}^k\cdot x^{2\cdot k+1}}{(2\cdot k+1)!}\right|\le \frac{{\left|x\right|}^{2\cdot n+1}}{(2\cdot n+1)!}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.abs_sin_sub_partial_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

The analogous sharp next-term bound holds at every order for sine. The proof handles nonnegative x by the alternating series and transports the result across the odd symmetry of sine.

Theorem 1.3 (An enclosed phase has an exact periodic representative).

$$\forall theta\in \mathbb{R},a\in \mathbb{R},b\in \mathbb{R},k\in \mathbb{Z},\left(a\le theta\wedge \left(theta\le b\wedge \left|a-k\cdot (2\cdot \pi )\right|+b-a\le 1\right)\right)\Rightarrow \left(\exists r\in \mathbb{R},theta=r+k\cdot (2\cdot \pi )\wedge \left(\left|r\right|\le 1\wedge \left(\cos \left(theta\right)=\cos \left(r\right)\wedge \sin \left(theta\right)=\sin \left(r\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.exists_reduced_phase (✓ std3). ∎

Source. Repository-derived.

Commentary.

This generic bridge consumes an already certified exact-pi residual bound and produces the reduced representative. The rational decision theorem below computes the index and supplies that bound.

Theorem 1.4 (The rational pi approximation has certified error).

$$\left|\pi -piApprox\right|<\frac{1}{10^{19}}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.abs_pi_sub_piApprox_lt (✓ std3). ∎

Source. Repository-derived.

Commentary.

The rational value 314159265358979323846 divided by 10 to the twentieth is within 10 to the minus nineteenth of pi. The proof uses Mathlib’s pinned twenty-decimal lower and upper bounds for pi.

Theorem 1.5 (A rational interval computes a two-pi phase index).

$$\forall a\in \mathbb{Q},b\in \mathbb{Q},theta\in \mathbb{R},\left(a\le theta\wedge \left(theta\le b\wedge \left(\left|a\right|\le 10^7\wedge \left|a-\mathrm{phaseIndex}\left(a\right)\cdot (2\cdot piApprox)\right|+b-a\le \frac{99}{100}\right)\right)\right)\Rightarrow \left(\exists r\in \mathbb{R},theta=r+\mathrm{phaseIndex}\left(a\right)\cdot (2\cdot \pi )\wedge \left(\left|r\right|\le 1\wedge \left(\cos \left(theta\right)=\cos \left(r\right)\wedge \sin \left(theta\right)=\sin \left(r\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.exists_reduced_phase_of_rat (✓ std3). ∎

Source. Repository-derived.

Commentary.

The computable phaseIndex is the rational floor of a divided by twice piApprox plus one half. A decidable rational residual certificate, together with the size bound on a, absorbs the approximation error and produces an exact representative of absolute value at most one.

Theorem 1.6 (A rational interval computes a sign-changing pi phase index).

$$\forall a\in \mathbb{Q},b\in \mathbb{Q},theta\in \mathbb{R},\left(a\le theta\wedge \left(theta\le b\wedge \left(\left|a\right|\le 10^7\wedge \left|a-\mathrm{phaseIndexPi}\left(a\right)\cdot piApprox\right|+b-a\le \frac{99}{100}\right)\right)\right)\Rightarrow \left(\exists r\in \mathbb{R},theta=r+\mathrm{phaseIndexPi}\left(a\right)\cdot \pi \wedge \left(\left|r\right|\le 1\wedge \left(\cos \left(theta\right)=(-1{)}^{\mathrm{phaseIndexPi}\left(a\right)}\cdot \cos \left(r\right)\wedge \sin \left(theta\right)=(-1{)}^{\mathrm{phaseIndexPi}\left(a\right)}\cdot \sin \left(r\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.exists_reduced_phase_pi_of_rat (✓ std3). ∎

Source. Repository-derived.

Commentary.

The companion phaseIndexPi uses rational nearest-integer arithmetic at period pi. It covers phases such as the golden germ’s first mode, whose reduced representative differs by three pi, and records the exact cosine and sine sign factors.

Theorem 1.7 (Real-coordinate interval accumulation).

$$\forall I\in Type,s\in \mathrm{Finset}\left(I\right),z\in I\to \mathbb{C},lo\in I\to \mathbb{R},hi\in I\to \mathbb{R},\left(\forall i\in s,lo\left(i\right)\le \mathrm{Re}\left(z\left(i\right)\right)\wedge \mathrm{Re}\left(z\left(i\right)\right)\le hi\left(i\right)\right)\Rightarrow \left(\sum _{i\in s}lo\left(i\right)\le \mathrm{Re}\left(\sum _{i\in s}z\left(i\right)\right)\wedge \mathrm{Re}\left(\sum _{i\in s}z\left(i\right)\right)\le \sum _{i\in s}hi\left(i\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.sum_re_le_of_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

Lower and upper bounds are accumulated term by term with Finset.sum_le_sum. This atom-required bridge supports the L2c finite certificate and does not require positive summands.

Theorem 1.8 (Imaginary-coordinate interval accumulation).

$$\forall I\in Type,s\in \mathrm{Finset}\left(I\right),z\in I\to \mathbb{C},lo\in I\to \mathbb{R},hi\in I\to \mathbb{R},\left(\forall i\in s,lo\left(i\right)\le \mathrm{Im}\left(z\left(i\right)\right)\wedge \mathrm{Im}\left(z\left(i\right)\right)\le hi\left(i\right)\right)\Rightarrow \left(\sum _{i\in s}lo\left(i\right)\le \mathrm{Im}\left(\sum _{i\in s}z\left(i\right)\right)\wedge \mathrm{Im}\left(\sum _{i\in s}z\left(i\right)\right)\le \sum _{i\in s}hi\left(i\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.sum_im_le_of_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

The same atom-required mixed-sign finite-sum enclosure is available independently in the imaginary coordinate for the L2c consumer.

Theorem 1.9 (Coordinate bounds imply an additive complex norm bound).

$$\forall z\in \mathbb{C},a\in \mathbb{R},b\in \mathbb{R},\left(\left|\mathrm{Re}\left(z\right)\right|\le a\wedge \left|\mathrm{Im}\left(z\right)\right|\le b\right)\Rightarrow \Vert z\Vert \le a+b$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.norm_le_of_re_im_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

This named bind-only companion connects coordinate intervals to Mathlib’s complex norm inequality. Its directed consumer is the L2c theorem g60_center_norm_lt.

Theorem 1.10 (The first sixty-one golden floors are exact).

$$\begin{array}{r}o5FloorTable=(1,3,4,6,8,9,11,12,14,16,17,19,21,22,24,25,27,29,30,32,33,35,37,38,40,42,43,45,46,48,50,51,53,55,56,58,59,61,63,64,66,67,69,71,72,74,76,77,79,80,82,84,85,87,88,90,92,93,95,97,98)\\ \forall v\in \mathbb{N},v\le 60\Rightarrow \lfloor \left(v+1\right)\cdot \phi \rfloor =o5FloorTable\left(v\right)\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.o5Beta_floor_table (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed table is exactly floor((v+1) phi) for every v from zero through sixty. Each entry follows from the rational enclosure 1.618033 < phi < 1.618034, derived from the defining square root.

Theorem 1.11 (The golden exponent has its table-driven affine form).

$$\forall v\in \mathbb{N},v\le 60\Rightarrow o5Beta\left(v\right)=o5FloorTable\left(v\right)-1-v+v\cdot \phi$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.o5Beta_eq_affine (✓ std3). ∎

Source. Repository-derived.

Commentary.

On the certified range, the exact floor table converts the frozen golden exponent into an affine expression. The proof connects to the independently frozen closed form through floor plus fractional part, so the table definition is not a tautological carrier.

References

• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.abs_cos_sub_partial_le
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.abs_pi_sub_piApprox_lt
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.abs_sin_sub_partial_le
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.exists_reduced_phase
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.exists_reduced_phase_of_rat
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.exists_reduced_phase_pi_of_rat
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.norm_le_of_re_im_bounds
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.o5Beta_eq_affine
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.o5Beta_floor_table
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.sum_im_le_of_bounds
• Truth anchor: D5/S3/Analytic/Certified/TrigEnvelopePhaseReduction.sum_re_le_of_bounds