Add the FORMALIZED verification rung: a Lean-certificate lane above VERIFIED - #9
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
Merged
9 tasks
Owner
Author
|
Closed in favour of #12, which is this branch's content merged with The conflict was not textual: a parallel cycle ran the same queue line (union-closed queue item 1) and landed its own attempts numbered 014/015 plus an engine called The two lines turned out to be compatible: 014 certifies the aggregate positive at n ≤ 32, 016 finds nothing negative there either and kills the ∀λ statement at n = 96–160 on a ladder 014's battery never built. 014 carries Generated by Claude Code |
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.
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