A noncoprime active blocker has a reduced congruence fibre
ProvedLonelyRunner.CollectiveFibreNormalForm.activeFibre_of_blocksformalizationlonely-runnerlrc-shared-repair-20261007number-theory
Write , , and for the existence of an integer with and . An active fibre for consists of natural numbers with , , , , , , and, for every , if and only if . For natural , assume , , , , , and for some . Then an active fibre for exists.
Preamble
import Mathlib import Mathlib.Data.ZMod.Units import Mathlib.GroupTheory.Index import Mathlib.RingTheory.Coprime.Lemmas import Mathlib.RingTheory.Int.Basic import Definitions.Def_LRC_SharedRepair_Defs
Formal statement
open LonelyRunner
open LonelyRunner.CollectiveFibreNormalForm
theorem LonelyRunner.CollectiveFibreNormalForm.activeFibre_of_blocks {n r m q : ℕ}
(hr : 0 < r) (hrn : r < n) (hm : 0 < m) (hqp : m*r < q)
(hnot : ¬ r ∣ q) (hcop : ¬ Nat.Coprime r q)
(hactive : ∃ b ∈ CollectiveUnits.units r,
CollectiveBoundary.Blocks (n:ℤ) r m q b) :
Nonempty (ActiveFibre n r m q) := by sorry
Source
Wade Hunter, lonely-runner research repository, https://github.com/huntrontrakkr/lonely-runner; local source snapshot 9b5f51aa235e321a3ec794c9bf60358933a8e6dc, lean/LonelyRunner/CollectiveFibreNormalForm.lean, lines 30–106, declaration LonelyRunner.CollectiveFibreNormalForm.activeFibre_of_blocks. AI-assisted formalization. The snapshot identifier records the submitted local source; it is not a claim that this commit is publicly hosted.