v3.2 -- e=1 closed for f>=3; guard and data corrections

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.

v3.1 — crossing-question subatomization; debt-correction pass

The prime case of Erdos problem 634 remains OPEN. This release records real
advances against it and a substantial formalization-debt correction pass,
with no claim of closure.

What advanced against the crossing question. Every route into the residue
(primes congruent to 11 mod 12) still reduces to one crossing question,
provably immune to nine classes of relocation-invariant argument. This
release adds a tenth and eleventh dead class, found and closed with proofs
rather than failed searches: Monsky's valuation/Sperner method (too weak --
area-only, blind to the collinearity the question actually asks about), and
the irrationality/transcendence class (the surviving branch is the absence
of a closure equation, not a coincidence to disprove). Oblique and bent
interior walls are shown to transmit no more than straight ones
(BentWallCoupling.lean): straightness is the strongest local angular
hypothesis available, not an arbitrary special case. A minimal-counterexample
descent architecture is shown structurally impossible (the family's only
recursion, the cevian decomposition, runs strictly upward). The Galois
conjugation of the coordinate field is proved to be exactly the mirror
symmetry already in use (GaloisMirror.lean), unifying two independent
2026-09-05/09-09 dead ends into one fact.

The crossing question's open branch -- "does an edge cross V_k or land on
it" -- is fully enumerated for the first time: exactly 2*floor(b/a)+2
explicit configurations (N1GapSubcases.lean), not the two the informal
account suggested. Every one of them is now proved to admit no monovariant
in its index (N1GapMastGap.lean, N1GapCRange.lean), including a precise
account of why a promising-looking straddle chain terminates after one step
rather than descending. A newly-identified prerequisite -- a base-column
dichotomy at f <= 2e -- is proved NOT to exist: the extra columns are
genuinely unbounded on the whole e=f-1 family, exactly f+2 of them, not a
finite few (EpredBaseColumns.lean). A real factor-2 error in the strip
rigidity argument's stated reach is found and corrected (StripRigid.lean):
the "mast" boundary constraint reaches exactly one tile position, not two.

Formalization-debt correction pass. A systematic audit of lean/PAPER_MAP.md
found and repaired eleven real defects that had accumulated: mislabeled Rule-0
statuses, vacuous "dissection-level" theorems whose existential conclusions
were provable with no geometric content (a recurring bug class, now named and
searched for systematically), a circular theorem restating its own hypothesis
as its conclusion, false citations -- including one that had propagated into
this project's own "verified end to end" claim for the E2 angle-sum layer --
a wrong base-word formula, and a build-gate coverage gap where roughly 68
files were never being checked by the project's own CI-equivalent build.
Four Rule-0 labels were corrected (one up, one down, two mislabeled
CONJECTURE/HEURISTIC rows moved to their earned status) after checking the
actual paper statement against the actual Lean, not against ingredients.

Base-beta family data. (e,f,m)=(1,4,2), N=188, tile (4,15,16): exhaustively
searched, NO_TILING, recorded to data/SETTLED.tsv. Not a prime instance, but
a genuine data point in the family's realizability table that several open
map rows depend on the shape of.

Net: the prime case is not closed. What is smaller and sharper is the set of
places a real argument could still live -- several tool classes and structural
routes are now closed with proofs, the crossing question's residual case
structure is explicit rather than informal, and the corpus's own formalization
debt is measurably more honest than it was.

v3.0 — Route 1 formalised to a single composition step; the open case mapped

The prime case of Erdos problem 634. Primes not congruent to 11 mod 12 are
excluded unconditionally. The residue -- the primes congruent to 11 mod 12 --
is OPEN, and this release maps it and advances it.

What the map says (GOAL_PRIMES.md). A prime forces the scale m = 1, so the
residue IS the m = 1 base-beta family. It splits e = 1 / e >= 2, and both
reduce to one crossing question that nine classes of invariant provably cannot
answer, each being invariant under relocating an edge while the question asks
where an edge lies. For e = 1 the shorter route is conj:advance, which if
proved closes the branch entirely.

