Periodic Orbits in Triangular Billiards
Fire a ball around a triangular table. Does some path always come back to where it started?
In plain terms
Take a triangle, treat it as a frictionless billiard table with no pockets, and send a ball off in some direction. It bounces off the walls forever, angle in equals angle out. A periodic path is one that eventually returns to its starting point travelling in its starting direction, and so repeats the same circuit for ever after.
Does every triangle have one? For a triangle with all angles under 90° the answer has been known since 1775: join the three points where the altitudes meet the opposite sides, and that inscribed triangle is itself a bouncing path. For a very flat triangle — one thin sliver with a nearly straight angle — nobody could construct a single such path, and for a long time nobody could prove one existed.
It sounds like a puzzle. It is on a short list of the most stubborn problems in dynamical systems.
What is known
Right triangles were settled in the early 1990s. Triangles whose angles are all rational multiples of a full turn were settled earlier still, and for a strong reason: rational angles mean the ball only ever travels in finitely many directions, which collapses the problem onto a surface where periodic paths are plentiful. Irrational angles destroy that structure completely.
The obtuse case was pushed forward by computer. Richard Schwartz, with a program called McBilliards, proved in 2009 that every triangle whose largest angle is at most 100° has a periodic path. In 2018 Garber, Marinov, Moore and Tokarsky extended the same style of argument to 112.3°, and reported that the method runs out of road at about 112.5°.
The mechanism behind those results is worth stating, because it is what makes the problem computable at all. Instead of reflecting the ball off a wall, reflect the table and let the ball travel straight. A candidate path is then just a straight line through a chain of mirrored copies of the triangle, and the sequence of walls it crosses — a word — either works or does not. Crucially, if a word works for one triangle it works for all nearby triangles too, so each word certifies a whole patch of the space of triangles. The conjecture becomes a tiling problem: cover the space of triangles with patches.
In June 2026 Giovanni Forni posted a preprint claiming the whole thing — that the billiard flow in any polygon has a periodic orbit. It has not been through peer review, and it is a proof by contradiction: it produces no actual path for any actual triangle. If it holds up, the existence question closes and the constructive question stays wide open.
Why it is hard
Everything easy about the problem comes from angles being rational, and the open case is exactly where they are not. The reflections generated by an irrational-angled triangle form an infinite group, so the unfolded picture never closes up, and there is no surface to hide behind.
The computer-assisted approach hits a different wall. As the obtuse angle grows, the patch certified by each word shrinks and the words needed get longer, so the search cost climbs while the ground covered falls. The two computer proofs to date read as a race between those quantities, and past roughly 112.5° the race is lost. Schwartz's deep searches also found parameter points around which infinitely many patches accumulate without ever covering a neighbourhood, which means no finite word list can finish the job by itself.
What a breakthrough would mean
Nothing practical, and the honest answer is that this problem is studied because it is a clean statement about an unclean object: the long-run behaviour of a system that is neither chaotic nor integrable. Polygonal billiards sit exactly on that boundary, and the tools for the boundary are thin. Anything strong enough to settle triangles constructively would be a tool for that whole regime — which is why the problem earned a place on Katok's list of most resistant problems in dynamics rather than a place in a puzzle book.
In this lab it is a new attack surface, added because the unfolding framework turns a dynamics question into exact arithmetic over the angles: a word either certifies a region of triangles or it does not, and the answer is a rational computation with no floating point anywhere. That is the kind of claim this lab can check. Nothing has been tried here yet.
What this lab tried
Standing: Evidence Word-census route mapped blind to length 26: 376 exact certificates (family orbits to length 66, gamma <= 160 deg), coverage staircase stalling at 135 deg, and a measured hyperbolic (not super-exponential) growth of needed word length vs angle - but certified box width collapses exponentially in length, so length buys angle reach, not area. Negatives are sample-bounded; skeptic-confirmed with one numeric correction.
Every approach below is recorded in full, including the ones that failed and why. Attempt titles link to the complete record.
Attempt 001blindEvidence
Canonical word census to length 26 with 376 exact certificates: coverage staircase stalls at 135 deg, blind rediscovery of the ~112.5 deg frontier, and a hyperbolic certificate-length growth law along the W(a,b) family (checked to length 66).
- Range checked
- canonical translation words of even length <= 26 (17,527 words); 1/64-cell midpoint screen of the obtuse half-disk; exact dyadic-box anchors; family rows to W(8,8), gamma <= 160 deg
- Open gaps
- sample-bounded-negatives
- death-angle-laws-unproven
Attempt 002blindVerified, with corrections
From-scratch re-implementation of every layer confirms 001 (36/36 sampled certificates at 180 exact apexes, 17,527-word universe reproduced word-for-word, death law survives two out-of-sample prediction rows); certified-area figure corrected to ~4.3e-6.
- Verifies
- attempt 001
- Corrections
- certified-area total over all 376 anchors is ~4.3e-6, not ~2.2e-6 (which is the map-anchor subtotal)
- the 64.3% uncovered figure is of the resolved interior, not the whole obtuse region
- anchor simulation re-derivation is at the anchor centre; the full 9-sample box attack ran on every 5th/7th record
- kill-condition verdict is measured only to gamma ~ 160 deg; beyond that the hyperbolic form is the SPECULATION law's extrapolation
Attempt 003informedVerified
The W(a,b) death-angle laws of 001 survive both out-of-sample tests (W(10,9) -> 162.90, W(12,12) -> 2160/13, to ~1e-12), and are then derived: exact division-free unfolding gives closed-form binding functions, a general law gamma_d = 180 - 90(a+b)/(a(b+1)) (confirmed out-of-sample on W(5,3) -> 144 and W(4,2) -> 135), and a machine-certified necessity theorem: the corridor is empty at every gamma >= gamma_d, for 15 verified members.
- Range checked
- necessity theorem machine-certified for the 15 members (2,1),(2,2),(3,2),(3,3),(4,2),(4,3),(4,4),(5,3),(5,4),(5,5),(6,6),(7,7),(8,8),(10,9),(12,12); exact alive certificates at gamma_d - 1e-6 (1e-8 for (3,3),(4,2)) for 8 members; float deaths measured to ~1e-11 for 11 members; parametric statement for all a >= b >= 1, a >= 2, a <= 2b+3 rests on two per-member-verified inputs (identities I1-I3 and Lemma C) labelled SPECULATION in general
- Open gaps
- sufficiency-limit-unclosed (death = gamma_d exactly needs alive points approaching gamma_d; certified alive stops at gamma_d - 1e-6)
- parametric-identities-unproven-in-general (I1-I3 and Lemma C verified per member, 15 members; general (a,b) statement labelled SPECULATION)
- a-greater-than-2b+3-uncovered (branch analysis breaks; W(6,3)-type members unmeasured)
Attempt 004informedVerified, with corrections
From-scratch re-verification confirms 003 end to end: glide reduction and mod-360 case tree re-derived by hand (1.9M-point adversarial sign search, zero dropped-branch hits), I1-I3 re-proven in an independent ring plus an off-torus grid-interpolation proof for W(2,1), Lemma C re-certified with an independent interval stack (4 members), all 8 exact alive certificates match digit-for-digit, four out-of-sample deaths re-measured to about 1e-12, mirror-half windows confirmed; two wording-level corrections, nothing load-bearing refuted.
- Range checked
- identities and glide facts re-proven for all 15 members (own ring; proof-grade off-torus grid for W(2,1); 20 exact spot points each); Lemma C re-certified for (2,1),(5,3),(10,9),(12,12); case tree searched at 1.94M adversarial points across all 15 members; all 8 exact alive certificates re-verified; deaths re-measured for (10,9),(12,12),(5,3),(4,2) plus calibration (2,1),(3,3); dead hunts at gamma_d + {0..0.5} deg for 4 members
- Verifies
- attempt 003
- Corrections
- the W(5,3) exact alive certificate is at gamma_d - 1e-6, not the gamma_d - 1e-8 stated in 003 section on the general law (the Outcome/range/Death-brackets statements are correct; only that one sentence is wrong)
- 003 Outcome bullet corridor is empty at every gamma >= gamma_d overstates the theorem: it proves no positive width; a zero-width touching corridor at gamma_d is not excluded (alive is defined as positive width throughout, so nothing downstream is damaged)
Attempt 005informedVerified
Death law completed on both sides: the half word composes to R_0 Rot_A(2a.alpha) Rot_B(-2b.beta), so I1-I4 and the glide facts become one exact 4-variable Laurent check valid for ALL (a,b); Lemmas C and D fall to an elementary c.cot(cs) monotonicity; the case tree is closed for all a >= b >= 1, a >= 2 (the a <= 2b+3 restriction removed); and certified alive segments into the death corner give death(W(a,b)) = gamma_d(a,b) EXACTLY (sup not attained) for 20 members including the newly measured W(6,3), W(6,1), W(8,2), W(8,1), W(7,1).
- Range checked
- I1-I4, D1, D2 and glide facts proven for ALL integers a, b >= 1 (formal ring; specialization cross-checked exactly on 23 members, floats to a = 40); Lemma C proven for all a >= 2, 1 <= b <= a and Lemma D for all b >= 1; necessity theorem for all integers a >= b >= 1, a >= 2 (no upper restriction on a); exact death = gamma_d certified for 20 members via alive segments t in (0, 1/4], gamma sweeping [gamma_d - 1/4, gamma_d); new float deaths for (6,3),(6,1),(8,2),(8,1),(7,1) at gamma_d to ~5e-12; adversarial case-tree scans ~1.56M points over 13 members
- Open gaps
- parametric-sufficiency-open
- a-equals-1-column-unmeasured
- birth-side-unproven
Attempt 006informedVerified
The 135 deg stall dissolves: 001 pinch gap was a sampler artifact (W(4,3) certified alive at gamma in (135.0000001, 135.048)), births obey a closed form gamma_birth = 180 - 90(a+b+1)/(a(b+1)) making staircase windows touch, the never-measured W(5,2) and a genuinely new four-block word are certified alive at gamma EXACTLY 135 (rational apexes on the arc, exact orbits), and the W family covers all 157 sampled obtuse arcs - while the design screens (3000+ canonical doubled words to length 50) find nothing of length <= 26 alive past 135 and show clean angle laws are confined to W's two-fan factorization.
- Range checked
- five exact certificates (rational apexes, Fraction corridors, independently simulated orbits): W(4,3) at certified gamma in (135.001,135.048) and (135.0000001,135.001); W(5,4) at (144.0000001,144.001); W(5,2) len 30 and non-W four-block N1 len 46 at gamma exactly 135 (exact on-arc identity); 003 obligations machine-certified for two new members (5,2),(6,2). Float screens sample-bounded: 245 canonical doubled words len <= 26 dead at 13 arcs >= 135; 811 len-30 words (only W(4,3),W(5,2) alive on 135-144); 2008 two-alternating words len 34-50 (only W members + two four-block words); three-block family a,b,c <= 3 (25/27 dead everywhere obtuse); birth law float-checked at 11 members; coverage checked at 157 arcs 90.5-165
- Open gaps
- birth-law-unproven (gamma_birth closed form is float-fitted + factor-structure motivated; no necessity/sufficiency theorem)
- coverage-conjecture-open (union of windows covering (90,180) reduces to an elementary Diophantine statement, unproven)
- length-26-stall-sample-bounded (doubled words only, 13 arcs; non-doubled even words 24-26 not rescreened)
- four-block-death-angles-uncharacterized (binding differences provably non-elementary here only by failed factor search)
Attempt 007informedVerified, with corrections
From-scratch re-verification confirms 006 everywhere it is exact: all five certificates re-established by a third corridor implementation (digit-for-digit widths) plus an own exact simulator, the exactly-135 on-arc identity re-derived by hand, 001's pinch-gap birth value regenerated from a replica of its own sampler (mechanism: the alive window is a corner sliver inside the grid's terminal 6e-4 clearance), the birth law survives three genuinely out-of-sample members to ~3e-11 (= sampler floor, including a > 2b+3), and the (5,2)/(6,2) theorem extension re-proves in an independent ring; four corrections, none load-bearing.
- Range checked
- all 5 exact certificates re-verified (own matrix-form exact corridor, widths match digit-for-digit; own exact orbit simulation; own certified gamma brackets via 004's interval stack; on-arc gamma=135 identity hand-derived and Fraction-checked; Niven applicability checked); W(4,3) birth floor-tracked at 4 sampler depths; 001's census sampler replicated (reproduces 135.0486) and window x-extent measured at 7 gammas; birth law tested out-of-sample on W(7,3), W(6,3), W(8,2) (all +3.0e-11 = floor, dead-sampled below); coverage re-run at 25 own arcs (25/25 alive); universes recounted (245 and 2008 confirmed, 566-vs-811 correction); s1 hits reclassified (14 W + N1/N2); N1/N2 non-W checked incl. 0-1 swap; 60-word random dead re-test + 19 near-miss attacks (zero kills); identities + case tree (550k points) + Lemma C re-certified for (5,2),(6,2). NOT re-swept: full length-30 and s1 negative universes, three-block table, design_factor.py factorizations
- Verifies
- attempt 006
- Corrections
- universe counts: the length-30 (|u|=15) universe is 566 canonical words, not 811 (811 is |u| <= 15 cumulative); 'all doubled odd words to length 30: 1056' double-counts (true count 811); the index one_line's '3000+' is 2846 counted correctly - screen coverage itself is unaffected
- 'length 30 is alive throughout the measured gap' overstates: certificates prove alive points AT gamma = 135 exactly and at one gamma in each of (135.0000001, 135.001) and (135.001, 135.048); the continuum statement is float evidence plus the SPECULATION window law
- refutation semantics vs 001: 001's gap claim was knowledge-scoped ('nothing <= 30 KNOWN alive') and stays true as written; what 006 overturns is 001's birth measurements (error 0.0486 deg, 10x the stated ~0.005 sampling noise, whose 'deaths only under-estimated' hedge does not transfer to births) - correction/closure, not refutation
- the window pairing (a,b) <-> (b+1, a-1) is a canonical-word identity (0<->1 swap + rotation/reversal; verified exactly on six pairs), so it is vacuous as evidence for the birth law, 006's 11-member fit spans only 9 canonical words, and 003's 'two distinct words dying on the same arc' (W(3,3)/W(4,2)) is a relabeling of one canonical word
Attempt 008informedVerified, with corrections
Adversarial re-verification confirms 005 end to end: the closed-form bridge u = R_0 Rot_A(2a.alpha) Rot_B(-2b.beta) recomposed exactly at off-torus rational points (40 members to a = 40), I1-I4 and glide facts re-proven in an independent 4-variable ring with u re-derived by symbolic map composition, Lemmas L1/C/D re-derived by hand and stressed to a = 10^6, the extended case tree re-derived branch by branch (threshold identity exact; 447k-point scan on 10 a > 2b+3 members, zero hits), the sufficiency segments independently certified alive by full-corridor interval unfolding down to gamma_d - 9.3e-10, and all five new deaths re-measured on the mirror half; one numeric correction, nothing load-bearing refuted.
- Range checked
- bridge recomposed exactly for 40 members incl. (40,40) at 2 rational points each; identities re-proven formally (my ring, 14/14); Lemma numerics 14,183 checks to a = 10^6; case tree scanned at ~447k adversarial points over 10 members with a > 2b+3 (k up to 2 reachable); segments certified alive at 42 points (7 members incl. the 5 new, t down to 2^-30); plaw_suffice trig layer audited (596 enclosure checks); 5 deaths re-measured with 004's sampler; plaw_suffice all NOT re-run end to end (selftest + one member reproduced, code audited)
- Verifies
- attempt 005
- Corrections
- 005 states the five new exact-alive certificates certify gamma within 1e-6 of gamma_d; the data files show gamma_d - 1e-4 for W(6,3), W(8,2), W(8,1), W(7,1) (only W(6,1) reaches 1e-6) - the --dg 1e-6 request is a float target, the certified bound is the largest 10^-k that certifies after apex snapping
- caveat, not an error: the five new members' necessity rests on the parametric theorem alone (no per-member deathlaw_prove obligations were run for them, unlike 003's fifteen); sound by design since the identities are now proven for all (a,b)
Attempt 009informedFormalized
First Lean 4 certificate in the lab: Lemma L1 of 005 (c.cot(cs) strictly decreasing on (0,1] for fixed s in (0, pi/2]) proved in mathlib with zero sorries and only the three standard axioms, statement matching 005 hypothesis-by-hypothesis with no narrowing; independent statement review and independent rebuild still pending.
- Range checked
- exactly the formal statement StrictAntiOn (fun c => c Real.cot (c s)) (Ioc 0 1) for all real s with 0 < s <= pi/2 (Lean 4.32.2, mathlib v4.32.2); Lemmas C and D themselves, and the I1-I4 Laurent block, are NOT formalized
- Verifies
- attempt 005
- Open gaps
- laurent-block-I1-I4-not-attempted (queue item 16 second half)
Attempt 010informedVerified
Independent completion of the FORMALIZE.md pass on 009: non-formalizer statement review finds cot_lemma_L1 matches 005's Lemma L1 hypothesis-for-hypothesis with no narrowing (StrictAntiOn/Ioc/Real.cot read from vendored mathlib source, no junk-value reliance, cheat scan clean), own fresh lake build after deleting the project build output is green with axioms exactly [propext, Classical.choice, Quot.sound], and all three of 005's L1 use sites instantiate inside the formalized hypotheses; zero corrections, two cosmetic nits.
- Range checked
- statement fidelity vs 005 section (ii)-B checked hypothesis by hypothesis; definitions Real.cot, StrictAntiOn, Set.Ioc read from mathlib rev 905b958 source; cheat scan over both project .lean files; rebuild = rm -rf .lake/build + lake build (8657 jobs, green) in a fresh container session with the pinned toolchain, mathlib oleans from the existing pinned cache (not re-downloaded); own axiom audit of both theorems; usage check of all three L1 call sites in 005. NOT audited: mathlib internals beyond the definitions used, Lean kernel, Lemmas C/D themselves
- Verifies
- attempt 009
Attempt 011informedFormalized
Second Lean 4 certificate: the full Laurent-identity block of 005 - closed-form half-word composition R0.RotA(2a alpha).RotB(-2b beta), I1-I4, D1, D2 and the glide facts - kernel-checked with (a,b) as formal exponent variables (23 theorems, zero sorries, standard three axioms only), tiers A+B+C green plus the letter-word iterate version for all natural (a,b); the block turns out homogeneous in i (no i^2 = -1 needed); geometry bridge out of scope per the lane, statement review pending.
- Range checked
- exactly the formal statements in formal/BilliardsFormal/LaurentBlock.lean: the identity block over an arbitrary field K with nonzero generators x, y, P, Q, i and 2 != 0 (P, Q carrying the (a,b) exponents formally; Tier C specializes P = x^a, Q = y^b for all integers a, b; half_word_letters covers the genuine letter word for all natural a, b); Lean 4.32.2, mathlib v4.32.2, axioms exactly [propext, Classical.choice, Quot.sound]
- Verifies
- attempt 005
- Open gaps
- geometry-bridge-not-formalized (ring model = unfolding geometry carried by 005/008, out of scope by design)
Attempt 012informedVerified
Independent completion of the FORMALIZE.md pass on 011: non-formalizer statement review confirms all 23 Lean theorems say what 005's Laurent block says (definitions, angle dictionary, signs, conj-as-substitution = 008's star involution, pair encoding assumption-free, i-drop safe, no nat-vs-int narrowing, v2's Q genuinely absent in 005 too); every theorem re-proven in an own 7-variable symbolic ring with i formal (31/31 exact zero polynomials, independently confirming the i-homogeneity), D1 additionally re-derived by hand, statements matched to 005's prose at 200 random points to ~4e-15; own fresh lake build green, own axiom audit of all 23 theorems exactly the standard three; zero corrections, three cosmetic nits.
- Range checked
- statement fidelity of all 23 theorems in formal/BilliardsFormal/LaurentBlock.lean checked against 005 (ii)-A Steps 2-4 and plaw_general.closed_forms definition by definition; every theorem re-proven symbolically in an independent stdlib ring with i as a formal Laurent variable (half_word_letters re-composed by symbolic iteration for a,b <= 3); Lean-to-005 mapping float-checked at 200 random (a,b,alpha,beta), a <= 12, 30 quantities; cheat scan over all four project .lean files; rebuild = rm -rf .lake/build + lake build (8658 jobs, green, LaurentBlock re-elaborated 41 s) in a fresh session with the pinned toolchain and mathlib cache; own axiom audit of all 23 theorems from an own scratch file. NOT audited: the geometry bridge (permanent certificate scope, carried by 005/008), Lemmas C/D and the analytic layer, mathlib internals, the Lean kernel
- Verifies
- attempt 011
Attempt 013informedVerified
The coverage Diophantine sublemma of 006 is closed: every t in (0,1) admits integers a,b >= 1 with a+b < t.a(b+1) < a+b+1, by an elementary overlapping-interval-chain proof (no continued fractions needed) with constructive witness q = floor(1/t)+1, a = floor((q-1)/(qt-1))+1, b = q-1 - so, conditional SOLELY on the SPECULATION birth/window law of 006, every obtuse angle lies strictly inside some W(a,b) window; the load-bearing open problem for coverage is now entirely the birth theorem (queue 11).
- Range checked
- proof re-derived step by step from an unverified external handoff (each equivalence machine-checked exactly); constructive witness verified for ALL 27,397 reduced rationals with denominator <= 300 in two independent arithmetic layers (formula-free integer brute force cross-checks denominator <= 60), 2,494 exact window-endpoint adversaries, denominators to 2e50, 2,000 random rationals to 1e40; consistency: witness at gamma = 135 is exactly 006's certified W(5,2). Lemma is unconditional; billiards meaning is conditional on the unproven birth law. Novelty searched, none found - recorded as elementary/likely folklore, not new mathematics
- Open gaps
- skeptic-pass-pending (proof not yet adversarially reviewed; lead 1 lists the attack surface)
- birth-law-still-speculation (coverage conjecture inherits it; queue 11 is the sole blocker)
- minimal-witness-staircase-open (constructive witness provably suboptimal, up to x15 in a+b on 006's grid; continued-fraction law still unproven)
Attempt 014informedVerified
Skeptic pass on 013 (confirmed with corrections): the coverage Diophantine lemma, its proof, its constructive witness, and the committed checker all survive - every step re-derived by hand incl. the strictness edge cases and a cleaner minimal-a0 closure of the union-endpoint worry, a from-scratch implementation written from the record's formulas alone reproduces every count (27,397 Farey witnesses, 21,539 overlap pairs, x15.33/x1.88 overshoot) and diffs witness-for-witness with zero mismatches, the novelty label holds after two fresh searches - but two prose errors are corrected: the gamma=144 spot-check names W(4,3), which is not a witness there (the checker itself says W(11,2); W(4,3) is never the constructive witness for any t), and the Step 2 parenthetical's inclusion I(q-1,q) in (1/q,2/q) is false (the interval is disjoint from it, lower endpoint exactly 2/q). Neither is load-bearing; queue 12's Diophantine side is closed for real.
- Range checked
- all four proof steps re-derived by hand from 013's prose incl. both integer edge cases (1/t integer, (q-1)/(qt-1) integer) and the automatic a >= q; union argument re-proven via minimal-a0 and machine-checked at 27,810 points incl. every lower endpoint a in [q, q+80], q <= 60; independent implementation (written before reading the committed code) re-runs every numbered check with different structure and seeds, zero failures; witness diff on all 27,397 reduced rationals r <= 300, zero mismatches; committed selftest re-run green (73,542 checks); novelty re-searched with two disjoint queries. NOT re-examined: 006's birth/window law (stays SPECULATION), the pointwise-vs-arc question (007 C2 stands), the minimal-witness staircase (open, 013 lead 3)
- Verifies
- attempt 013
Attempt 015informedVerified
Queue 11 broken open: every W(a,b) gate margin has a closed form (pivot +/- sidelengthsin(linear form); ring-verified bijectively, 25 members), the birth edge is the N2/PB double wall at (90/a, 90/(b+1)) so 006's birth law gamma_birth = 180 - 90(a+b+1)/(a(b+1)) is the second corner of a two-wall system - and birth-side NECESSITY (alive => theta < theta_birth) is PROVEN for all a >= b >= 1, a >= 2 by a five-step sign-constant-progression pigeonhole (worker-drafted, director re-derived with one repair); with 005's death necessity the window is contained in the law for every member. Sufficiency: two canonical segments (death rho=2, birth diagonal) jointly realize every theta in the window; certified in exact interval arithmetic for ALL 104 members a <= 14 - the full window law EXACT for that range - float-verified to a = 60 (1,829 members, zero failures) with the sharp wall t = 45/(a(b+1)) explaining 005's rho=2 uniformity. Remaining for ALL (a,b): seven elementary fan-margin lemmas, each with a swarm-drafted proof (SPECULATION until re-derived; N1 - the hardest - and four more ARE director-verified). Coverage of (90,180) via 013 is now a theorem for every gamma whose witness has a <= 14, and conditional on exactly those seven lemmas beyond.
- Range checked
- closed forms exact-ring-verified (bijection onto the engine's distinct diffs) for 25 members to W(15,7); T2 birth necessity proven for all a >= b >= 1, a >= 2 (elementary, no intervals; worker draft re-derived in full, Step-5 m>=1 branch repaired by the director); window = (gamma_birth, gamma_d) exact for all 104 members a <= 14 by certified interval arithmetic on both canonical segments (t in (0, 22.5/(a(b+1))], N1 via derivative+bisection, tau nonzero certified); float evidence to a = 60 both segments + 3,200-pair window coverage + 468k-sample adversarial birth-side scan, zero anomalies; 5 of 12 parametric lemma families director-verified (N1 k=1/2 incl. its N1'(0) sub-lemma, T2, AB_a, B-BA, rational ranges), 7 remain worker-drafted SPECULATION with claimed ranges covering k = 1/2. NOT: coverage as a theorem beyond a <= 14; arcs-as-intervals (007 C2 stands); a = 1 column; window endpoints
- Open gaps
- seven-fan-margin-lemmas-worker-drafted-unverified (S-rows of section 5; each <= 2 pages elementary trig; verifying all seven closes coverage for ALL obtuse angles)
- closed-form-endpoint-bookkeeping-not-formalized-for-all-ab (25-member exact check + hand derivation; do the 4-variable-ring pass like plaw_general did for I1-I4)
- skeptic-pass-pending (this record; queue top)
- birth-edge-touching-open (strictness at theta_birth itself, mirror of 004 C2)
Attempt 016informedVerified
Skeptic pass on 015 (confirmed with corrections) AND the queued main task done: all seven S-lemmas plus the tau row are re-derived from scratch (drafts never read - they are not in the repo) and PROVEN for all a >= b >= 1, a >= 2 at k = 1/2, so the window law window(W(a,b)) = (gamma_birth, gamma_d) and, via 013/014, coverage of (90,180) hold for ALL members - closing queue 11. T2 confirmed (with a one-line simplification of the a.alpha >= 90 branch: n = a gives sin(z_a) = -sin((b+1)beta) > 0 directly); N1 confirmed by a new derivative-free proof ((2b+1)cos(at)cos((2b+1)t) > ab.sin(90/a) via tan u >= u and sin(nx) <= n sin x); tau collapses to the closed form R = -4 sin(th) sin(a.al) sin((b+1)be), so tau != 0 is automatic at every alive point. Two record errors found, neither load-bearing: 015 SS1's s=0 C-image identity is -N1 not -N1-N2, and 015 SS4 overclaims - the death-segment BC0 (= N4) row is never evaluated by wmargins_certify.py (loop starts at j=1, no N4 leg); the row is true via 005's I4 and is certified exactly here (n4leg) for all 104 members a <= 14, and 015 SS5's reduction table is missing that N4-death family. Margin system independently validated: 1200/1200 sign agreements with 002's geometry, fresh 62-member exact ring bijection, 32 proof-step inequalities scanned to a = 3000 with zero violations, 453k-sample T2 adversarial scan clean.
- Range checked
- seven S-lemmas + tau + N1 + N4 + B-BA + AB_a proven for all a >= b >= 1, a >= 2, death and birth segments, t in (0, 22.5/(a(b+1))] (k = 1/2; D-AB/D-BC proofs reach k = 1); T2 re-derived in full for all (a,b); every proof step machine-scanned over all (a,b) with a <= 40 (96 t-points each) plus 20,000 random members to a = 3000, zero violations; margin system validated against 002's independent corridor geometry at 1200 random triangles a <= 12 and by exact ring bijection on 62 fresh members (union with 015: 67); T2 adversarial scan 453,605 beyond-wall candidates incl. 360-degree higher branches, zero alive; death BC0 = N4 certified exactly (ring identity + rational ranges) for all 104 members a <= 14. NOT covered: formal all-(a,b) endpoint bookkeeping (015's narrow SPECULATION stands, now 67-member exact + geometry-validated); this record's own proofs await their skeptic pass; a = 1 column; window endpoints; 007-C2 pointwise caveat
- Verifies
- attempt 015
- Corrections
- 015 SS1: 'the s=0 C-image margin is -N1-N2 (I1)' is false - the margin is exactly -N1 (max |AC0 + N1| = 3.2e-16 over 4000 random segment points; matches plaw_suffice's I1). Nothing downstream damaged
- 015 SS4: 'every margin sign on BOTH segments is certified in exact rational interval arithmetic' is overstated - wmargins_certify.py never evaluates the death-segment BC0 row (death B-fan C loop is range(1,b), no N4 leg; W(5,3)'s death_fan_leaves=13 vs 14 fan rows is the fingerprint). The row is true (BC0 = N4, I4's all-positive segment form) and is now certified exactly for all a <= 14 by wmsk015 n4leg; the a <= 14 window theorem stands
- 015 SS5: the reduction table is missing the N4-death family (a P row via I4 + rational ranges), and the '9 elementary lemma families' / 'seven S-rows' counts do not reconcile with the table's own 8 S rows (7 fan lemmas + tau) plus the omitted N4
- Open gaps
- skeptic-pass-pending (this record's seven proofs; attack surface pre-registered in lead 1)
- endpoint-bookkeeping-not-formal-for-all-ab (lead 2; the last SPECULATION under the coverage chain)
- birth-edge-touching-open (mirror of 004 C2)
- a-equals-1-column-unmeasured
Go deeper
Problem statement and published background · Full prior-art notes · Machine-readable index
Found something, or think we got it wrong?
Both are welcome, and the second especially. Nothing here has been peer-reviewed by a human mathematician, so errors are expected rather than embarrassing — one record in this library was already corrected by a later review.
Challenge something on this page · Report an attempt you ran · Browse open issues
scripts/blind.sh billiards-triangles ../workMore on blind and informed mode.