FORMALIZED rung + the 2026-08-04 cycle, merged with main (union-closed line renumbered 016/017) - #12
Merged
Merged
Conversation
…ERIFIED docs/FORMALIZE.md defines when a skeptic-confirmed proof step earns a machine-checked certificate, the statement-review step that carries the informal-to-formal bridge risk, and three pilot candidates from the current ledger. FORMALIZED enters the schema enum, the AGENTS.md vocabulary, the site badge/gloss tables, and the attempt template; problems/*/formal/ is registered tier 1. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…edure The skeptic pass now checks claimed-new results against the literature (rediscovery is recorded as rediscovery, with the citation), and CONTRIBUTING.md carries it as bar item 7. CYCLE.md step 4 points at the FORMALIZED escalation for load-bearing proof-shaped survivors. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
New current-guidance section (2026-08-04): ripple-scan the ten Astra results before other queue work, novelty gate and formalization lane adopted, portfolio note on preferring decade-open specialist-tractable targets with checkable deliverables. STATUS.md gets the dated insights entry, queue item 15 (ripple scan) and 16 (billiards formalization pilot), and a TL;DR process note. No mathematical state changed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…ment review pending First certificate of the docs/FORMALIZE.md lane: 005's Lemma L1 (for fixed s in (0, pi/2], c |-> c*cot(cs) strictly decreasing on (0,1]) proved in Lean 4 / mathlib v4.32.2, zero sorry, axioms limited to propext/Classical.choice/Quot.sound, prebuilt mathlib via lake cache. Review-shape record with the hypothesis mapping flagged pending independent statement review; formal/.lake is git-ignored. New mechanism tag machine-checked-formalization. test_records.py now skips .lake/ vendored docs in the missing-file lint. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…mplete Independent skeptic pass on the Lean pilot: statement fidelity vs 005's Lemma L1 confirmed hypothesis-by-hypothesis with no narrowing (Ioc, StrictAntiOn and Real.cot semantics read from mathlib source), vacuity/ cheat scan clean, root module confirmed to elaborate the theorem file, independent rebuild green with the reviewer's own axiom audit (propext, Classical.choice, Quot.sound only), all three L1 uses in 005 confirmed in-hypothesis. 009's two pending gaps closed in the index; 009's record untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
Ripple scan of the ten Astra results: zero hits across the portfolio; both flagged bites (Ehrhart vs mahler-4d, extremal/Ramsey vs erdos-gyarfas) recorded as reasoned misses, one conditional analysis-lens seed kept as SPECULATION in insights, two scan hazards recorded (name collision, Erdős numbering conflict). Formalization pilot closed: L1 certificate entry added to verified results, queue items 15/16 retired, new item 15 targets the I1-I4 Laurent block. GUIDANCE.md directives updated to completed state; ops notes on the Lean toolchain recorded in insights. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…n, review pending Second certificate of the FORMALIZE.md lane: 005's closed-form composition, the glide/translation facts, and identities I1-I4/D1-D2 proved in Lean 4 over an arbitrary field with (a,b) carried as actual powers of universally quantified generators; specialization corollaries included. 23 theorems, zero sorries, axioms propext/Classical.choice/ Quot.sound only, toolchain pins unchanged. Two findings recorded: the block is homogeneous in i (the i^2 = -1 hypothesis is never needed), and no Laurent-ring API is required (field_simp + ring_nf suffice). Geometry bridge explicitly out of scope; statement review and independent rebuild pending per the 009->010 precedent. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…ALIZED pass complete Independent skeptic pass, zero corrections: all 23 theorems mapped to 005 statement-by-statement (angle monomials, factor-of-2 conventions, signs and orientations all verbatim; permutation/sign-swap hunts came up empty), conjugation-as-substitution confirmed as 008's star involution with nothing smuggled (key theorems quantify over arbitrary pairs), dropped i^2=-1 confirmed safe-direction and independently re-proved with i as a formal variable, N/Z parameter coverage confirmed non-narrowing, cheat scan clean, independent rebuild green with own axiom audit. All 31 identities re-derived exactly in a from-scratch stdlib Laurent-ring engine (lbsk_review.py). Geometry bridge remains permanent out-of-scope carried by 005/008. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…keptic pending Queue item 1's probe-first step: the i-aggregated odds-ratio control survives every seeded attack at n <= 32 (013 anchor reproduced exact), but a replicated-witness ladder MU(n,r) with orbit-optimized shared unit weights drives the aggregate negative past n ~ 90: certified in exact rational arithmetic at t=4 (lambda=2) at n=96/128/160 with marginals <= 0.309 < 0.38271, enclosure widths <= 1e-18, dichotomy checks exact, sign robust to the alternative bookkeeping and 3% perturbations. Claimed ledger consequence (pending skeptic): the aggregated-control proof branch closes negative; the gap falls to the margin-modulated control and a lambda <~ c/n restricted variant. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…tions Fully independent confirmation: quantity re-derived from 007/013 prose and re-implemented from scratch (scaled-integer arithmetic, own log2 enclosure via interval squaring + directed dyadic rounding), hitting the 013 anchor digit-for-digit and re-deriving all three kill certificates to 18+ digits (n=96 enclosure strictly negative, width 1.3e-20). Family rebuilt atom-for-atom from prose; marginals and dichotomy certified as integer inequalities; positive controls confirmed and the surviving raw-weight ladder upgraded to certified +0.157. Corrections: C1 cosmetic (n=128 has 252 atoms, not 253); C2 real - the violation lives at lambda in [2,2.5], NOT in the 009/011 workable window (~0.05 at n=96), so the recorded forall-lambda gap is validly closed but the lambda <~ c/n restricted variant is untouched and stays live alongside the margin-modulated control. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…ed lines) TL;DR rewritten for the cycle headline (aggregated OR control refuted at large n, Laurent block formalized); union-closed and billiards problem rows updated; queue item 1 restated to the two surviving Gap-1 candidates with probe-first designs, old item 15 replaced by the kill-frontier follow-ups; verified-results entries added for the Laurent block (011/012) and the aggregated-control refutation (014/015); new dead-end entry for the unrestricted-lambda aggregated form with the ladder genre as reusable adversary; unit-replication insight recorded; GUIDANCE and FORMALIZE.md pilot list updated to completed state. Crouzeix blind line still pending integration. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
First attempt on the last untouched problem, run blind per the queue (worked in a blind.sh copy; prior art physically absent). 286-start census of the Crouzeix ratio at n=3, deg<=3 from seven structured start families, certified rational enclosures at every endpoint, zero refutations: all probe-surviving local maxima are known structure (13 ice-cream-cone points at ratio 1 - a blind rediscovery of Greenbaum-Overton's configuration, cited; 97 Jordan-type endpoints climbing to ratio ~2); all four intermediate candidates fell to deep escape-probing as optimizer stalls. Standing gap recorded: the published GO intermediate maxima are untested by this design. Merge adds the four mechanism-tag definitions per the blind-flow rule. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
Independent re-certification of 30/286 endpoints with a structurally different certifier (Sylvester-minor bisection, Bernstein segment bounds, own direction set) - all consistent, anchors to the last digit, denominator discretization confirmed conservative. All four intermediate-candidate stall verdicts re-confirmed with a corrected equal-sample-count probe protocol (001's 128-vs-512 comparison could manufacture ascent; verdicts survive at 512-vs-512). Corrections: near-2 class is 94 not 97 (partition now exact); index one_line's 'all certified below 2' overstated - the sound statement is 0 certified above 2; Calcolo 2021 / arXiv:2105.14176 is Overton alone; ascent figures precise; 2/13 ratio-1 maxima have near-flat multipeaks. Blind label accurate for prior-art absence; task framing was orchestrator-assigned (caveat recorded). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…tempted Crouzeix moves off 'no attempts': verified-results entry for the 286-start certified census (001/002) with the skeptic's corrected scoping (0 certified above 2; near-2 class 94), queue item 10 restated to the intermediate-maxima basin hunt (informed; the blind census is spent), TL/DR finalized, counts updated (25 verified results, ~56 tools, no unattempted problems). Two insights recorded: blind-mode data point #3 with the task-framing caveat, and the escape-probe sample-parity lesson. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011D7zA3zXd1mMPYsjz6RXqz
…on-closed line to 016/017 Two cycles ran the same queue item (union-closed queue 1, the mandated large-n probe of the i-aggregated odds-ratio control) in parallel, so both sides landed attempts numbered 014/015 and an engine called uc_or_agg_probe.py. main's pair merged first, so this branch's pair is renumbered and its engines renamed: attempts/014-aggregated-control-probe-large-n.md -> 016-... attempts/015-skeptic-review-of-014.md -> 017-skeptic-review-of-016.md explore/uc_or_agg_probe.py -> explore/uc_agg_ctrl_probe.py explore/uc_or_agg_probe2.py -> explore/uc_agg_ctrl_probe2.py explore/uc_or_agg_skeptic.py -> explore/uc_agg_ctrl_skeptic.py Only identifiers moved: no finding, number, or certificate in either record was altered. Internal cross-references, the engine imports, and the leak_terms follow the new names; the kill certificate re-runs identically after the rename (n = 96 ladder, A = -0.000759865186), and main's engine still reproduces its own cross-checks. The two lines are consistent: 014 certifies the aggregate positive at n <= 32, which is exactly where 016 also finds nothing; 016 kills the forall-lambda statement at n = 96-160 on a unit-replicated ladder 014's battery did not build. 014 gets superseded_by = 016 in the index, since its forward-looking call (proof effort now justified) is the part that does not survive; everything it certified stands. STATUS.md is merged by hand: both cycles' headlines, table rows, and verified-result entries are kept, the union-closed entries cross- reference each other, queue item 1 is rewritten around the kill while keeping the still-live structural questions from 014/015, and this branch's old queue item 15 becomes 18 behind main's maxwell items. python -m pytest tests/ -q: 196 passed, 7 skipped. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4KNG9XEbwSxgSuwwngZ9V
main gained two onboarded problems (almost-mathieu, three-phase- conductivity) with queue lines 18-19 while this branch was being reconciled. STATUS.md is merged by hand again: - both TL;DR paragraphs kept; this branch's "no problem is unattempted any more" is scoped to the problems carried at the time, since the two new ones have no attempts yet - the library-summary counts recomputed against the merged file rather than taking either side's: 28 verified results, 8 dead ends, 13 problems (11 attempted), ~84 tools - this branch's union-closed frontier item moves from 18 to 20, behind main's 18-19, so main's "queue 18-19" pointer stays correct python -m pytest tests/ -q: 208 passed, 7 skipped. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4KNG9XEbwSxgSuwwngZ9V
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Supersedes #9, which could not merge: both branches ran union-closed queue item 1 in parallel and both landed attempts numbered 014/015 plus an engine called
uc_or_agg_probe.py. This is #9's content with main merged in and the collision resolved.What this adds
Everything from #9 — the
FORMALIZEDverification rung (docs/FORMALIZE.md, schema enum, tier-1problems/*/formal/), the literature-novelty gate, the billiards Lean certificates (009–012), the crouzeix dim-3 census (001/002), and the union-closed large-n probe that kills the ∀λ aggregated control — plus main's parallel cycle (maxwell-equilibria 001/002, union-closed 014/015), reconciled.Problem: repo-wide, plus union-closed and billiards-triangles records
Mode: informed
Status claimed: unchanged from the records themselves (
FORMALIZED,REFUTED,EVIDENCE,VERIFIED_WITH_CORRECTIONSas each record states)The collision, and how it was resolved
main's pair merged first, so this branch's pair is renumbered and its engines renamed:
attempts/014-aggregated-control-probe-large-n.mdattempts/016-aggregated-control-probe-large-n.mdattempts/015-skeptic-review-of-014.mdattempts/017-skeptic-review-of-016.mdexplore/uc_or_agg_probe.pyexplore/uc_agg_ctrl_probe.pyexplore/uc_or_agg_probe2.pyexplore/uc_agg_ctrl_probe2.pyexplore/uc_or_agg_skeptic.pyexplore/uc_agg_ctrl_skeptic.pyOnly identifiers moved. No finding, number, or certificate in either side's records was altered; cross-references, imports and
leak_termsfollow the new names.The two lines are consistent. 014 certifies the aggregate positive at n ≤ 32 with the margin growing; 016 finds nothing negative at n ≤ 32 either, and kills the ∀λ statement at n = 96–160 on a unit-replicated ladder 014's battery never built. 014 therefore gets
superseded_by: "016"in the index — its forward-looking call ("proof effort now justified") is the only part that does not survive. Everything it certified stands, and its equality-set structure is what makes the λ-restricted variant the live question.STATUS.mdis merged by hand: both cycles' headlines, table rows and verified-result entries kept, the two union-closed entries cross-referencing each other, queue item 1 rewritten around the kill while keeping the still-live structural questions from 014/015, and this branch's old queue item 15 renumbered to 18 behind main's maxwell items.The bar
uc_agg_ctrl_skeptic.py --quickreproduces the n = 96 kill certificate (A = −0.000759865186, width 1.2e-20) anduc_or_agg_probe.py Xpasses main's cross-checks — the two lines' engines coexist inexplore/.SPECULATIONis labelled inline — unchanged from the records.VERIFIEDdescribes a range, not the conjecture — unchanged from the records.modeis honest — unchanged (informedon both union-closed records).main; leaving them at 014/015 would have collided with the records that had. main's records were not touched.prior-art.jsonupdated: both pairs indexed,verifieson 017 → 016,superseded_byon 014 → 016,leak_termsrenamed to match the engines.python -m pytest tests/ -qpasses: 196 passed, 7 skipped.What is not claimed
That the merge adjudicated the mathematics. It did not re-run either probe's full battery (round 2 alone is ~30 min plus drills) and it did not test the one thing that would settle the pair outright — running 014's battery against 016's MU(n,r) ladder. The claim here is narrower: the two records' scopes do not overlap where they disagree, and each reproduces its own headline certificate under the new names. The
superseded_bylink and the merged STATUS prose are an editorial reading of two independently skeptic-confirmed records, not a new result.Obstruction / open gaps
The minimal violating n is still bracketed (32, 96] — queue item 18. The λ ≲ c/n window-restricted variant and the margin-modulated control are untouched by the kill and are queue item 1.
Generated by Claude Code