What advanced. conj:advance had two gaps; the second was already closed by
prop:doublec at every initial block length, and the stale text claiming
otherwise is corrected. The first reduces to a single question -- what covers
a segment [V,E] of length exactly a -- whose chain is now machine-checked in
41 theorems (lean/Erdos634/RouteOne.lean, companion section 'Route 1's chain,
formalised'):

• the approach points to V exist and are covered, V being interior;
• taken strictly above the wall, the tile the pigeonhole selects is an upper
  tile, not the straight tile below;
• its edge directions are weakly upward, its other vertices lying in its
  carrier and a strictly-below point being interior to the tile beneath;
• hence the flank at V lies along the line, non-degeneracy supplying the
  not-both-horizontal condition since the cross product IS the determinant;
• a b- or c-edge from V contains E strictly and dies by the very blocking
  whose failure defined the escape;
• the surviving a-advance is a descent terminating after finitely many wall
  edges, each advance consuming a distinct one.

One hypothesis remains uncomposed: that V is a vertex of the serving tile
rather than interior to one of its edges. The figure at V gives it in
principle, the single straight angle there belonging to the tile below, but
the pigeonhole's returned tile is not yet known to be among the tiles the
figure counts.

Also in this release. N = 1451 certified, 168 of 168 orbits at both proved
reaches -- thirteen members now settled by certified exhaustive search, each
with a coverage certificate. prop:orientmonobdy VERIFIED: monotonicity of the
orientation word on a side of the target, with no bridge (c), the local corner
figure giving it. A coordinate model of the march run validated against the
engine's exact arithmetic, with the BG->GB transition killed two independent
ways. The Zenodo description corrected: it had said the base-beta branch was
excluded by a forcing chain, which it is not.

Labels: VERIFIED 45, PROVED 125, CONJECTURE 32, HEURISTIC 4, OPEN 3.
Lean: 216 files, no sorry, axioms limited to propext, Classical.choice,
Quot.sound.

v2.62 — Route 1's chain formalised; N=1451 certified; the open case mapped

Prime case, honest position: the residue is the primes = 11 mod 12. This
release maps it (GOAL_PRIMES.md) and advances the shorter route for e = 1.

New:

• N = 1451 certified, 168 of 168 orbits at both proved reaches; thirteen
  members now settled by certified exhaustive search.
• conj:advance's gap 2 was already closed by prop:doublec; the stale text
  claiming otherwise is corrected. The remaining gap reduces to one question,
  what covers a segment [V,E] of length exactly a.
• That question's chain is machine-checked (lean/Erdos634/RouteOne.lean,
  companion section 'Route 1's chain, formalised'): the flank at V lies along
  the line; a b- or c-edge would contain E strictly and dies by the very
  blocking whose failure defined the escape; the surviving a-advance is a
  descent terminating after finitely many wall edges. Two hypotheses remain
  uninstantiated at the escape configuration (rem:routeoneopen).
• prop:orientmonobdy VERIFIED: monotonicity of the orientation word on a side
  of the target, with no bridge (c) -- the local corner figure gives it.
• A coordinate model of the march run, validated against the engine's exact
  arithmetic, with the BG->GB transition killed two independent ways.

Labels: VERIFIED 44, PROVED 125, CONJECTURE 32, HEURISTIC 4, OPEN 3.

v2.61 — core paper stripped to results

The papers are restructured so that the core result is readable on its own.

erdos-634.pdf (34 pp, was 41) — the prime case. Results only.

erdos-634-companion.pdf (55 pp, was 68) — the base-beta branch. Every theorem, no record of what failed.

erdos-634-obstructions.pdf (23 pp, new) — scope limits, no-go theorems, closed routes, and the claim-by-claim verification table. Nothing here is needed to read the other two.

Moved out of the two mathematical papers: 47 scope-and-failure remarks, the subsection on the two mechanisms provably unable to close p=1, the list of closed routes, and the verification catalogue. Each moved remark leaves a one-sentence pointer under the same label, so no theorem now stands without its scope and cross-references still resolve.

Kept in place: Zhang's spectrum results, the Beeson Theorem 14 defect and its counterexample, Hall's condition as the sharp criterion for the extra base columns, and the statements of what is and is not unconditional.

Audited across all three files: 52 theorems, 46 lemmas, 41 propositions, 20 corollaries, 2 definitions — nothing removed. All three compile with no undefined references.

Verification unchanged: 69 Lean modules, 807 theorems, no sorry, no axioms beyond Mathlib's three. The 28-, 44-, 77- and 99-tiling certificates are kernel-checked.

v2.60 — tiling certificates and a counterexample to Beeson's Theorem 14

Machine-checked tiling certificates, and a counterexample to Theorem 14 of Beeson's Triangle tiling III.

Tiling certificates (Lean 4, kernel-checked, no axioms). Four explicit dissections of a triangle into congruent triangles, each certificate verifying that every piece has the correct squared side multiset, is positively oriented, lies inside the closed target, is separated from every other piece by an explicit line, and that the signed areas sum exactly to the target's area:

N	target	tile	source
28	—	—	Beeson's triquadratic construction
44	(16,16,22)	(2,3,4)	this work
77	—	—	Beeson's four-component construction
99	(24,24,33)	(2,3,4)	this work

None of 28, 44, 77, 99 is of the form k^2, k^2+m^2 or 3k^2.

Counterexample to Theorem 14 of arXiv:1206.2229. The 99-tiling has s = a/c = 1/2, g = gcd(a,c) = 2, N = 99, M = 9. The theorem's other conclusions hold exactly on it — N/M^2 = 11/9 = (3-s^2)/(1+s)^2, and 0 < N/3 = 33 < M^2 = 81 < 2N = 198 — while its conclusion g | M fails. M is not chosen: it is pinned both by that displayed equation and by the colouring equation M(a+b+c) = X +/- Y + Z of the same paper's Theorem 1, and the colouring condition is automatic there by its Lemma 10.

Base-beta branch. The inflated tile admits no p=1 boundary at thirteen members; the family e = f-1 is closed uniformly with no search. The crux at (3,7) remains open and is stated as such.

Verification. 69 Lean modules, 798 theorems, zero sorry.

v2.59 — consolidation, status ledger, and a retraction

Consolidation of all working copies, a new top-level ledger, and a retraction.

STATUS_TABLE.md — the ledger

New top-level document. The headline theorem with every hypothesis it carries; branch-by-branch
status of the prime problem; what this project has that the literature does not; the four gaps
stated precisely; the machine-checked inventory (18 Lean files, 138 theorems, no sorry, all
axiom-clean); the dead ends that must not be retried; the traps that have already cost us; and
ranked next moves.

Retraction

The earlier Zenodo/referee package (now at archive/zenodo-v1/) closes one of its notes with:

"Therefore no prime = 3 (mod 4) is a number of congruent triangles tiling a triangle -- the
folklore conjecture, and the open part of Erdos #634, is resolved."

That is false. The Phi-invariant original to that note is sound and survives verbatim in the
current paper. The error is in the assembly: it disposes of the 3a+2b = pi family "by standing
theorems", and we have since proved those theorems defective. Beeson III Theorem 14 is FALSE --
refuted by an explicit 99-tiling we constructed and verified in exact Q(sqrt 15) arithmetic -- and
Theorems 18, 19, 20, the squarefree half of Lemma 8, and Lemma 6 as quoted are unsound. With those
removed the base-beta sub-branch is open, and it is exactly the primes = 11 (mod 12): 42 below
1000, of which six are settled, all by exhaustive search and none by theorem.

The N = 19 conclusion survives, because 19 = 7 (mod 12) is not a base-beta candidate; but its
original justification routed through the same defective citations and is repaired in the current
paper. archive/zenodo-v1/SUPERSEDED.md states all of this at the point of use.

The defensible claim now is: no prime = 7 (mod 12) is a tile count, in particular not 19; the class
11 (mod 12) is open; and here are five defects in Beeson's Triangle Tiling III, one refuted by an
explicit tiling.

Consolidation

Three directories held 634 material; everything is now in one place. Merged in the verification
scripts, the search engine and its three tiling certificates, and the entire superseded Zenodo
package preserved verbatim (including its Rust search code) under archive/zenodo-v1/.

Corrections to README and HANDOFF

The thin regime (f > 2e) is NOT closed structurally -- withdrawn. N = 59 is settled, not "under
search". The Lean layer is eighteen files, not ten. The far-side chase is a closed branch, not a
live next action.

Papers unchanged: main 29 pp, companion 10 pp, both building clean.

v2.58 — the split: 29 pp main, 10 pp companion

The paper is split, and two correctness defects are fixed.

The split

erdos-634.pdf 29 pp the main theorem and the record
erdos-634-companion.pdf 10 pp the base-beta branch

21 numbered environments moved to the companion: the entire base-beta boundary-walk chase. None of
it is needed for the main theorem -- it concerns the one open branch. Cross-document references are
wired with xr, so the companion cites the main paper's numbering directly. Both documents build
with zero undefined references or citations, and all 16 headline results remain in the main paper.

The main paper keeps the newly proved corner figures, gamma-trap, unsplittability of b and corner
parallelogram: they are short, general, and the gamma-trap is what explains why [BeesonIII, Lem. 6]
is false as quoted, which is a headline correction. Four references that used to point into the
"e >= 2 residue" remark now point where they belong -- two at those new propositions, two at the
companion.

The companion carries a section recording what is DEAD on this branch, so it is not retried: the
entire class of linear direction invariants and the metric bounds derived from them; closing e = 1
by proving R >= 2 on every side; boundary tile counts; and the far side of the mismatch ray.

Corrections

• thm:frontier cited theorems this paper refutes. Its dependency list read
  [BeesonIII, Thms. 3, 7, 11, 14, 17, 19] without qualification, while the paper shows Thm 14's
  conclusion FALSE and Thm 19's proof unsound -- a visible circularity in the headline record.
  Narrowed to the tiling equations only, with an explicit note that the g|M conclusions are not
  used and that rem:colouring re-derives the equations citation-free.
• lem:cancel's proof had an overhang gap. It worked with maximal straight segments, where a
  tile edge can extend past the segment's endpoints. Restated via the common refinement into
  minimal pieces, which removes that case; the non-edge-to-edge step is now airtight.

A dead end, recorded

Counting tiles that meet the boundary and comparing against N does not work. Measured on the
certificates: 28 of 44 and 44 of 99 tiles touch the boundary -- a falling fraction -- and the
overlap between sides is 7, not the 5 that corner tiles alone would give. The comparison never
bites.

Record and headline unchanged: every N <= 69 settled, 70 the sole gap below 80, no triangle can be
cut into 19 congruent triangles.

v2.57 — walk structure at m=1, in a regime

The e = 1 walk reduction is generalised to a regime, and a defect in the vertex census is fixed.

New theorem (machine-checked, axiom-clean, lean/BaseBetaWalkArith.lean)

At m = 1, with gcd(e,f) = 1 and 1 <= e < f:

(i) if f^2 > 2e^2, each equal side carries NO b-edge; its edges are a's and c's with
n_a = fk and n_c = f - ke >= 1, and it ends with a c-edge at the apex;
(ii) if f^2 > 2ef + e^2 (equivalently f/e > 1 + sqrt 2), the base carries EXACTLY e b-edges,
with n_a = fl and n_c = e(2 - l), l in {0,1}. So R_base is e or 2e.

Both hypotheses are sharp. n_b = 2f on an equal side is admissible exactly when f^2 <= 2e^2, and
n_b = e + f on the base exactly when f^2 <= 2ef + e^2 -- the latter because
(f+e)^2 (f-e) = e(3f^2 - e^2) + f(f^2 - 2ef - e^2).

The two competing equal-side solutions die for different reasons, which is what makes the gamma-trap
load-bearing here: n_b = f forces (n_a, n_b, n_c) = (e, f, 0), a walk with no c-edge, killed by the
gamma-trap; n_b >= 2f is simply too long.

Coverage among the 42 base-beta prime candidates below 1000: 28 satisfy (i) -- including the thick
values 23, 131 and 167, since (i) needs only f/e > sqrt 2 -- and 17 satisfy (ii). The previous
result covered only e = 1, which is 7 of them. Cross-checked by enumerating all walk solutions for
the 198 coprime pairs with f <= 25: zero discrepancies.

Stated honestly: the theorem structures these cases, it does not by itself exclude any of them.

Correction

The vertex census in rem:e2 read Q_013 = 1 + P_320 + 2 Q_640 + Q_431. That omits the interior
vertices at which some tile is met in the relative interior of one of its edges: such a tile
contributes a straight angle, so the remaining tile angles sum to pi rather than 2pi and the figure
is (3,2,0) or (1,1,1). These types are not optional -- the dissections here are not edge-to-edge --
and this is the same assumption behind two earlier retractions in this paper. Corrected to
Q_013 = 1 + P_320 + 2 Q_640 + Q_431 + W_320, with the companion count likewise. The extra types only
enlarge the feasible set, so the "Euler carries no information here" conclusion is unaffected.

Record and headline unchanged: every N <= 69 settled, 70 the sole gap below 80, no triangle can be
cut into 19 congruent triangles.

v2.56 — gamma-trap proved; e=1 reduced to one walk

Two structural facts that were unproved heuristics are now theorems, and the e = 1 subfamily is
reduced to a single walk.

Proved (arithmetic backbone machine-checked, axiom-clean, lean/BaseBetaCorners.lean)

Corner figures. The angle relation at a corner splits into two integer equations. A base corner
(angle beta) admits only (p,q,r) = (0,1,0) -- a SINGLE tile presenting beta, with edges a and c
there. The apex (angle 3*alpha) admits only (3,0,0) -- exactly three tiles, each presenting alpha,
with edges b and c. In particular no corner of the target carries a gamma.

The gamma-trap: every side carries at least one c-edge. Each a- or b-edge is incident to gamma
at exactly one endpoint; each interior junction absorbs at most one gamma; and no corner carries
one. So a c-free side forces the chain E_1 -> J_1, then E_2 -> J_2, and inductively E_n -> J_n --
a corner. Contradiction. The corner hypothesis is essential, and is precisely why [BeesonIII,
Lem. 6] is false as quoted: on the tile-similar target a corner IS a gamma, the chain terminates
harmlessly, and the known counterexample has two c-free sides.

b is unsplittable, and hence the corner parallelogram: the base-corner tile's b-edge is a
chord with both endpoints on the boundary, so no edge can straddle it without leaving the triangle;
unsplittability gives a single matching tile, and the gamma-cap forces alpha and gamma interchanged.
Consequently the first two edges of each side at a base corner lie in {a,c}. Checked against both
genuine certificates before being proved: 6/6 sides, and 4/4 corners give c to exactly one of their
two sides.

The e = 1 subfamily reduces to one walk

For e = 1, m = 1, f >= 3 -- the candidates N = 3f^2 - 1, including 11, 47, 107, 191, 431, 587 and
971 below 1000 -- the equal sides carry no b-edge and begin and end with c (so R >= 2 there), and
the base carries exactly one b-edge and exactly one c-edge and begins and ends with a. The base walk
is therefore a permutation of (a^f, b, c) starting and ending with a, with b in position 3..f.
Arithmetic verified by enumeration for f = 3..12.

A plan corrected

Closing e = 1 by proving "R >= 2 on every side" does not work: R >= 2 is false at the base. The
walk with R = 2 is exactly the one the corner parallelogram kills, and the survivor has R = 1. On
the base, "R >= 2" is a restatement of the remaining problem rather than a reduction of it. It does
hold on the two equal sides, and is proved there.

Record and headline unchanged: every N <= 69 settled, 70 the sole gap below 80, no triangle can be
cut into 19 congruent triangles.