The twin-prime configuration is admissible
ProvedHardyLittlewood.twin_tuple_admissibleThe twin-prime offsets (0, 1) — giving the constellation (p, p + 2) — are admissible: the doubled offsets (0, 2) occupy at most two residue classes modulo any prime, so they never cover all classes. This is the concrete admissibility check that lets the first Hardy–Littlewood conjecture specialize to twin primes.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- The twin-prime configuration is admissible: the doubled offsets (0, 2)
occupy at most two residue classes modulo any prime, so they never cover all
residue classes. -/
theorem twin_tuple_admissible :
IsAdmissibleTuple (![0, 1] : Fin 2 → ℕ) := by
sorry
end HardyLittlewood
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for the tuple assigning offset 0 to index 0 and offset 1 to index 1 — a function from the two-element set {0, 1} to the natural numbers — the proposition "IsAdmissibleTuple" holds: for every prime q, the map sending i to the residue of 2 · m i modulo q is not surjective onto the residue classes modulo q.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.