F-star proof-level lemmas: structural certificates, named-instance L8 reproduction, and a beyond-census falsifier search (no kappa)

research/fstar-proof-lemmas-seed3096ed3f/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "research/root-unit-decoder-lemmas/README.md",
+      "usage": "input",
+      "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb",
+      "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9"
+    }
+  ]
+}

research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md

@@ -0,0 +1,10 @@
+Task ID / proposed scope key: KB5-fstar-proof (explicit open request, kappa-blocker KB5; drawn card replay-runtime/portable-replay discarded as saturated)
+Base commit; exact predecessor and dependency heads: 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2; predecessor https://github.com/CrocSwap/integer-mult-bounds/pull/2335 head 856cd760 (F-star census); named instances from https://github.com/CrocSwap/integer-mult-bounds/pull/2111 head 98da76c2 (tied_min, cex_min_1)
+Concrete object and question: open problem F-star of research/root-unit-decoder-lemmas section 7: cert(M) >= floor(2v/3) for every exact 3-total rational decoder. Move from census-level witnesses to proof level: (P1) PROVEN structural lemmas with exact hypotheses (support-forced anchor cert >= MAS(H); matched-pivot/acyclic-colouring certificate cert = v when the zero digraph is 3-dichromatic; mod-2 anchor cert >= #anchored lines with the exact isotropic/tied-minima criterion); (P2) independent stdlib reproduction of the one-copy L8 certificates on the named instances tied_min (recorded cert 11) and cex_min_1 (recorded cert 18); (P3) targeted falsifier search beyond the censused domain.
+Scope status: changed; reason for refinement or change: authorized "explicit open request" scope change to kappa-blocker KB5 (F-star proof-level work). The chooser OS draw (nonce 3096ed3facbe5aa91a71df29d9f6c6e7, track verifier-engineering) landed on replay-runtime and portable-replay, both saturated card readings with no kappa bearing; the orchestrator's KB5 assignment is the recorded reason. Pair-collision check before computation (discussions 1317 and 1166 via disc-comments incl. nested replies, 2026-10-15 16:40 UTC) found no live F-star proof claim; PR 2335's census is released.
+Existing restriction being changed (or exact claim being audited): the census's own limitation is audited: "witnesses are lower bounds on cert, not a proof" (PR 2335 README). No existing theorem is relaxed; F-star is attacked as stated (floor form) and every lemma carries its exact hypothesis.
+Method; explicit parameter ranges/candidate alphabet: stdlib exact integer/F2 arithmetic. Engine: for fixed a-labels the b-labels, order and kept set complete exactly by subset DP (O(v 2^v)); witnesses = local search over a-labels plus exact completion; exact cert by exhaustive a-enumeration at v <= 6; falsifier criterion = an explicit admissible pairing B with cost(B) = sum_j rank_F2 B[R_j,A_j] < floor(2v/3) (the proven chain cert <= cost(B)); brute-force-over-all-labellings cross-checks at v <= 3. Search domains beyond the census (v = 4..12, entries -2..2, three families): (i) factor entries in {-3..3}, v ascending from 4; (ii) v = 13..16 tied-heavy 2-adic constructions; (iii) named instances tied_min (v = 12) and cex_min_1 (v = 19) from PR 2111.
+Nearest overlapping PRs and why this adds something: PR 2335 (mine: witness-level census; this adds written proofs, exact-value upgrades and an out-of-domain search, not another census); PR 2111/PR 2162 (DreamingOfClouds: the named instances and certificate limits; their cert 11/18 values are CHECKED (recorded) CP-SAT results, here reproduced by a different stdlib-exact method on the one-copy side, with their theorems cited not restated); research/root-unit-decoder-lemmas (merged: F-star, cert definition, L8 lemma). Refined overlap pass on proper names at 16:44 UTC, complete pagination: no other proof-level F-star work.
+Optimistic full cost budget; required observable improvement: no kappa budget in play (missing-lemma work); the observable improvement over the predecessor is proof-level status: at least one PROVEN lemma with a checkable hypothesis plus exact cert values where the predecessor had witnesses only.
+Success evidence; falsification test; time/compute cap: success = written proofs (each demoted where incomplete) + PASS markers from verify.py showing engine/brute agreement, named-instance certificate reproduction and the declared search domain; falsification test = first exact falsifier (explicit B below threshold or exact cert below threshold at v <= 6), smallest falsifying instance first; stop at first falsifier or the declared domain, one bounded pivot maximum, early kill with the exact obstruction recorded. Compute cap: about 90 minutes single-process stdlib Python, each registered command below 600 s.
+Predecessor authors; intended artifact and reproduction command: predecessors = research/root-unit-decoder-lemmas (merged; PR 1590 (https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance), DreamingOfClouds PR 2111/PR 2162 (tied_min/cex_min_1), Aaron Wang PR 2335 (census). Artifact: research/fstar-proof-lemmas-seed3096ed3f/ with TASK.json, SOURCES.json, verify.py, CERTIFICATE.json, README.md; reproduction: python3 -B research/fstar-proof-lemmas-seed3096ed3f/verify.py then python3 scripts/research_package.py --package research/fstar-proof-lemmas-seed3096ed3f --check-only.