OAI.PeriodicTilingThree.periodic_tiling_counterexample_and_minimality
OpenThe theorem states two things, with Lattice(d) denoting the integer lattice ℤ^d and Space(d) denoting ℝ^d. First, there is a nonempty finite set T of points in ℤ^3 such that: some subset A of ℤ^3 tiles with T, meaning the map (t,a) ↦ t+a from T×A to ℤ^3 is a bijection; every subset A of ℤ^3 that tiles with T in this sense fails to be fully periodic, where fully periodic means that some finite-index additive subgroup P of ℤ^3 consists of periods of A (v is a period when x+v∈A exactly when x∈A for all x); there is an almost-everywhere tiling of ℝ^3 by the thickening of T, namely the union of unit cubes [0,1]^3 translated by the points of T, using some set A⊆ℝ^3, meaning that for Lebesgue-almost every x there is exactly one a∈A with x−a in the thickening; and every such almost-everywhere tiling set A fails to be Euclidean fully periodic, meaning there is no real basis of ℝ^3 whose integer span consists entirely of periods of A. Second, 3 is the least natural number d for which some nonempty finite T⊆ℤ^d tiles ℤ^d with some set A, while no set A that tiles with T is fully periodic.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/PeriodicTilingThree.lean; bytes 1498..1954
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
import Definitions.Def_PeriodicTilingThree
namespace OAI
noncomputable section
universe u
namespace PeriodicTilingThree
variable {G : Type u} [AddCommGroup G]
open MeasureTheory
theorem periodic_tiling_counterexample_and_minimality :
(∃ T : Finset (Lattice 3), T.Nonempty ∧
(∃ A : Set (Lattice 3), Tiles T A) ∧
(∀ A : Set (Lattice 3), Tiles T A → ¬ FullyPeriodic A) ∧
(∃ A : Set (Space 3), AETiles (Thickening T) A) ∧
(∀ A : Set (Space 3),
AETiles (Thickening T) A → ¬ EuclideanFullyPeriodic A)) ∧
IsLeast {d : ℕ | HasTileWithoutPeriodicComplement d} 3 := by
sorry
end PeriodicTilingThree
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.