Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Algebra

Abstract

Second peak SecondPeakA2: Algebra

The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.1 (z).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.z

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.z (✓ std3).

Source. Repository-derived.

Commentary.

Definition z in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.2 (t).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.t

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.t (✓ std3).

Source. Repository-derived.

Commentary.

Definition t in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.3 (y).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.y

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.y (✓ std3).

Source. Repository-derived.

Commentary.

Definition y in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.4 (A).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.A

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.A (✓ std3).

Source. Repository-derived.

Commentary.

Definition A in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.5 (B).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.B

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.B (✓ std3).

Source. Repository-derived.

Commentary.

Definition B in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.6 (L).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.L

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.L (✓ std3).

Source. Repository-derived.

Commentary.

Definition L in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.7 (K).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.K

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.K (✓ std3).

Source. Repository-derived.

Commentary.

Definition K in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.8 (SU).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.SU

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.SU (✓ std3).

Source. Repository-derived.

Commentary.

Definition SU in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.9 (SV).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.SV

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.SV (✓ std3).

Source. Repository-derived.

Commentary.

Definition SV in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.10 (SW).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.SW

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.SW (✓ std3).

Source. Repository-derived.

Commentary.

Definition SW in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.11 (Q).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.Q

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.Q (✓ std3).

Source. Repository-derived.

Commentary.

Definition Q in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.12 (D).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.D

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.D (✓ std3).

Source. Repository-derived.

Commentary.

Definition D in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.13 (R).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.R

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.R (✓ std3).

Source. Repository-derived.

Commentary.

Definition R in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.14 (First).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.First

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.First (✓ std3).

Source. Repository-derived.

Commentary.

Definition First in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.15 (Windows).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.Windows

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.Windows (✓ std3).

Source. Repository-derived.

Commentary.

Definition Windows in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Definition 1.16 (Good).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.Good

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.Good (✓ std3).

Source. Repository-derived.

Commentary.

Definition Good in the source module; The old and new physical endpoint polynomials retain the actual fresh charge. A2 specializes the generic x parameter to 4 and proves first, second and third charged windows with polynomial slack on the full unbounded cone. The physical endpoint expressions are consumed by the later charged-window proofs.

Theorem 1.17 (first_of_exact).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.first_of_exact

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

Source. Repository-derived.

Commentary.

theorem first_of_exact (p q h v m : ℤ) (before : Bool) (hp : 4 ≤ p) (hq : 2 ≤ q) (hh : 1 ≤ h) (hm : 0 ≤ m) (hmy : 2m < y p q h) (hw : if before then 0 ≤ 8R p q h v m ∧ 8R p q h v m ≤ A p q h-1+4mQ q else 3A p q h+1+4mQ q ≤ 8R p q h v m ∧ 8R p q h v m ≤ 4*A p q h-4) : First p q h v m before

Theorem 1.18 (second_windows).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.second_windows

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

Source. Repository-derived.

Commentary.

theorem second_windows (p q h M : ℤ) (hp : 4 ≤ p) (hq : 2 ≤ q) (hh : h=1 ∨ h=2) (hdlo : 2h ≤ 5M-(y p q h-8hp)) (hdhi : 5M-(y p q h-8hp) ≤ 4hp) : 0 < M ∧ 2M < y p q h ∧ (0 ≤ 2B p q h-2K p q h+2ML p q ∧ 2B p q h-2K p q h+2ML p q ≤ B p q h-1) ∧ (0 ≤ 2SU p q h-2SW p q h+2MSV p q ∧ 2SU p q h-2SW p q h+2MSV p q ≤ SU p q h-1)

Theorem 1.19 (third_windows).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.third_windows

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

Source. Repository-derived.

Commentary.

theorem third_windows (p q h : ℤ) (hp : 4 ≤ p) (hq : 2 ≤ q) (hh : h=1 ∨ h=2) : (0 ≤ 2B p q h-2L p q ∧ 2B p q h-2L p q ≤ K p q h-1) ∧ (0 ≤ 2SU p q h-2SV p q ∧ 2SU p q h-2SV p q ≤ SW p q h-1)

Theorem 1.20 (windows_of_first).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakA2/Algebra.windows_of_first

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

Source. Repository-derived.

Commentary.

theorem windows_of_first (p q h v m M : ℤ) (before : Bool) (hp : 4 ≤ p) (hq : 2 ≤ q) (hh : h=1 ∨ h=2) (hfirst : First p q h v m before) (hdlo : 2h ≤ 5M-(y p q h-8hp)) (hdhi : 5M-(y p q h-8hp) ≤ 4h*p) : Windows p q h v m M before

References