We do not use static look-up tables. We use a Dynamic Covering System. Every possible input state is routed through one of three deterministic transition gates — a routing-completeness property formally verified in Lean 4. (See note below: covering is a property of the front-end routing logic, distinct from per-orbit trajectory coverage of the iterated recurrence; the latter is bounded above by the recurrent set R, compute.html §3.11.)
This simulation visualizes the Erdős Covering System as a gravitational machine. Input states (Particles) fall through the system. Instead of being blocked, they are accelerated by Modulus Gates ($3n, 5n, 7n$) into new trajectories.
Standard sieves have holes. The Drift Sieve is watertight. The union of the transition functions forms a complete cover of $\mathbb{Z}$, guaranteeing that no "Idle" or "Undefined" states exist in the hardware.
When a state hits a "Modulus Gate," it isn't just routed; it is algebraically accelerated. The multiplication injects entropy (bit expansion), while the division manages the energy budget (bit contraction).
We prove the completeness of this Covering System in Lean 4. Two theorems are established: every integer satisfies at least one transition (no "Idle" or "Shadow" states), and every integer satisfies exactly one (no simultaneous routing into multiple gates).
-- Verified File: Completeness.lean
-- Proves the transition conditions form a complete, exclusive cover of ℤ.
import Mathlib.Data.Int.ModEq
import Mathlib.Tactic
namespace DriftCoverage
def T1_condition (n : ℤ) : Prop := n % 2 = 0
def T2_condition (n : ℤ) : Prop := n % 4 = 1
def T3_condition (n : ℤ) : Prop := n % 4 = 3
/-- **Completeness**: every integer satisfies at least one transition. -/
theorem complete_coverage (n : ℤ) :
T1_condition n ∨ T2_condition n ∨ T3_condition n := by
dsimp [T1_condition, T2_condition, T3_condition]
have hlo : 0 ≤ n % 4 := Int.emod_nonneg n (by norm_num)
have hhi : n % 4 < 4 := Int.emod_lt_of_pos n (by norm_num)
interval_cases (n % 4) <;> omega
/-- **Exclusivity**: every integer satisfies *exactly one* of T1/T2/T3.
Strengthens `complete_coverage` from a disjunction to a partition. -/
theorem complete_coverage_exactly_one (n : ℤ) :
( T1_condition n ∧ ¬ T2_condition n ∧ ¬ T3_condition n) ∨
(¬T1_condition n ∧ T2_condition n ∧ ¬ T3_condition n) ∨
(¬T1_condition n ∧ ¬ T2_condition n ∧ T3_condition n) := by
dsimp [T1_condition, T2_condition, T3_condition]
have hlo : 0 ≤ n % 4 := Int.emod_nonneg n (by norm_num)
have hhi : n % 4 < 4 := Int.emod_lt_of_pos n (by norm_num)
have hmod2 : n % 2 = n % 4 % 2 := by omega
interval_cases (n % 4) <;> omega
end DriftCoverageBoth theorems are fully discharged in formal_verification/Completeness.lean with no sorry and no axioms beyond Mathlib's standard library. interval_cases (n % 4) dispatches the four residue classes, and omega closes each case via linear arithmetic.
SCOPE NOTE. What this theorem proves: the routing logic at the front of the core is a complete, exclusive partition of the integers (no undefined input states, no shadow triggers). What it does not prove: that the iterated recurrence visits every state on a single orbit. The latter is the stronger "ergodicity" claim and is provably false in the strict measure-preserving sense on Fin (2^W) — driftStep is exactly 2-to-1 (compute.html §3.8), so each orbit is confined to the recurrent set R with |R| ≤ 2^(W-1) (§3.11). The covering theorem above is about routing completeness; it does not by itself establish per-orbit trajectory coverage of the iterated map.