Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

ContinuousCover

Abstract

Second peak SecondPeakA2: ContinuousCover

Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.1 (CoverRow).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.CoverRow

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.CoverRow (✓ std3).

Source. Repository-derived.

Commentary.

Definition CoverRow in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.2 (epsLo).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.epsLo

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.epsLo (✓ std3).

Source. Repository-derived.

Commentary.

Definition epsLo in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.3 (epsHi).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.epsHi

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.epsHi (✓ std3).

Source. Repository-derived.

Commentary.

Definition epsHi in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.4 (etaMax).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.etaMax

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.etaMax (✓ std3).

Source. Repository-derived.

Commentary.

Definition etaMax in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.5 (nominal).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.nominal

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.nominal (✓ std3).

Source. Repository-derived.

Commentary.

Definition nominal in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.6 (lower).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.lower

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.lower (✓ std3).

Source. Repository-derived.

Commentary.

Definition lower in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.7 (upper).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.upper

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.upper (✓ std3).

Source. Repository-derived.

Commentary.

Definition upper in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.8 (chain8).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.chain8

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.chain8 (✓ std3).

Source. Repository-derived.

Commentary.

Definition chain8 in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.9 (chain16).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.chain16

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.chain16 (✓ std3).

Source. Repository-derived.

Commentary.

Definition chain16 in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Definition 1.10 (chain32).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.chain32

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.chain32 (✓ std3).

Source. Repository-derived.

Commentary.

Definition chain32 in the source module; Three exact rational chains cover the entire closed unit interval for z=8,16,32. Their epsilon and eta envelopes apply to every p>=64 and both h=1,2, rather than to a finite sample of p. The largest selected j is 31.

Theorem 1.11 (continuous_cover).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.continuous_cover

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.continuous_cover (✓ std3). ∎

Source. Repository-derived.

Commentary.

theorem continuous_cover (z eps eta x : ℚ) (hz : z=8 ∨ z=16 ∨ z=32) (heL : epsLo z≤eps) (heU : eps≤epsHi z) (heta : eta≤etaMax z) (hx : 0≤x) (hx’ : x≤1) : ∃ j : ℕ, ∃ second : Bool, ∃ s : ℤ, j≤31 ∧ (if second then 3/8+eta else eta) ≤ x+j*(5/8-eps)-s ∧ x+j*(5/8-eps)-s ≤ (if second then 1/2-eta else 1/8-eta)

Theorem 1.12 (continuous_parameter_bounds).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.continuous_parameter_bounds

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/ContinuousCover.continuous_parameter_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

theorem continuous_parameter_bounds (p q h : ℤ) (hp : 64≤p) (hq : q=2 ∨ q=4 ∨ q=8) (hh : h=1 ∨ h=2) : epsLo (4q) ≤ (D p q h:ℚ)/(8(A p q h:ℚ)) ∧ (D p q h:ℚ)/(8*(A p q h:ℚ)) ≤ epsHi (4q) ∧ ((1+124hQ q:ℤ):ℚ)/(8(A p q h:ℚ)) ≤ etaMax (4*q)

References