Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Dyadic transport and complete residues

Abstract

Dyadic transport and complete residues

Multiplication by 2^k transports both binary supports without changing inclusion. The six residues of 2^s modulo 9 give a complete decomposition 82^s=72R+r for arbitrary s. Twelve residue families and eight boundary families retain their common actual integer realization. Their low-bit masks embed in disjoint high blocks; the two charge identities retain the actual new endpoints.

Definition 1.1 (ResidueFamily).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.ResidueFamily

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.ResidueFamily (✓ std3).

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Definition 1.2 (FixedFamily).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.FixedFamily

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.FixedFamily (✓ std3).

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Definition 1.3 (residueFamilies).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.residueFamilies

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.residueFamilies (✓ std3).

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Definition 1.4 (fixedFamilies).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.fixedFamilies

Formalization. D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.fixedFamilies (✓ std3).

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Theorem 1.5 (submask_scale).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.submask_scale

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.submask_scale (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Theorem 1.6 (residue_masks).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.residue_masks

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.residue_masks (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Theorem 1.7 (fixed_masks).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.fixed_masks

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.fixed_masks (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Theorem 1.8 (residue_decomposition).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.residue_decomposition

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.residue_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Theorem 1.9 (first_charge).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.first_charge

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.first_charge (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

Theorem 1.10 (second_charge).

Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.second_charge

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakHighD/SmallAAllHData.second_charge (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consumed in the construction described here, with the exact telescope supplied by Lean.

References