Radius-Two Lee Ball Lattice Obstruction
Abstract
The three-dimensional radius-two Lee ball fails to inject into every index-twenty-five lattice quotient.
Definition 1.1 (The complete radius-two Lee ball).
Formalization. D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo (✓ std3).
Source. Repository-derived.
Commentary.
The definition lists all twenty-five integer triples in the three-dimensional radius-two Lee ball. The following membership theorem verifies that this finite enumeration is exactly the set cut out by the stated l1 inequality.
Theorem 1.2 (Enumeration equals the Lee inequality).
Proof. Machine-checked in Lean as D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.mem_leeBallTwo_iff (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every listed point has l1 norm at most two, and a bounded integer case split proves that every triple satisfying the inequality occurs in the list.
Theorem 1.3 (The ball has twenty-five points).
Proof. Machine-checked in Lean as D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo_card (✓ std3). ∎
Source. Repository-derived.
Commentary.
Kernel reduction checks the cardinality of the complete explicit enumeration; no native evaluator is used.
Theorem 1.4 (Second moment over ZMod 25).
Proof. Machine-checked in Lean as D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo_second_moment (✓ std3). ∎
Source. Repository-derived.
Commentary.
For each coefficient vector, every integer coordinate is reduced modulo twenty-five before multiplication. Expansion of the twenty-five terms gives eighteen times the coordinate-square sum.
Theorem 1.5 (Fourth moment over ZMod 25).
Proof. Machine-checked in Lean as D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo_fourth_moment (✓ std3). ∎
Source. Repository-derived.
Commentary.
The fourth-power expansion separates into thirty times the fourth power sum and twelve times the square of the second power sum. All operations occur in ZMod 25.
Theorem 1.6 (The cyclic readout is never injective).
Proof. Machine-checked in Lean as D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.zmod25_readout_not_injective (✓ std3). ∎
Source. Repository-derived.
Commentary.
Injectivity would identify the ball with all residues modulo twenty-five. The complete second and fourth residue moments then force a fourth-power sum congruent to four modulo five, while three fourth powers over F5 can sum only to zero, one, two, or three.
Theorem 1.7 (The elementary readout is never injective).
Proof. Machine-checked in Lean as D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.zmod5_pair_readout_not_injective (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every nonzero linear functional on F5 squared has five points in each fibre. Fibrewise summation and the second moment make the span of the two coefficient vectors totally isotropic. The explicit ternary F5 calculation then makes the vectors dependent, contradicting an injective paired readout.
Theorem 1.8 (Classification of additive groups of order twenty-five).
Proof. Machine-checked in Lean as D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.addCommGroup_card_twenty_five_classification (✓ std3). ∎
Source. Repository-derived.
Commentary.
The cyclic case is equivalent to ZMod 25. In the noncyclic case, exponent five supplies a ZMod 5 module; its cardinality forces finrank two and hence an additive equivalence with F5 squared.
Theorem 1.9 (No index-twenty-five lattice quotient separates the ball).
Proof. Machine-checked in Lean as D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo_lattice_obstruction (✓ std3). ∎
Citation. Sylvain Gravier and Michel Mollard and Charles Payan (1998). On the Non-existence of 3-Dimensional Tiling in the Lee Metric. DOI: 10.1006/eujc.1998.0211.
Commentary.
The quotient has order twenty-five, so the classification sends it to either the cyclic or elementary readout obstruction. Thus two points of the radius-two Lee ball have the same quotient class.
This module is an independent kernel-checked proof of the n = 3 lattice case proved by Gravier, Mollard, and Payan in 1998. Leung and Zhou proved the radius-two lattice result for every n at least three in 2020 (arXiv:1808.08520). The formal theorem asserts nothing about non-lattice tilings, other dimensions, or other radii; the cited papers are provenance rather than Lean proof dependencies. Literature attestation applies only to this lattice obstruction. The explicit ball enumeration, membership characterization, cardinality, moments, readout obstructions, and classification are independently derived proof ingredients in this repository.
References
- Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.addCommGroup_card_twenty_five_classification - Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo - Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo_card - Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo_fourth_moment - Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo_lattice_obstruction - Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.leeBallTwo_second_moment - Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.mem_leeBallTwo_iff - Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.zmod25_readout_not_injective - Truth anchor:
D5/S3/Arith/Coding/LeeBallTwoLatticeObstruction.zmod5_pair_readout_not_injective