Repository navigation
The prime case of Erdos problem 634 remains OPEN. This release records a real
closure of one branch (e = 1, all f >= 3) and a substantial data/guard
correction pass, with no claim of closure of the prime case as a whole.
The e = 1 subfamily is closed, for every f >= 3, independent of the
advance-and-collide conjecture. A new argument (MarchInduction.lean,
MarchSlots.lean, RunPartition.lean, MarchCompose.lean, E1NormalForm.lean,
E1BaseWord.lean; ~5000 lines, axiom-free beyond propext, Classical.choice
and Quot.sound, no sorry) proves that no congruent dissection of the m = 1,
e = 1 base-beta target exists for f >= 3, over exactly the paper's class of
tilings (any isometry including reflections, any tile count). The mechanism:
every junction of the forced base word is a boundary point of the target,
hence a finite vertex figure that pins each tile's orientation; a new
exact-partition lemma for a straight run clamped between placed tiles or the
target boundary (formalising Proposition cornerpara's own argument) then
excludes every remaining configuration. The result was adversarially audited
twice by a fresh reviewer with no access to the proving session's reasoning:
no vacuous hypotheses, the negative control (every certified real tiling in
the corpus: N=44, 99, 176, 63, 52, 22, 28, 77) correctly fails the theorem's
hypotheses by computation, and the theorem's class of dissections matches the
paper's exactly. Composed with the existing thm:mod12/prop:repunique/thm:main,
every prime 3f^2 - 1 with f >= 3 (47, 107, 191, 431, 587, ...) is excluded;
f = 2 (N = 11) remains settled by exhaustive search, outside the Lean
theorem. thm:e1family's paper tag is corrected from CONJECTURE to PROVED for
f >= 3 accordingly, citing this route rather than the deferred
strip-and-column exposition, which is kept for its architecture.
This does not touch the prime case's harder branch. e >= 2 (N = 83 first,
the large majority of base-beta primes by density) is untouched and still
reduces entirely to the crossing question, proven immune to nine tool
classes and to every pairwise combination of them (closed this cycle). A
newly-formalized residue at thick members (e = f-1: EpredColumnKill.lean)
shows that branch's open content is NOT the crossing question but exclusion
of a family of extra base columns -- a different, equally untouched, open
problem.
Data and guard correction pass. An audit of the computational record found
and fixed a real hole in code/guard_run.sh (it parsed instances by line, so
a packed one-line instance -- the format used by every N=83/N=131 search --
was waved through as novel rather than refused as settled; the fix's own
first version then clobbered the engine's node-cap argument, caught by a
strengthened guard_selftest.sh). The e=1 sweeps' coverage certificate was
found to rest on an unproved pincer reach (reach 4; the proved reach is 3):
recomputed at the proved reach, four of five sweeps already covered it and
the fifth (f=24) was missing 21 orbits, now run and exhausted -- all NO_TILING,
matching an exact closed-form node-count formula fitted to all 539 sweep
results (zero residual, product of Fibonacci marches on the base word's
three runs, every coefficient f-independent). Twelve unrecorded search
results were backfilled into data/SETTLED.tsv and two wrong rows corrected.
Net: one full branch of the prime case (e = 1) is closed unconditionally for
all f >= 3, by a machine-checked argument independently audited twice. The
harder branch (e >= 2) is exactly as open as before, with its residue now
more precisely characterized. The computational record and the guard that
protects it against recomputation are more reliable than they were.