Endpoint
Abstract
Endpoint
For every natural 3<=a<c, c+2<=d and d<b, the original seed 1+2^a+2^(a+b)+2^(a+b+c) admits both original orders with a literal fresh ear at cut zero or immediately after nX. Every physical label occurs once. Separate zero period sums transport both strips to every natural repetition and every natural take, including zero and overlong takes. The key connection is between cyclic source arithmetic and physical packet mass: the same binary submask allocation controls both centered source systems, while inserting one fresh label changes the charge without changing the old label order. This completes this HighD domain; a=2 and the whole Circle problem remain separate.
Theorem 1.1 (actualSource_second_peak_high_d_joint_lift).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/Endpoint.actualSource_second_peak_high_d_joint_lift
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/Endpoint.actualSource_second_peak_high_d_joint_lift (✓ std3). ∎
Source. Repository-derived.
Commentary.
Consumed by the full HighD construction with the exact Lean telescope.