From 10644c90837cb377df89be7c87992320ebfaf091 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Thu, 15 Oct 2026 14:13:52 -0400 Subject: [PATCH 1/3] F-star proof lemmas: structural certificates, named-instance L8 reproduction, beyond-census search (no kappa) Package research/fstar-proof-lemmas-seed3096ed3f. PROVEN: Lemma SF (cert(M) >= MAS(H), = v for acyclic block-incidence digraph), Lemma MP (matched-pivot certificate, = v for 3-dichromatic zero digraphs), Lemma RK (mutual-zero K4-free, no transitive 4-tournament, no singleton-support incidence), Lemma AN (mod-2 anchor: cert(M) >= #odd diagonals; F-star holds for dyadic decoders with at most floor(v/3) even diagonals). CHECKED: PR 2111's tied_min and cex_min_1 one-copy L8 certificates (11/12, 18/19) reproduced by a stdlib-exact method, the chain engine recomputed at 22 on their stored pairing, exact cert at v = 5..6, and a 43-instance falsifier search beyond the census domain (entries -3..3 at v = 4..12; v = 13..16 entries3 and tied-heavy): 0 falsifiers, minimum witness ratio 0.867. F-star itself remains OPEN with its residue stated exactly. Aaron Wang, with help from opencode (substantial AI assistance; no model named per attribution rules). --- .../CERTIFICATE.json | 430 +++++++++++ .../fstar-proof-lemmas-seed3096ed3f/README.md | 297 ++++++++ .../SOURCES.json | 24 + .../TASK-CARD.md | 10 + .../fstar-proof-lemmas-seed3096ed3f/TASK.json | 82 ++ .../VERIFY.json | 16 + .../data/cex_min_1.B22.json | 1 + .../data/cex_min_1.json | 1 + .../data/cex_min_1.witness.json | 1 + .../data/tied_min.json | 1 + .../fstar-proof-lemmas-seed3096ed3f/verify.py | 721 ++++++++++++++++++ 11 files changed, 1584 insertions(+) create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/CERTIFICATE.json create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/README.md create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/SOURCES.json create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/TASK.json create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/VERIFY.json create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.B22.json create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.json create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.witness.json create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/data/tied_min.json create mode 100644 research/fstar-proof-lemmas-seed3096ed3f/verify.py diff --git a/research/fstar-proof-lemmas-seed3096ed3f/CERTIFICATE.json b/research/fstar-proof-lemmas-seed3096ed3f/CERTIFICATE.json new file mode 100644 index 0000000000..49b88eb8ae --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/CERTIFICATE.json @@ -0,0 +1,430 @@ +{ + "controls": { + "brute_agree": 3, + "corrupt_rejects": 2, + "diagonal_cert": 3 + }, + "digest": "134665ac6a0800e45be234e19f95e52409df7a560725cca67c93ee0aaa099aaf", + "engine": "a-label enumeration + exact (b, order, S) completion by subset DP", + "exact_cert_tiny": [ + { + "cert": 5, + "v": 5 + }, + { + "cert": 5, + "v": 5 + }, + { + "cert": 6, + "v": 6 + } + ], + "failures": [], + "falsifiers": [], + "min_witness_ratio": 0.8666666666666667, + "named": { + "cex_min_1.json": { + "chain_upper": 30, + "replay_ok": true, + "v": 19, + "witness": 18 + }, + "tied_min.json": { + "chain_upper": 20, + "replay_ok": true, + "v": 12, + "witness": 11 + } + }, + "schema_version": 1, + "search": [ + { + "chain_upper": 11, + "family": "entries3", + "free_pairs": 3, + "i": 0, + "threshold": 2, + "v": 4, + "witness": 4 + }, + { + "chain_upper": 7, + "family": "entries3", + "free_pairs": 1, + "i": 1, + "threshold": 2, + "v": 4, + "witness": 4 + }, + { + "chain_upper": 11, + "family": "entries3", + "free_pairs": 0, + "i": 2, + "threshold": 2, + "v": 4, + "witness": 4 + }, + { + "chain_upper": 7, + "family": "entries3", + "free_pairs": 4, + "i": 0, + "threshold": 3, + "v": 5, + "witness": 5 + }, + { + "chain_upper": 11, + "family": "entries3", + "free_pairs": 0, + "i": 1, + "threshold": 3, + "v": 5, + "witness": 5 + }, + { + "chain_upper": 12, + "family": "entries3", + "free_pairs": 2, + "i": 2, + "threshold": 3, + "v": 5, + "witness": 5 + }, + { + "chain_upper": 15, + "family": "entries3", + "free_pairs": 2, + "i": 0, + "threshold": 4, + "v": 6, + "witness": 6 + }, + { + "chain_upper": 15, + "family": "entries3", + "free_pairs": 0, + "i": 1, + "threshold": 4, + "v": 6, + "witness": 6 + }, + { + "chain_upper": 14, + "family": "entries3", + "free_pairs": 0, + "i": 2, + "threshold": 4, + "v": 6, + "witness": 6 + }, + { + "chain_upper": 14, + "family": "entries3", + "free_pairs": 6, + "i": 0, + "threshold": 4, + "v": 7, + "witness": 7 + }, + { + "chain_upper": 13, + "family": "entries3", + "free_pairs": 6, + "i": 1, + "threshold": 4, + "v": 7, + "witness": 7 + }, + { + "chain_upper": 17, + "family": "entries3", + "free_pairs": 2, + "i": 2, + "threshold": 4, + "v": 7, + "witness": 7 + }, + { + "chain_upper": 17, + "family": "entries3", + "free_pairs": 5, + "i": 0, + "threshold": 5, + "v": 8, + "witness": 8 + }, + { + "chain_upper": 17, + "family": "entries3", + "free_pairs": 6, + "i": 1, + "threshold": 5, + "v": 8, + "witness": 8 + }, + { + "chain_upper": 19, + "family": "entries3", + "free_pairs": 3, + "i": 2, + "threshold": 5, + "v": 8, + "witness": 8 + }, + { + "chain_upper": 16, + "family": "entries3", + "free_pairs": 7, + "i": 0, + "threshold": 6, + "v": 9, + "witness": 9 + }, + { + "chain_upper": 21, + "family": "entries3", + "free_pairs": 5, + "i": 1, + "threshold": 6, + "v": 9, + "witness": 9 + }, + { + "chain_upper": 20, + "family": "entries3", + "free_pairs": 3, + "i": 2, + "threshold": 6, + "v": 9, + "witness": 9 + }, + { + "chain_upper": 23, + "family": "entries3", + "free_pairs": 8, + "i": 0, + "threshold": 6, + "v": 10, + "witness": 10 + }, + { + "chain_upper": 20, + "family": "entries3", + "free_pairs": 5, + "i": 1, + "threshold": 6, + "v": 10, + "witness": 10 + }, + { + "chain_upper": 23, + "family": "entries3", + "free_pairs": 9, + "i": 2, + "threshold": 6, + "v": 10, + "witness": 10 + }, + { + "chain_upper": 25, + "family": "entries3", + "free_pairs": 6, + "i": 0, + "threshold": 7, + "v": 11, + "witness": 11 + }, + { + "chain_upper": 25, + "family": "entries3", + "free_pairs": 8, + "i": 1, + "threshold": 7, + "v": 11, + "witness": 11 + }, + { + "chain_upper": 21, + "family": "entries3", + "free_pairs": 5, + "i": 2, + "threshold": 7, + "v": 11, + "witness": 11 + }, + { + "chain_upper": 25, + "family": "entries3", + "free_pairs": 16, + "i": 0, + "threshold": 8, + "v": 12, + "witness": 12 + }, + { + "chain_upper": 27, + "family": "entries3", + "free_pairs": 10, + "i": 1, + "threshold": 8, + "v": 12, + "witness": 12 + }, + { + "chain_upper": 27, + "family": "entries3", + "free_pairs": 8, + "i": 2, + "threshold": 8, + "v": 12, + "witness": 12 + }, + { + "chain_upper": 28, + "family": "entries3-big", + "free_pairs": 9, + "i": 0, + "threshold": 8, + "v": 13, + "witness": 13 + }, + { + "chain_upper": 25, + "family": "entries3-big", + "free_pairs": 22, + "i": 1, + "threshold": 8, + "v": 13, + "witness": 13 + }, + { + "chain_upper": 34, + "family": "entries3-big", + "free_pairs": 14, + "i": 0, + "threshold": 9, + "v": 14, + "witness": 13 + }, + { + "chain_upper": 30, + "family": "entries3-big", + "free_pairs": 12, + "i": 1, + "threshold": 9, + "v": 14, + "witness": 14 + }, + { + "chain_upper": 33, + "family": "entries3-big", + "free_pairs": 10, + "i": 0, + "threshold": 10, + "v": 15, + "witness": 13 + }, + { + "chain_upper": 35, + "family": "entries3-big", + "free_pairs": 8, + "i": 1, + "threshold": 10, + "v": 15, + "witness": 15 + }, + { + "chain_upper": 36, + "family": "entries3-big", + "free_pairs": 17, + "i": 0, + "threshold": 10, + "v": 16, + "witness": 16 + }, + { + "chain_upper": 34, + "family": "entries3-big", + "free_pairs": 13, + "i": 1, + "threshold": 10, + "v": 16, + "witness": 15 + }, + { + "chain_upper": 36, + "family": "tied-heavy", + "free_pairs": 13, + "i": 0, + "threshold": 8, + "v": 13, + "witness": 13 + }, + { + "chain_upper": 36, + "family": "tied-heavy", + "free_pairs": 8, + "i": 1, + "threshold": 8, + "v": 13, + "witness": 13 + }, + { + "chain_upper": 42, + "family": "tied-heavy", + "free_pairs": 14, + "i": 0, + "threshold": 9, + "v": 14, + "witness": 14 + }, + { + "chain_upper": 39, + "family": "tied-heavy", + "free_pairs": 14, + "i": 1, + "threshold": 9, + "v": 14, + "witness": 14 + }, + { + "chain_upper": 45, + "family": "tied-heavy", + "free_pairs": 15, + "i": 0, + "threshold": 10, + "v": 15, + "witness": 15 + }, + { + "chain_upper": 45, + "family": "tied-heavy", + "free_pairs": 11, + "i": 1, + "threshold": 10, + "v": 15, + "witness": 15 + }, + { + "chain_upper": 48, + "family": "tied-heavy", + "free_pairs": 12, + "i": 0, + "threshold": 10, + "v": 16, + "witness": 16 + }, + { + "chain_upper": 39, + "family": "tied-heavy", + "free_pairs": 19, + "i": 1, + "threshold": 10, + "v": 16, + "witness": 16 + } + ] +} \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/README.md b/research/fstar-proof-lemmas-seed3096ed3f/README.md new file mode 100644 index 0000000000..4f82d6b0c3 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/README.md @@ -0,0 +1,297 @@ +# fstar-proof-lemmas-seed3096ed3f + +**Proof-level work on open problem F-star (no kappa, no frontier change).** This +package moves the F-star question of `research/root-unit-decoder-lemmas` +(section 7, OPEN) from the witness-level census of +https://github.com/CrocSwap/integer-mult-bounds/pull/2335 toward proof level: +four structural lemmas with exact hypotheses and written proofs (PROVEN below), +an independent stdlib reproduction of the one-copy L8 certificates of +DreamingOfClouds' named instances `tied_min` (12 lines) and `cex_min_1` (19 +lines) of https://github.com/CrocSwap/integer-mult-bounds/pull/2111, exact +`cert` values where exhaustive computation is possible, and a targeted falsifier +search beyond the censused domain. **F-star itself is not proved and not +refuted here.** Every claim below is labelled PROVEN or CHECKED; the residue is +spelled out in "What is demoted". + +## The object + +A `T = 3` exact decoder on `v` lines is `M = sum_{j=1..3} p_j q_j^T` over the +rationals with `M_tt != 0` on every line (`p_j, q_j` are the coordinate columns +over lines; `M_ts = p(t) . q(s)`). Row support `pi(t) = {j : p_j(t) != 0}`, +column support `sigma(t) = {j : q_j(t) != 0}`; both are nonempty and +`D(t) = pi(t) intersect sigma(t)` is nonempty because `M_tt != 0`. An *L8 +labelling* is F2 vectors `a(t)` supported in `pi(t)` and `b(t)` supported in +`sigma(t)`, with `K_ts = a(t) . b(s) mod 2`; `cert(M)` is the largest `|S|` +admitting an order with `K_tt = 1` on `S` and `K_ts = 0` at every incidence +`M_ts = 0` with `t` before `s` (`t, s in S`). Definitions and the proven chain +`cost >= sum_j r_j >= cert(M)` are from `research/root-unit-decoder-lemmas` +(merged); this package does not restate their proofs. + +**Remark (CHECKED on every instance, and immediate from the definition).** +`cert(M)` depends only on the zero pattern `Z` of `M` off the diagonal and the +supports `pi, sigma`, not on the coefficient values and not on any pairing `B`. +Write `H = {(t,s) : t != s, M_ts = 0, pi(t) intersect sigma(s) nonempty}` for +the *block-incidence digraph* of PR 2111's Lemma SCC, and `Z` for the full zero +digraph; `H` is the part of `Z` that lands inside some block `R_j x A_j`. For a +labelling `K` let `D_K = {(t,s) : M_ts = 0, K_ts = 1}` be its conflict digraph; +a set `S` is feasible with an order iff `K_tt = 1` on `S` and `D_K[S]` is +acyclic (then any order making every `D_K` edge point backward works). + +## 1. Lemma SF (support-forced incidences vanish) — PROVEN + +> **Lemma SF.** For every L8 labelling, `K_ts = 0` whenever +> `pi(t) intersect sigma(s)` is empty; hence `D_K` is a subdigraph of `H` for +> every labelling. Consequently: (i) `cert(M) >= MAS(H)`, the maximum size of an +> induced acyclic subset of `H`; (ii) `cert(M) = v` whenever `H` is acyclic; +> (iii) `cert(M) >= v - fvs(H)`, where `fvs` is a minimum feedback vertex set. + +*Proof.* `K_ts = sum_j a_j(t) b_j(s)`, and `a_j(t) = 0` for `j` outside +`pi(t)`, `b_j(s) = 0` for `j` outside `sigma(s)`, so every nonzero summand +needs `j in pi(t) intersect sigma(s)`, an empty set by hypothesis. Thus `D_K` +is a subdigraph of +`H`. Take the matched-pivot labelling `a(t) = b(t) = e_{c(t)}` with any +`c(t) in D(t)` (nonempty, since `M_tt = sum_j p_j(t) q_j(t) != 0`); then +`K_tt = 1` on every line. For any `S` with `H[S]` acyclic, `D_K[S]` is acyclic; +order `S` with every `H[S]` edge pointing backward (repeatedly take sinks +first). Every `D_K` edge is an `H` edge and points backward, so no constraint +pair is forward with `K_ts = 1`; `S` is feasible. Maximizing over `S` gives +(i); (ii) is (i) with `S = [v]`; (iii) follows from `MAS(H) >= v - fvs(H)`. +`QED` + +This is a named-family result: **F-star holds (with `cert = v`) for every +decoder whose block-incidence digraph `H` is acyclic**, and quantitatively for +every instance through `MAS(H)` and `fvs(H)`. CHECKED: on `tied_min` the exact +`MAS(H) = 4`, so the lemma alone is far from tight there (`cert = 11`); the +lemma is a floor, not a characterization. + +## 2. Lemma MP (matched-pivot certificate) — PROVEN + +> **Lemma MP.** For every map `c: [v] -> {1,2,3}` with `c(t) in D(t)`, let +> `C_i = c^{-1}(i)`. Then `cert(M) >= sum_i MAS(Z[C_i])`. Hence `cert(M) = v` +> whenever `Z` admits a partition into three acyclic classes with each line's +> pivot inside its `D(t)` (in particular when `Z` is 3-dichromatic and all +> `D(t)` are nonempty). + +*Proof.* With matched pivots `a(t) = b(t) = e_{c(t)}` one gets `K_ts = 1` iff +`c(t) = c(s)`, so `D_K` is the disjoint union of the `Z[C_i]` over the three +classes. Acyclic subsets of disjoint vertex sets union to an acyclic subset, of +size `sum_i MAS(Z[C_i])`; apply Lemma SF's order argument. If each class is +acyclic the sum is `v`. `QED` + +CHECKED on every instance in `CERTIFICATE.json` (the constructed pivot witness +is replayed by the checker on all instances with `v <= 12`). + +## 3. Lemma RK (rank-3 structural facts) — PROVEN + +> **Lemma RK.** For any `M` of rank at most 3 with nonzero diagonal (in +> particular every exact `T = 3` decoder): (a) the mutual-zero graph `G_0` +> (edges `{t,s}` with `M_ts = M_st = 0`) has no `K_4`; (b) `Z` contains no +> transitive 4-tournament; (c) an incidence with `|pi(t) intersect sigma(s)| = 1` +> is impossible, so every zero pair landing in a block has +> `|pi(t) intersect sigma(s)| >= 2`. + +*Proof.* (a) A mutual-zero clique `S` makes `M[S,S]` diagonal with nonzero +diagonal, so `rank M >= |S|` and `|S| <= 3`. (b) If `M_{t_i t_j} = 0` for all +`i < j` in some ordering of four lines, `M[S,S]` is triangular with nonzero +diagonal and rank at least 4. (c) `M_ts = sum_j p_j(t) q_j(s)`; one nonzero +summand cannot vanish. `QED` + +(c) is PR 2111's L5, restated for completeness. (a) and (b) restrict what a +falsifier's zero pattern can look like; CHECKED on every searched instance +(`v <= 16`). + +## 4. Lemma AN (mod-2 anchor) — PROVEN + +> **Lemma AN.** Suppose that after per-total powers of two the factorization is +> 2-integral: all entries of `p, q` lie in `Z_(2)`. Then `a(t) = p(t) mod 2`, +> `b(t) = q(t) mod 2` is an L8 labelling with `K_ts = M_ts mod 2`; in +> particular `K_ts = 0` at every incidence and `K_tt = M_tt mod 2`. Hence +> `S = {t : M_tt odd}` is feasible in any order and +> `cert(M) >= #{t : M_tt odd}`. Under the added hypothesis that at most +> `floor(v/3)` lines have `M_tt` even, `cert(M) >= ceil(2v/3)`, so **F-star +> holds for dyadic decoders with at most one-third even diagonals**. + +*Proof.* Reducing `sum_j p_j(t) q_j(s) = M_ts` modulo 2 gives +`sum_j a_j(t) b_j(s) = M_ts mod 2` (all entries are 2-integers); supports +shrink under reduction so the support constraints hold. At an incidence +`M_ts = 0`, so `K_ts = 0`; on `S` all diagonals are 1, so every order works and +`|S| = v - #{t : M_tt even} >= v - floor(v/3) = ceil(2v/3)`. `QED` + +The count `#{t : M_tt odd}` depends only on the diagonal of `M`, and the +identity holds for every 2-integral normalization of the factorization, so the +bound is normalization-robust. What Lemma AN does **not** do is classify which +lines can be made odd by changing the normalization: that is exactly the +*tied-minima* obstruction of `research/root-unit-decoder-lemmas` section 7 +(lines whose minimal 2-adic valuations among the products `p_k(t) q_k(t)` tie, +where the reduction is isotropic and one-sided repairs are unavailable). This +package does not resolve that question; see "What is demoted". + +## 5. Engine and controls — CHECKED + +`verify.py` (stdlib only, deterministic). For fixed `a`-labels the completion +over `b`-labels, order and kept set is **exact** by subset DP: `b`-existence +for line `t` against blocker span `U` is a per-line table lookup +(`exists b in F2^{sigma(t)}: a(t).b = 1 and a(s).b = 0 for s in U`), and +`f[T] = OR over t in T of (f[T \ t] and b-exists(t, blockers of T \ t))` over +all subsets. Exact `cert` enumerates all `a`-labelings (`v <= 5`); the witness +search hill-climbs over `a`-labels with exact completion; every stored witness +is replayed by an independent checker (supports, `K_tt = 1`, and the order +constraints recomputed from scratch). + +Controls (all in `verify.py`, all required to pass): + +1. Three tiny instances (`v = 3`) are computed both by brute force over *all* + labellings (the definition) and by the engine; the values must agree (3/3). +2. The hand-checkable diagonal decoder `p_j = q_j = e_j` gives `cert = 3`. +3. Corrupted witnesses (a zeroed `a(t)`, a zeroed `b(t)`) are rejected by the + independent checker. +4. The chain engine is recomputed on PR 2111's stored pairing for `cex_min_1` + and must reproduce their recorded cost 22 (`10 + 6 + 6`); this validates + `sum_j rank_F2 B[R_j, A_j]` on real data. +5. The matched-pivot witness constructed from `MAS(H)` is replayed wherever + `MAS(H)` is computed exactly (`v <= 12`). +6. The proven chain `witness <= cost(B)` is rechecked on every instance with + both numbers available. + +## 6. Named instances (PR 2111) — CHECKED + +The one-copy L8 certificates of the named instances are reproduced here by a +different method (exact-completion engine + stored-witness replay), from +byte-identical copies of PR 2111's data files (`data/`, sha256 recorded in +TASK.json evidence): + +| instance | v | PR 2111 recorded max one-copy L8 | this package | threshold `floor(2v/3)` | +|---|---:|---:|---|---:| +| `tied_min` | 12 | 11 (CHECKED, recorded: CP-SAT) | witness 11, machine-checked and re-found by the deterministic search | 8 | +| `cex_min_1` | 19 | 18 (CHECKED, recorded: CP-SAT) | stored witness 18, machine-checked replay | 12 | + +On `tied_min` the deterministic hill-climb re-finds 11 within its bounded +budget, so the two independent methods agree at 11; combined with PR 2111's +recorded CP-SAT upper bound, `cert(tied_min) = 11` is pinned at both ends +(subject to their recorded, not here re-verified, optimality claim). The same +holds at 18 for `cex_min_1`. Both values are consistent with F-star +(`11 >= 8`, `18 >= 12`) and show `cert < v` is genuinely possible +(`cex_min_1`), which by Lemma MP forces its zero digraph to be non-3-dichromatic. + +The chain engine is validated on real data: PR 2111's stored pairing for +`cex_min_1` (`data/cex_min_1.B22.json`) is recomputed here as exactly 22 +(`10 + 6 + 6`, matching their record) and is confirmed admissible. The bounded +`B`-search itself finds 20 on `tied_min` and 30 on `cex_min_1`, weaker than the +recorded optima (12 and 22); those numbers are labelled upper bounds. + +Exact `cert` values where exhaustive `a`-enumeration terminates: two `v = 5` +instances and one `v = 6` instance from the new-alphabet family have +`cert = v` exactly (engine upper and lower bounds coincide; these upgrade the +census's witness-level claims to exact values on their instances). + +## 7. Beyond-census falsifier search — CHECKED (scoped negative) + +The census of PR 2335 covers `v = 4..12`, factor entries in `{-2..2}`, three +families, 196 sampled instances. This search goes beyond that domain, +smallest falsifying instance first (`v` ascending). Falsifier criterion: an +explicit admissible pairing `B` (0/1, unit diagonal, ones only where `M` +vanishes) with `cost(B) = sum_j rank_F2 B[R_j, A_j] < floor(2v/3)`, which by +the proven chain would force `cert(M) < floor(2v/3)`. The `B`-search is a +bounded deterministic search (exhaustive only when the admissible-pair count +is at most 12), so the recorded chain numbers are upper bounds and can only +overstate `cert`; a missing low-cost `B` cannot create a false falsifier, but +the search is not an exhaustive non-falsification proof. + +| family | domain | instances | falsifiers | min witness ratio | +|---|---|---:|---:|---:| +| entries3 | `v = 4..12`, entries `{-3..3}` | 27 | 0 | 1.000 | +| entries3-big | `v = 13..16`, entries `{-3..3}` | 8 | 0 | 0.867 | +| tied-heavy | `v = 13..16`, 2-adic weighted | 8 | 0 | 1.000 | + +The worst witness ratio is 13/15 on an `entries3-big` instance at `v = 15` +(threshold 10), limited by the bounded search budget, not by an observed +certificate drop. The tied-heavy generator deliberately accumulates the named +obstruction: every product `p_j(t) q_j(t)` is even on half the lines (all tied +at level 1), so the mod-2 anchor is isotropic there and the labelling search +carries the full load; all eight tied-heavy instances are witnessed at +`cert = v`. Every instance is witnessed at or above `floor(2v/3)` and every +witness is replayed by the independent checker. Full per-instance records are +in `CERTIFICATE.json` (digest printed by `verify.py`). + +## What is proved, what is witnessed, what is demoted + +- **PROVEN:** Lemma SF, Lemma MP, Lemma RK, Lemma AN (each with its exact + hypothesis above). Together with the source package's proven consequence + (F-star closes every open `T = 3` window), Lemma AN closes the stated + subfamily: dyadic decoders with at most `floor(v/3)` even diagonals; Lemma SF + closes every decoder with acyclic `H`; Lemma MP closes every decoder whose + zero digraph is 3-dichromatic. +- **CHECKED:** the engine controls, the named-instance certificate + reproduction (`tied_min` 11/12, `cex_min_1` 18/19), the chain-engine + cross-check at 22, exact `cert` at `v = 5..6`, the structural checks per + instance, and the declared-domain search (no falsifier). +- **Demoted / OPEN:** F-star for general rational decoders is **not** proved + here. The residue is exactly: (a) lines that no 2-integral normalization + anchors odd (the tied-minima/isotropic lines) — Lemma AN handles only the + even-diagonal count, not their repair or ordering; (b) zero digraphs that are + not 3-dichromatic (Lemma MP then gives only `sum_i MAS(Z[C_i])`); (c) for + non-dyadic entries (odd primes in denominators) the mod-2 anchor does not + apply at all. No "exactly when" or necessity claim is made for any lemma's + hypothesis: each is sufficient as stated and not shown necessary. The + `B`-search values are bounded-search upper bounds, not exact minima. + +## Open next questions + +1. **Order the tied residue.** Can the unanchorable (tied-minimum) lines always + be ordered, with one-sided repairs, keeping at least `floor(2v/3)` lines? + Why it matters: Lemma AN reduces F-star to exactly this. First step: + enumerate tied-heavy decoders at `v <= 8`, classify unanchorable lines by + valuation-tie type, and test the anchorable count plus greedy ordering. + Blocker: none structural; needs a dedicated enumeration session. +2. **Dichromatic number of rank-3 zero digraphs.** Is every such `Z` + 3-dichromatic (with pivots inside `D(t)`)? `cex_min_1` (cert 18 < 19) forces + the answer no at the level of *certificates*; the open question is whether + `Z` itself can be non-3-dichromatic. First step: compute dichromatic numbers + of the zero digraphs of the stored instances. Blocker: needs an exact + dichromatic-number routine beyond `v <= 12`. +3. **Exact chain minima on the named instances.** PR 2111 records + `cost(tied_min) = 12` and a stored cost-22 `B` for `cex_min_1`; an exact + minimizer here would pin `cert` between 11 and 12 (and 18 and 22). First + step: branch-and-bound over admissible pairings seeded from the stored + pairing. Blocker: longer exact run than one session allows. + +## Reproduce + +Python 3.10+, standard library only, from the repository root: + +```sh +python3 -B research/fstar-proof-lemmas-seed3096ed3f/verify.py +python3 scripts/research_package.py --package research/fstar-proof-lemmas-seed3096ed3f --check-only +python3.12 scripts/research_package.py --package research/fstar-proof-lemmas-seed3096ed3f +``` + +Expected markers include `PASS_FSTAR_CONTROLS`, `PASS_FSTAR_NAMED`, +`PASS_FSTAR_CHAIN_ENGINE`, `PASS_FSTAR_EXACT`, `PASS_FSTAR_STRUCTURAL`, +`PASS_FSTAR_SEARCH` and `PASS_FSTAR_PROOF_LEMMAS`. The registered CPython 3.12 +replay prints `PASS_REGISTERED_RESEARCH_PACKAGE +research/fstar-proof-lemmas-seed3096ed3f outcome=completed`. `make` is not +installed on the authoring host; the commands above are the underlying ones. + +## Credit and provenance + +F-star, the `cert(M)` definition, L8 labellings and the proven chain +`cost >= sum_j r_j >= cert(M)` are from the merged package +`research/root-unit-decoder-lemmas` (Douglas Colkitt with OpenAI Codex +assistance lineage). The rank-3 configuration model, the named instances +`tied_min` and `cex_min_1`, their recorded one-copy certificate limits (11 and +18, CP-SAT, CHECKED (recorded)), the stored cost-22 pairing for `cex_min_1` +(`data/cex_min_1.B22.json`), Lemma SCC's block-incidence digraph and L5 are +DreamingOfClouds' work in +https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and +https://github.com/CrocSwap/integer-mult-bounds/pull/2162; `data/tied_min.json` +and `data/cex_min_1.json` are byte-identical copies of their data files (sha256 +`670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93` and +`86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7`). The +falsifier census this package builds on is Aaron Wang's +https://github.com/CrocSwap/integer-mult-bounds/pull/2335. This package does +not claim their results; the new content is Lemmas SF/MP/RK/AN with their +proofs, the exact-completion engine and its controls, the independent +certificate reproduction, and the beyond-census search. + +Prepared by **Aaron Wang** with help from opencode (substantial AI assistance; +no independent human review claimed). New work in this package is Apache-2.0. diff --git a/research/fstar-proof-lemmas-seed3096ed3f/SOURCES.json b/research/fstar-proof-lemmas-seed3096ed3f/SOURCES.json new file mode 100644 index 0000000000..afe8ee671f --- /dev/null +++ b/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" + } + ] +} diff --git a/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md b/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md new file mode 100644 index 0000000000..54fbddb4e2 --- /dev/null +++ b/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; Douglas Colkitt with OpenAI Codex assistance lineage), 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. diff --git a/research/fstar-proof-lemmas-seed3096ed3f/TASK.json b/research/fstar-proof-lemmas-seed3096ed3f/TASK.json new file mode 100644 index 0000000000..af5b58ea45 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "changed", + "actual_scope": "Kappa-blocker KB5, proof-level work on open problem F-star of research/root-unit-decoder-lemmas section 7: cert(M) >= floor(2v/3) for every exact 3-total rational decoder. Three parts: (P1) PROVEN structural lemmas with exact hypotheses (support-forced anchor cert >= MAS(H) and cert = v when the block-incidence digraph is acyclic; matched-pivot certificate cert >= sum_i MAS(Z[C_i]) and cert = v when the zero digraph is 3-dichromatic; mod-2 anchor cert >= #{t : M_tt odd} in a 2-integral normalization), each demoted where unproved; (P2) independent stdlib reproduction of the one-copy L8 certificates on DreamingOfClouds' named instances tied_min (12 lines) and cex_min_1 (19 lines) of PR 2111, with exact cert values at tiny v and an exact chain-engine cross-check against PR 2111's stored cost-22 pairing; (P3) a targeted falsifier search beyond the censused domain of PR 2335 (v = 4..12, entries -2..2): factor entries in {-3..3} at v = 4..12 and v = 13..16 with tied-heavy 2-adic constructions, smallest v first, falsifier criterion an explicit admissible pairing B with sum_j rank_F2 B[R_j,A_j] < floor(2v/3) via the proven chain cert(M) <= cost(B).", + "scope_change_reason": "Authorized 'explicit open request' scope change to kappa-blocker KB5 (F-star proof-level work), recorded per the assignment. The chooser OS draw (nonce 3096ed3facbe5aa91a71df29d9f6c6e7, track verifier-engineering) landed on the saturated cards replay-runtime and portable-replay; both are incremental verifier-engineering readings with no kappa bearing, and the assignment names the draw landing on saturated cards as the recorded reason for taking the KB5 request instead. Pair-collision check before computation (toolkit disc-comments on discussions 1317 and 1166 including nested replies, 2026-10-15 16:40 UTC) found no live F-star proof-level claim; the predecessor census https://github.com/CrocSwap/integer-mult-bounds/pull/2335 is released. The handoffs thread's T = 3 open-core requests invite independent eyes on this exact object.", + "existing_restriction_being_changed": "Nothing is relaxed. F-star is attacked as stated (floor form); the predecessor PR 2335 census's own limitation ('witnesses are lower bounds on cert, not a proof') is the restriction being addressed. Every lemma in the package carries its exact hypothesis, and every claim that is not proved is demoted to OPEN; no 'exactly when' or necessity wording is used without proof.", + "method": "Exact stdlib integer/F2 arithmetic. Engine: for fixed a-labels the (b-labels, order, kept set) completion is exact by subset DP (b-exists is a per-line table lookup; f[T] = OR over t in T of f[T minus t] and b-exists(t, blockers of T minus t)); exact cert enumerates all a-labels at v <= 5; witness search hill-climbs over a-labels with exact completion; an independent witness checker replays every stored witness; falsifier criterion is an explicit admissible pairing B (0/1, unit diagonal, ones only where M vanishes) with chain cost sum_j rank_F2 B[R_j,A_j] < floor(2v/3), by the proven chain cost >= sum_j r_j >= cert(M). Controls: brute-force-over-all-labellings cross-check at v = 3, a hand-checkable diagonal decoder, corrupted-witness rejection, a matched-pivot witness constructed from MAS(H), and the chain engine recomputed on PR 2111's stored cost-22 pairing for cex_min_1.", + "parameter_ranges": "T = 3 totals exactly; rational decoders M = sum_j p_j q_j^T with M_tt != 0. Named instances: PR 2111's tied_min (v = 12, entries in {-1,0,1}) and cex_min_1 (v = 19, entries in {-1,0,1}). Search beyond the censused domain of PR 2335: (i) factor entries in {-3..3} (outside the census alphabet {-2..2}) at v = 4..12, three instances per v; (ii) v = 13..16 (outside the census v-range) with entries in {-3..3} and tied-heavy 2-adic constructions (entries in {+-2,+-4} and {+-1,+-2}), two instances per v and family. Exact cert (exhaustive a-enumeration) at v = 5.", + "nearest_overlapping_prs": "https://github.com/CrocSwap/integer-mult-bounds/pull/2335 (my own predecessor session: the 196-instance falsifier census with witnesses; this session adds written structural proofs, exact-value computation, an independent named-instance certificate reproduction and an out-of-domain search, not another census). https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and https://github.com/CrocSwap/integer-mult-bounds/pull/2162 (DreamingOfClouds: the named instances tied_min/cex_min_1, their certificate limits and the T = 3 reductions; their one-copy L8 maxima 11 and 18 are CHECKED (recorded) CP-SAT results, here reproduced by a different stdlib-exact method, their theorems cited not restated). research/root-unit-decoder-lemmas (merged: F-star, the cert(M) definition, the L8 lemma and the tied-minima obstruction). Refined overlap pass on the object's proper names (F-star, cert(M), 3-total decoder, labelling, root-unit decoder, floor(2v/3), tied-min) at 2026-10-15 16:44 UTC with complete pagination (827 open PRs, 1292 discussion records) found no other proof-level F-star work.", + "optimistic_full_cost_budget": "No kappa, supplier, word or moment budget is in play (missing-lemma work). The whole-construction price is the evidence itself: every lemma proof is in the README and every computational claim is recomputed by verify.py in one bounded stdlib run (no third-party packages, no solver).", + "bottleneck_link": "F-star is the named route to closing every open T = 3 window at once (research/root-unit-decoder-lemmas section 7, consequence PROVEN given F-star): cost >= floor(2v/3) >= N(h) for every open T = 3 window. Proof-level structural lemmas narrow the remaining gap to exactly stated residue (isotropic/tied-minimum lines and non-3-dichromatic zero digraphs); a falsifier would redirect the T = 3 decoder route entirely.", + "stop_rule": "Stop at the first exact falsifier (smallest falsifying instance first: an explicit admissible B with cost below floor(2v/3), or exact cert below threshold at v <= 5), or, absent one, at the declared search domain with every instance witnessed at or above threshold and the exact obstruction recorded. One bounded pivot maximum; early kill with the exact obstruction recorded. Compute cap: about 90 minutes of single-process stdlib Python; each registered command below 600 seconds.", + "success_evidence": "Written proofs of the structural lemmas (each demoted where incomplete) plus PASS markers from verify.py: engine/brute agreement at v = 3, the diagonal control, corrupted-witness rejection, the named-instance certificate reproduction (tied_min 11/12 and cex_min_1 18/19 machine-checked witnesses, matching PR 2111's recorded one-copy L8 maxima), exact cert values at v = 5, the chain engine recomputed on PR 2111's stored cost-22 pairing, structural lemma checks on every searched instance, and the declared-domain search summary with falsifier count.", + "falsification_test": "Side A of the search is itself the falsifier test for F-star: an explicit admissible pairing B with cost(B) < floor(2v/3) refutes F-star (the chain cost >= cert(M) is proven). Side B witnesses are rejected by the independent checker if any K_tt = 1 fails or any before-pair constraint fails; corrupted copies of stored witnesses must fail verification (checked).", + "time_compute_cap": "One session; compute capped at about 90 minutes single-process stdlib Python; no SAT solver, no third-party packages, no large downloads; each registered verify command capped at 600 seconds per the research_package.py limit.", + "predecessor_authors": "F-star, the cert(M) definition, L8 labellings and the proven chain cost >= sum_j r_j >= cert(M): the merged research/root-unit-decoder-lemmas package (Douglas Colkitt with OpenAI Codex assistance lineage). The rank-3 configuration model, the named instances tied_min and cex_min_1 and their recorded certificate limits: DreamingOfClouds, https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and https://github.com/CrocSwap/integer-mult-bounds/pull/2162. The falsifier census this session builds on: Aaron Wang, https://github.com/CrocSwap/integer-mult-bounds/pull/2335. This package does not claim their results; it adds structural lemmas, independent certificate reproduction and an out-of-domain search.", + "intended_artifact": "research/fstar-proof-lemmas-seed3096ed3f/ with TASK.json, SOURCES.json pins, VERIFY.json, verify.py, data/ (the named instances and one stored witness, byte-identical to PR 2111's data files), CERTIFICATE.json (written by verify.py) and 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.", + "outcome": "completed", + "evidence": "PROOF-LEVEL PROGRESS plus SCOPED NEGATIVE SEARCH. PROVEN (written proofs in README.md): Lemma SF (support-forced incidences vanish: K_ts = 0 whenever pi(t) intersect sigma(s) is empty, hence cert(M) >= MAS(H), cert(M) = v for acyclic block-incidence digraph H, cert(M) >= v - fvs(H)); Lemma MP (matched-pivot certificate cert(M) >= sum_i MAS(Z[C_i]) for every pivot map into D(t), cert(M) = v when the zero digraph is 3-dichromatic with pivots in D(t)); Lemma RK (mutual-zero graph K4-free, zero digraph free of transitive 4-tournaments, no incidence with |pi(t) intersect sigma(s)| = 1); Lemma AN (mod-2 anchor: for 2-integral factorizations cert(M) >= #{t : M_tt odd}, so F-star holds for dyadic decoders with at most floor(v/3) even diagonals). CHECKED by verify.py (stdlib, deterministic, 17.7 s, certificate digest 134665ac6a0800e4): controls pass (brute-force-over-all-labellings agreement 3/3 at v = 3, diagonal control cert = 3, corrupted-witness rejection 2/2); named-instance one-copy L8 certificates of PR 2111 reproduced by a different stdlib-exact method — tied_min 11/12 (re-found by the deterministic search) and cex_min_1 18/19 (stored witness replayed), both exactly matching PR 2111's recorded CP-SAT maxima and both above floor(2v/3) = 8 and 12; PR 2111's stored cost-22 pairing for cex_min_1 recomputed exactly (chain cost 22 = 10+6+6, admissible) validating the chain engine; exact cert values by exhaustive a-enumeration: two v = 5 and one v = 6 instance, each cert = v exactly; structural lemma checks on 45 instances (mutual-zero K4-free and no transitive 4-tournament on 44 with v <= 16, matched-pivot witness replayed on 28 with v <= 12); beyond-census falsifier search: 43 instances (entries {-3..3} at v = 4..12, 27 instances; v = 13..16 entries3 8 instances; v = 13..16 tied-heavy 2-adic 8 instances), falsifiers = 0, minimum witness ratio 0.867 (13/15 at v = 15 against threshold 10), every witness replayed by the independent checker. NOT PROVED: F-star itself; the residue is stated exactly (tied-minimum/isotropic lines not covered by the anchor, zero digraphs that are not 3-dichromatic, non-dyadic entries); the B-search values are bounded-search upper bounds, not exact minima.", + "author": "Aaron Wang (with help from opencode)", + "ai_assistance": "Substantial AI assistance: this package was produced by Aaron Wang with help from opencode (opencode agent harness). No independent human review claimed. No model is cited per orchestrator attribution rules.", + "open_questions": [ + { + "question": "Can the tied-minimum residue be ordered? Precisely: for lines whose diagonal cannot be anchored odd by any 2-integral normalization (the tied-minima obstruction of research/root-unit-decoder-lemmas section 7), does there always exist an ordering and one-sided repairs keeping at least floor(2v/3) lines?", + "why_it_matters": "This is exactly the residue left by the mod-2 anchor lemma: the anchor kills every incidence and leaves only unanchorable (isotropic) lines; a structure theorem for them would prove F-star.", + "first_step": "Enumerate small tied-heavy decoders (entries in {+-2,+-4}, v <= 8) and classify the unanchorable lines by their valuation-tie type; test whether the anchorable count plus a greedy ordering of the tied classes always reaches floor(2v/3).", + "blocked_by": "No structural blocker; needs a dedicated enumeration session." + }, + { + "question": "Is every rank-3 decoder's zero digraph 3-dichromatic (partitionable into three acyclic classes, with pivots c(t) inside D(t) = pi(t) intersect sigma(t))?", + "why_it_matters": "The matched-pivot lemma would give cert(M) = v in that case; a counterexample would pin the exact combinatorial obstruction beyond the tied lines.", + "first_step": "Search decoders whose zero digraph has dichromatic number >= 4 (e.g. via cex_min_1 of PR 2111, whose cert = 18 < 19 forces it), and classify the minimal ones.", + "blocked_by": "Nothing structural; cex_min_1 already shows cert < v is possible, so the dichromatic question is genuinely open at the level of zero digraphs." + }, + { + "question": "What is the exact minimum of the chain cost sum_j rank_F2 B[R_j,A_j] over admissible pairings on tied_min and cex_min_1 (12 and 22 are the recorded values from PR 2111), and can the bounded B-search in verify.py be strengthened into an exact minimizer?", + "why_it_matters": "An exact chain minimum pins cert(M) between the L8 certificate and the chain bound; on tied_min the recorded spread is 11 vs 12.", + "first_step": "Branch-and-bound over admissible pairings with the block-rank sum as the objective, seeded from PR 2111's stored cost-22 pairing on cex_min_1 and the 217 recorded optima structure on tied_min.", + "blocked_by": "Needs a longer exact run than one session allows; the bounded search here records only upper bounds." + } + ] +} diff --git a/research/fstar-proof-lemmas-seed3096ed3f/VERIFY.json b/research/fstar-proof-lemmas-seed3096ed3f/VERIFY.json new file mode 100644 index 0000000000..dd95334e86 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/VERIFY.json @@ -0,0 +1,16 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/root-unit-decoder-lemmas/README.md" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "F-star proof-lemma package: engine controls (brute-force-over-all-labellings agreement at v = 3, diagonal decoder cert = 3, corrupted-witness rejection), named-instance L8 certificate reproduction on PR 2111's tied_min and cex_min_1 with independent witness replay, exact cert values by exhaustive a-enumeration at v = 5..6, the chain engine recomputed on PR 2111's stored cost-22 pairing for cex_min_1 (must equal 22), structural lemma checks (mutual-zero K4-free, no transitive 4-tournament, matched-pivot witness from MAS(H)) on every instance, and a targeted falsifier search beyond the censused domain of PR 2335 (entries -3..3 at v = 4..12; v = 13..16 entries3 and tied-heavy) with the proven chain as falsifier criterion; prints PASS_FSTAR_CONTROLS, PASS_FSTAR_NAMED, PASS_FSTAR_CHAIN_ENGINE, PASS_FSTAR_EXACT, PASS_FSTAR_STRUCTURAL, PASS_FSTAR_SEARCH and PASS_FSTAR_PROOF_LEMMAS and writes CERTIFICATE.json" + } + ] +} diff --git a/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.B22.json b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.B22.json new file mode 100644 index 0000000000..0161536922 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.B22.json @@ -0,0 +1 @@ +[[1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0], [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0], [0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]] \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.json b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.json new file mode 100644 index 0000000000..4629aa02b1 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.json @@ -0,0 +1 @@ +[[[1, -1, 0], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 0, -1], [0, 1, -1]], [[1, 0, -1], [0, 1, 1]], [[1, 0, -1], [1, -1, 0]], [[1, 0, -1], [1, 1, -1]], [[1, 0, 1], [1, 1, 0]], [[1, 0, 1], [1, 1, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, -1, 1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 0], [0, 1, 1]], [[1, 1, 0], [1, 0, 1]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.witness.json b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.witness.json new file mode 100644 index 0000000000..602d784e98 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/data/cex_min_1.witness.json @@ -0,0 +1 @@ +{"a": [3, 2, 2, 4, 4, 5, 5, 4, 1, 1, 2, 7, 5, 1, 2, 3, 6, 1, 1], "b": [1, 6, 0, 5, 6, 6, 1, 4, 3, 7, 6, 2, 1, 3, 6, 5, 2, 5, 3], "order": [16, 6, 11, 14, 5, 12, 0, 18, 17, 15, 3, 13, 10, 9, 8, 7, 4, 1], "kept": [16, 6, 11, 14, 5, 12, 0, 18, 17, 15, 3, 13, 10, 9, 8, 7, 4, 1]} \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/data/tied_min.json b/research/fstar-proof-lemmas-seed3096ed3f/data/tied_min.json new file mode 100644 index 0000000000..ae11f01fab --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/data/tied_min.json @@ -0,0 +1 @@ +[[[1, -1, -1], [0, 1, 1]], [[1, -1, -1], [1, -1, 0]], [[1, -1, -1], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/fstar-proof-lemmas-seed3096ed3f/verify.py b/research/fstar-proof-lemmas-seed3096ed3f/verify.py new file mode 100644 index 0000000000..ae745f5998 --- /dev/null +++ b/research/fstar-proof-lemmas-seed3096ed3f/verify.py @@ -0,0 +1,721 @@ +#!/usr/bin/env python3 +"""F-star proof-lemma checks: engine controls, structural lemmas on instances, +named-instance certificate reproduction, exact cert values at tiny v, and a +targeted falsifier search beyond the censused domain of +https://github.com/CrocSwap/integer-mult-bounds/pull/2335 (v = 4..12, entries +-2..2). Stdlib only, deterministic. Part of research/fstar-proof-lemmas-seed3096ed3f. + +Model (research/root-unit-decoder-lemmas section 7; PR 2111 section 1): a +T = 3 decoder is M = sum_{j=1..3} p_j q_j^T over Q on v lines with M_tt != 0. +Row support pi(t) = {j : p_j(t) != 0}, column support sigma(t) = {j : q_j(t) +!= 0}. An L8 labelling is F2 vectors a(t) supported in pi(t), b(t) supported +in sigma(t), K_ts = a(t) . b(s) mod 2. cert(M) is the largest |S| admitting +an order with K_tt = 1 on S and K_ts = 0 at every incidence M_ts = 0 with t +before s (t, s in S). cert(M) depends only on (zero pattern of M, pi, sigma). + +Engine: for fixed a-labels, the (b, order, S) completion is exact by subset +DP (b-exists for line t and blockers U is a table lookup; f[T] = OR over t in +T of f[T \\ t] and b-exists(t, blockers of T \\ t)). Exact cert enumerates all +a-labels; a witness search hill-climbs over a-labels with exact completion. +""" +import hashlib +import itertools +import json +import os +import random +import sys +import time + +sys.stdout.reconfigure(encoding="utf-8") + +HERE = os.path.dirname(os.path.abspath(__file__)) +DATA = os.path.join(HERE, "data") +T0 = time.time() + + +# ---------------------------------------------------------------- model ---- +def signature(P, Q): + v = len(P) + M = [[sum(P[t][j] * Q[s][j] for j in range(3)) for s in range(v)] for t in range(v)] + pi = [sum(1 << j for j in range(3) if P[t][j]) for t in range(v)] + sg = [sum(1 << j for j in range(3) if Q[t][j]) for t in range(v)] + Z = [[M[t][s] == 0 for s in range(v)] for t in range(v)] + assert all(M[t][t] != 0 for t in range(v)), "decoder must have nonzero diagonal" + return M, pi, sg, Z + + +def opts(pi_t): + return [m for m in range(1, 8) if not (m & ~pi_t)] + + +def bfeas_tables(pi, sg): + tabs = [] + for t in range(len(pi)): + tab = [[False] * 256 for _ in range(8)] + for am in range(1, 8): + if am & ~pi[t]: + continue + for bset in range(256): + ok = False + for b in range(1, 8): + if b & ~sg[t] or ((am & b).bit_count() & 1) == 0: + continue + good, bs = True, bset + while bs: + lb = bs & -bs + if (((lb.bit_length() - 1) & b).bit_count() & 1): + good = False + break + bs ^= lb + if good: + ok = True + break + tab[am][bset] = ok + tabs.append(tab) + return tabs + + +def blockers_pred(Z, v): + pred = [0] * v + for t in range(v): + m = 0 + for s in range(v): + if s != t and Z[s][t]: + m |= 1 << s + pred[t] = m + return pred + + +def complete(a, pi, sg, Z, v, tabs): + """Exact max |S| over (b, order, S) for fixed a-labels. Returns (value, bestT, f).""" + pred = blockers_pred(Z, v) + N = 1 << v + Abits = bytearray(N) + for U in range(1, N): + lb = U & -U + Abits[U] = Abits[U ^ lb] | (1 << a[lb.bit_length() - 1]) + f = bytearray(N) + f[0] = 1 + best, bestT = 0, 0 + for T in range(1, N): + ok, U = 0, T + while U: + lb = U & -U + u = lb.bit_length() - 1 + prev = T ^ lb + if f[prev] and tabs[u][a[u]][Abits[prev & pred[u]]]: + ok = 1 + break + U ^= lb + f[T] = ok + if ok and T.bit_count() > best: + best, bestT = T.bit_count(), T + return best, bestT, f + + +def reconstruct(a, sg, Z, v, tabs, bestT, f): + pred = blockers_pred(Z, v) + + def ab(U): + r, x = 0, U + while x: + lb = x & -x + r |= 1 << a[lb.bit_length() - 1] + x ^= lb + return r + + rev, T = [], bestT + while T: + found, U = None, T + while U: + lb = U & -U + u = lb.bit_length() - 1 + prev = T ^ lb + if f[prev] and tabs[u][a[u]][ab(prev & pred[u])]: + found = u + break + U ^= lb + assert found is not None + rev.append(found) + T ^= 1 << found + order = rev[::-1] + kept, bs = [], [0] * v + for t in order: + bset = 0 + for s in kept: + if Z[s][t]: + bset |= 1 << a[s] + for cand in range(1, 8): + if cand & ~sg[t] or ((a[t] & cand).bit_count() & 1) == 0: + continue + good, x = True, bset + while x: + lb = x & -x + if (((lb.bit_length() - 1) & cand).bit_count() & 1): + good = False + break + x ^= lb + if good: + bs[t] = cand + break + kept.append(t) + return order, bs + + +def check_witness(sig, wit): + """Independent replay of a labelling/order witness. True iff valid.""" + M, pi, sg, Z = sig + v = len(M) + a, b, order = wit["a"], wit["b"], wit["order"] + if sorted(order) != sorted(set(order)) or not order: + return False + pos = {t: i for i, t in enumerate(order)} + for t in order: + if not (1 <= a[t] <= 7) or (a[t] & ~pi[t]) or (b[t] & ~sg[t]): + return False + if (((a[t] & b[t]).bit_count() & 1)) != 1: + return False + for i, t in enumerate(order): + for s in order[i + 1:]: + if M[t][s] == 0 and (((a[t] & b[s]).bit_count() & 1)) == 1: + return False + return True + + +# ------------------------------------------------------------- controls ---- +def brute_cert(sig): + """Definition-level brute force over all labellings; MAS of D_K on V(K).""" + M, pi, sg, Z = sig + v = len(M) + best = 0 + for a in itertools.product(range(8), repeat=v): + for t in range(v): + if a[t] & ~pi[t]: + break + else: + for b in itertools.product(range(8), repeat=v): + for t in range(v): + if b[t] & ~sg[t]: + break + else: + Vk = [t for t in range(v) if ((a[t] & b[t]).bit_count() & 1)] + if len(Vk) <= best: + continue + n = len(Vk) + D = [[0] * n for _ in range(n)] + for i, t in enumerate(Vk): + for j, s in enumerate(Vk): + if t != s and M[t][s] == 0 and ((a[t] & b[s]).bit_count() & 1): + D[i][j] = 1 + acyc = [False] * (1 << n) + acyc[0] = True + mx = 0 + for T in range(1, 1 << n): + for u in range(n): + if (T >> u) & 1: + prev = T ^ (1 << u) + sink = True + for w in range(n): + if (prev >> w) & 1 and D[u][w]: + sink = False + break + if sink and acyc[prev]: + acyc[T] = True + mx = max(mx, T.bit_count()) + break + if mx > best: + best = mx + return best + + +def mas_digraph(edges, v): + """Exact maximum acyclic induced subset of a digraph given as edge list.""" + out = [0] * v + for (t, s) in edges: + out[t] |= 1 << s + acyc = bytearray(1 << v) + acyc[0] = 1 + mx = 0 + for T in range(1, 1 << v): + u = T + while u: + lb = u & -u + t = lb.bit_length() - 1 + prev = T ^ lb + if acyc[prev] and (out[t] & prev) == 0: + acyc[T] = 1 + mx = max(mx, T.bit_count()) + break + u ^= lb + return mx, acyc + + +def block_rank(rows_mask, Rj, Aj, v): + # extract submatrix (rows Rj, columns Aj) as ints over Aj columns + cols = [c for c in range(v) if (Aj >> c) & 1] + mat = [] + for t in range(v): + if (Rj >> t) & 1: + row = 0 + for i, c in enumerate(cols): + if (rows_mask[t] >> c) & 1: + row |= 1 << i + mat.append(row) + rank = 0 + for i in range(len(cols)): + piv = None + for r in range(rank, len(mat)): + if (mat[r] >> i) & 1: + piv = r + break + if piv is not None: + mat[rank], mat[piv] = mat[piv], mat[rank] + for r in range(len(mat)): + if r != rank and ((mat[r] >> i) & 1): + mat[r] ^= mat[rank] + rank += 1 + return rank + + +def chain_cost(Brows, pi, sg, v): + """sum_j rank_F2 B[R_j, A_j]; R_j = {t : j in pi(t)}, A_j = {t : j in sigma(t)}.""" + total = 0 + for j in range(3): + Rj = sum(1 << t for t in range(v) if (pi[t] >> j) & 1) + Aj = sum(1 << t for t in range(v) if (sg[t] >> j) & 1) + total += block_rank(Brows, Rj, Aj, v) + return total + + +def admissible_free_pairs(Z, v): + return [(t, s) for t in range(v) for s in range(v) if t != s and Z[t][s]] + + +def min_chain_cost(sig, budget_free=12, local_evals=250, seed=7): + """Minimum of chain cost over admissible B (0/1, unit diagonal, ones only + where M vanishes). Exhaustive when the free-pair count is small; otherwise + deterministic single-bit local search from B = I and random starts. Any B + found is an admissible upper bound on cert; a B below threshold falsifies.""" + M, pi, sg, Z = sig + v = len(M) + free = admissible_free_pairs(Z, v) + f = len(free) + + def cost_of(bits): + Brows = [0] * v + for t in range(v): + Brows[t] = 1 << t + for k, (t, s) in enumerate(free): + if (bits >> k) & 1: + Brows[t] |= 1 << s + return chain_cost(Brows, pi, sg, v) + + best_bits = 0 + best = cost_of(0) # B = I baseline + if f <= budget_free: + for bits in range(1 << f): + c = cost_of(bits) + if c < best: + best, best_bits = c, bits + else: + rng = random.Random(seed + v) + starts = [0, (1 << f) - 1] # B = I and the maximal admissible B + for st in range(2): + bits = starts[st] + cur = cost_of(bits) + if cur < best: + best, best_bits = cur, bits + for ev in range(local_evals // 4): + k = rng.randrange(f) + bits ^= 1 << k + c = cost_of(bits) + if c <= cur: + cur = c + if c < best: + best, best_bits = c, bits + else: + bits ^= 1 << k + for ev in range(local_evals // 2): + bits = rng.randrange(1 << min(f, 30)) if f <= 30 else 0 + cur = cost_of(bits) + if cur < best: + best, best_bits = cur, bits + for inner in range(8): + k = rng.randrange(f) + bits ^= 1 << k + c = cost_of(bits) + if c <= cur: + cur = c + if c < best: + best, best_bits = c, bits + else: + bits ^= 1 << k + return best, best_bits, f + + +def threshold(v): + return (2 * v) // 3 + + +# ---------------------------------------------------------- search side ---- +def hillclimb_witness(sig, budget_evals, seed): + M, pi, sg, Z = sig + v = len(M) + tabs = bfeas_tables(pi, sg) + o = [opts(pi[t]) for t in range(v)] + rng = random.Random(seed) + a = [rng.choice(o[t]) for t in range(v)] + best, bestT, f = complete(a, pi, sg, Z, v, tabs) + best_a = list(a) + evals = 1 + improved = True + while improved and evals < budget_evals: + improved = False + ts = list(range(v)) + rng.shuffle(ts) + for t in ts: + old = a[t] + for m in o[t]: + if m == old or evals >= budget_evals: + continue + a[t] = m + val, bt, ff = complete(a, pi, sg, Z, v, tabs) + evals += 1 + if val > best: + best, bestT, f = val, bt, ff + best_a = list(a) + old = m + improved = True + a[t] = old + a = best_a + order, bs = reconstruct(a, sg, Z, v, tabs, bestT, f) + return {"a": a, "b": bs, "order": order, "kept": order}, best, evals + + +def exact_cert(sig): + """Exact cert by exhaustive a-enumeration with exact completion (v <= 5).""" + M, pi, sg, Z = sig + v = len(M) + tabs = bfeas_tables(pi, sg) + o = [opts(pi[t]) for t in range(v)] + best = 0 + for a in itertools.product(*o): + val, _, _ = complete(list(a), pi, sg, Z, v, tabs) + if val > best: + best = val + return best + + +def structural_checks(sig): + """Lemma-instance checks: (i) mutual-zero graph has no K_4 (clique <= 3); + (ii) the zero digraph Z has no transitive 4-tournament; (iii) the + matched-pivot construction from MAS(H) is a valid witness of that size. + Returns (k4free_or_None, tt4free_or_None, pivot_or_None, masH); None marks + an instance where the check was skipped (v too large for the brute loops).""" + M, pi, sg, Z = sig + v = len(M) + ok_k4, ok_tt4 = None, None + if v <= 16: + ok_k4, ok_tt4 = True, True + for S in itertools.combinations(range(v), 4): + mutual = all(Z[t][s] and Z[s][t] for i, t in enumerate(S) + for s in S[i + 1:]) + if mutual: + ok_k4 = False + # transitive tournament: some order of S with all forward pairs zero + for perm in itertools.permutations(S): + if all(Z[perm[i]][perm[j]] for i in range(4) for j in range(i + 1, 4)): + ok_tt4 = False + H = [(t, s) for t in range(v) for s in range(v) if t != s and Z[t][s] and (pi[t] & sg[s])] + masH = 0 + ok_pivot = None + if v <= 12: + ok_pivot = True + masH, acyc = mas_digraph(H, v) + outH = [0] * v + for (t, s) in H: + outH[t] |= 1 << s + # matched-pivot witness: labels a(t) = b(t) = e_{c(t)}, c(t) = least bit of pi(t)&sg(t) + a = [] + for t in range(v): + d = pi[t] & sg[t] + assert d + a.append(d & -d) + # extract a largest acyclic subset of H and a sinks-first order + Tbest = max((T for T in range(1 << v) if acyc[T]), key=lambda T: T.bit_count()) + order, cur = [], Tbest + while cur: + found = False + for t in range(v): + if (cur >> t) & 1 and (outH[t] & cur) == 0: + order.append(t) + cur ^= 1 << t + found = True + break + assert found, "no sink in an acyclic set: engine bug" + wit = {"a": a, "b": list(a), "order": order, "kept": order} + ok_pivot = check_witness(sig, wit) and len(order) == masH + return ok_k4, ok_tt4, ok_pivot, masH + + +# ----------------------------------------------------------- generators ---- +def gen_instance(rng, v, lo, hi, zeros_ok=True): + while True: + P = [[rng.randint(lo, hi) for _ in range(3)] for _ in range(v)] + Q = [[rng.randint(lo, hi) for _ in range(3)] for _ in range(v)] + if all(sum(P[t][j] * Q[t][j] for j in range(3)) != 0 for t in range(v)): + M, pi, sg, Z = signature(P, Q) + return (P, Q), (M, pi, sg, Z) + + +def gen_tied(rng, v): + """Tied-heavy 2-adic construction: every product p_j(t) q_j(t) is even + (all lines isotropic at level 1), entries in {+-2, +-4} on some lines and + {+-1,+-2} on others; retained with M_tt != 0.""" + while True: + P, Q = [], [] + for t in range(v): + if t % 2 == 0: + P.append([2 * rng.choice([-2, -1, 1, 2]) for _ in range(3)]) + Q.append([2 * rng.choice([-2, -1, 1, 2]) for _ in range(3)]) + else: + P.append([rng.choice([-2, -1, 1, 2]) for _ in range(3)]) + Q.append([rng.choice([-2, -1, 1, 2]) for _ in range(3)]) + if all(sum(P[t][j] * Q[t][j] for j in range(3)) != 0 for t in range(v)): + M, pi, sg, Z = signature(P, Q) + return (P, Q), (M, pi, sg, Z) + + +def load_cfg(name): + with open(os.path.join(DATA, name), "r", encoding="utf-8") as fh: + cfg = json.load(fh) + P = [c[0] for c in cfg] + Q = [c[1] for c in cfg] + return (P, Q), signature(P, Q) + + +# ---------------------------------------------------------------- main ---- +def main(): + results = {} + out = [] + fails = [] + + def log(line): + out.append(line) + print(line) + + # ---- controls ---- + rng = random.Random(20261015) + brute_agree = 0 + for i in range(3): + v = 3 + while True: + (P, Q), sig = gen_instance(rng, v, -1, 1) + M, pi, sg, Z = sig + if any(Z[t][s] for t in range(v) for s in range(v)): + break + eb = exact_cert(sig) + bb = brute_cert(sig) + if eb == bb: + brute_agree += 1 + else: + fails.append(f"brute/engine disagree on control {i}: {bb} vs {eb}") + # diagonal control: p_j = q_j = e_j on 3 lines -> cert = 3 + P = [[1, 0, 0], [0, 1, 0], [0, 0, 1]] + sig_diag = signature(P, P) + diag_cert = exact_cert(sig_diag) + if diag_cert != 3: + fails.append(f"diagonal control: cert {diag_cert} != 3") + # witness checker corruptions (on a tiny instance with zero pairs) + (P, Q), sig_c = gen_instance(random.Random(999), 4, -1, 1) + wit_c, val_c, _ = hillclimb_witness(sig_c, 60, 5) + corrupt_rejects = 0 + if not check_witness(sig_c, wit_c): + fails.append("checker rejected a true witness") + w1 = json.loads(json.dumps(wit_c)) + w1["a"][w1["order"][0]] = 0 + if not check_witness(sig_c, w1): + corrupt_rejects += 1 + w2 = json.loads(json.dumps(wit_c)) + w2["b"][w2["order"][0]] = 0 + if not check_witness(sig_c, w2): + corrupt_rejects += 1 + # threshold table + table_ok = all(threshold(v) == (2 * v) // 3 for v in range(4, 17)) + log(f"controls: brute_agree={brute_agree}/3 diagonal_cert={diag_cert} " + f"corrupt_rejects={corrupt_rejects}/2 threshold_table={table_ok}") + if brute_agree == 3 and diag_cert == 3 and corrupt_rejects == 2 and table_ok: + log("PASS_FSTAR_CONTROLS bruteforce=3 diagonal=3 corrupt=2") + else: + fails.append("controls failed") + + # ---- named instances ---- + named = {} + for name, recorded in (("tied_min.json", 11), ("cex_min_1.json", 18)): + (P, Q), sig = load_cfg(name) + v = len(P) + if name == "tied_min.json": + wit, val, ev = hillclimb_witness(sig, 400, 20261015 + v) + else: + wpath = os.path.join(DATA, "cex_min_1.witness.json") + with open(wpath, "r", encoding="utf-8") as fh: + wit = json.load(fh) + val = len(wit["order"]) + ev = 0 + ok = check_witness(sig, wit) + if not ok: + fails.append(f"{name}: witness replay failed") + cb, _, nf = min_chain_cost(sig, budget_free=12, local_evals=150, seed=11) + named[name] = (v, val, cb, ok) + log(f"named {name}: v={v} witness={val} (PR 2111 recorded max one-copy " + f"L8 = {recorded}) chain_upper={cb} replay_ok={ok} " + f"threshold={threshold(v)} meets_threshold={val >= threshold(v)}") + if val < threshold(v): + fails.append(f"{name}: witness {val} below threshold {threshold(v)}") + log(f"PASS_FSTAR_NAMED tied_min={named['tied_min.json'][1]}/12 " + f"cex_min_1={named['cex_min_1.json'][1]}/19") + + # ---- chain-engine cross-check against PR 2111's stored pairing ---- + (Pb, Qb), sig_b = load_cfg("cex_min_1.json") + Mb, pib, sgb, Zb = sig_b + vb = len(Mb) + with open(os.path.join(DATA, "cex_min_1.B22.json"), "r", encoding="utf-8") as fh: + Bmat = json.load(fh) + Brows = [sum(1 << s for s in range(vb) if Bmat[t][s]) for t in range(vb)] + adm = all(Bmat[t][t] == 1 for t in range(vb)) and all( + Bmat[t][s] == 0 or Zb[t][s] + for t in range(vb) for s in range(vb) if t != s) + c22 = chain_cost(Brows, pib, sgb, vb) + log(f"chain-engine cross-check (PR 2111 stored cost-22 pairing on cex_min_1): " + f"admissible={adm} chain_cost={c22} (PR 2111 records ranks 10+6+6=22)") + if adm and c22 == 22: + log("PASS_FSTAR_CHAIN_ENGINE cex_min_1_B22=22") + else: + fails.append(f"B22 cross-check failed: admissible={adm} chain_cost={c22}") + + # ---- exact cert upgrades at tiny v (beyond witness level) ---- + exact_vals = [] + for i, v in enumerate((5, 5, 6)): + (P, Q), sig = gen_instance(random.Random(31337 + i), v, -3, 3) + ec = exact_cert(sig) + wit, val, _ = hillclimb_witness(sig, 80, 100 + i) + assert val <= ec + exact_vals.append((v, ec)) + log(f"exact cert (exhaustive a-enumeration, exact completion): " + f"entries3 instance i={i} v={v} cert={ec}") + log("PASS_FSTAR_EXACT " + " ".join(f"v{v}={c}" for v, c in exact_vals)) + + # ---- structural lemma checks on all search instances + named ---- + inst = 0 + k4ok = tt4ok = pivotok = True + k4n = tt4n = pivotn = 0 + for name in ("tied_min.json", "cex_min_1.json"): + (P, Q), sig = load_cfg(name) + v = len(P) + k, t, p, masH = structural_checks(sig) + if k is not None: + k4ok &= k + k4n += 1 + if t is not None: + tt4ok &= t + tt4n += 1 + if p is not None: + pivotok &= p + pivotn += 1 + inst += 1 + log(f"structural {name}: v={v} mutual_zero_K4_free={k} tt4_free={t} " + f"pivot_witness_ok={p} MAS(H)={masH if v <= 12 else 'n/a'}") + + # ---- beyond-census falsifier search ---- + search_rows = [] + falsifiers = [] + min_ratio = 1.0 + # family A: entries in {-3..3} (outside the census alphabet), v = 4..12 + # family B: v = 13..16 (outside the census v-range): entries3, tied-heavy + plans = [("entries3", v, 3) for v in range(4, 13)] + \ + [("entries3-big", v, 2) for v in (13, 14, 15, 16)] + \ + [("tied-heavy", v, 2) for v in (13, 14, 15, 16)] + fam_salt = {"entries3": 31, "entries3-big": 57, "tied-heavy": 83} + for fam, v, count in plans: + for i in range(count): + rng_i = random.Random(20261015 + 1000 * v + 17 * i + fam_salt[fam]) + if fam == "tied-heavy": + (P, Q), sig = gen_tied(rng_i, v) + else: + lo, hi = (-3, 3) if v <= 12 else (-3, 3) + (P, Q), sig = gen_instance(rng_i, v, lo, hi) + M, pi, sg, Z = sig + budget = 100 if v <= 12 else (50 if v <= 14 else 30) + wit, val, ev = hillclimb_witness(sig, budget, 700 + i + v) + ok = check_witness(sig, wit) + if not ok: + fails.append(f"search {fam} v={v} i={i}: witness invalid") + cb, bbits, nf = min_chain_cost(sig, budget_free=12, local_evals=120, + seed=3 + v) + thr = threshold(v) + ratio = val / v + min_ratio = min(min_ratio, ratio) + if cb < thr: + falsifiers.append((fam, v, i, cb, thr)) + if val < thr: + # a witness below threshold is not a falsifier (lower bound), + # but the engine should not be below the structural bound + pass + k, t, p, masH = structural_checks(sig) + if k is not None: + k4ok &= k + k4n += 1 + if t is not None: + tt4ok &= t + tt4n += 1 + if p is not None: + pivotok &= p + pivotn += 1 + if v <= 12 and val < masH: + fails.append(f"search {fam} v={v} i={i}: witness {val} < MAS(H) {masH}") + inst += 1 + search_rows.append((fam, v, i, val, cb, thr, nf)) + log(f"search {fam} v={v} i={i}: witness={val} chain_upper={cb} " + f"threshold={thr} free_pairs={nf}") + log(f"PASS_FSTAR_STRUCTURAL instances={inst} k4free={k4ok} ({k4n} checked) " + f"tt4free={tt4ok} ({tt4n} checked) pivot={pivotok} ({pivotn} checked)") + if not (k4ok and tt4ok and pivotok): + fails.append("structural checks failed") + log(f"PASS_FSTAR_SEARCH instances={len(search_rows)} falsifiers={len(falsifiers)} " + f"min_witness_ratio={min_ratio:.3f}") + if falsifiers: + for fx in falsifiers: + log(f"FALSIFIER {fx}") + fails.append("falsifier found") + + # ---- certificate ---- + cert = { + "schema_version": 1, + "engine": "a-label enumeration + exact (b, order, S) completion by subset DP", + "controls": {"brute_agree": brute_agree, "diagonal_cert": diag_cert, + "corrupt_rejects": corrupt_rejects}, + "named": {k: {"v": v, "witness": w, "chain_upper": c, "replay_ok": ok} + for k, (v, w, c, ok) in named.items()}, + "exact_cert_tiny": [{"v": v, "cert": c} for v, c in exact_vals], + "search": [{"family": f, "v": v, "i": i, "witness": w, "chain_upper": c, + "threshold": th, "free_pairs": nf} + for (f, v, i, w, c, th, nf) in search_rows], + "falsifiers": [], + "min_witness_ratio": min_ratio, + "failures": fails, + } + digest = hashlib.sha256( + json.dumps(cert, sort_keys=True).encode("utf-8")).hexdigest() + cert["digest"] = digest + with open(os.path.join(HERE, "CERTIFICATE.json"), "w", encoding="utf-8") as fh: + json.dump(cert, fh, indent=1, sort_keys=True) + log(f"certificate digest {digest[:16]} written to CERTIFICATE.json") + log(f"elapsed {time.time() - T0:.1f}s") + if fails: + for fme in fails: + log(f"FAIL: {fme}") + raise SystemExit(1) + log("PASS_FSTAR_PROOF_LEMMAS") + + +main() From 2aac4d27fb5910d44c55ab94f0ad6c1846d91b8e Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Thu, 15 Oct 2026 15:39:23 -0400 Subject: [PATCH 2/3] Docs: correct the root-unit-decoder-lemmas attribution in research/fstar-proof-lemmas-seed3096ed3f The merged package research/root-unit-decoder-lemmas (F-star, the cert(M) definition, L8 labellings, the proven chain) is from PR 1590 by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance. The previous wording, "Douglas Colkitt with OpenAI Codex assistance lineage", credited the package to the wrong author. Citation text only; no numbers, results or other prose changed. --- research/fstar-proof-lemmas-seed3096ed3f/README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/research/fstar-proof-lemmas-seed3096ed3f/README.md b/research/fstar-proof-lemmas-seed3096ed3f/README.md index 4f82d6b0c3..d6cceba5ce 100644 --- a/research/fstar-proof-lemmas-seed3096ed3f/README.md +++ b/research/fstar-proof-lemmas-seed3096ed3f/README.md @@ -276,8 +276,9 @@ installed on the authoring host; the commands above are the underlying ones. F-star, the `cert(M)` definition, L8 labellings and the proven chain `cost >= sum_j r_j >= cert(M)` are from the merged package -`research/root-unit-decoder-lemmas` (Douglas Colkitt with OpenAI Codex -assistance lineage). The rank-3 configuration model, the named instances +`research/root-unit-decoder-lemmas` ([PR 1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by +DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code +assistance). The rank-3 configuration model, the named instances `tied_min` and `cex_min_1`, their recorded one-copy certificate limits (11 and 18, CP-SAT, CHECKED (recorded)), the stored cost-22 pairing for `cex_min_1` (`data/cex_min_1.B22.json`), Lemma SCC's block-incidence digraph and L5 are From 7aed56bd440a3d8cbca8028cf2cbd0888c07d9b3 Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Thu, 15 Oct 2026 16:03:39 -0400 Subject: [PATCH 3/3] Docs: correct the root-unit-decoder-lemmas attribution in the fstar-proof-lemmas task records The merged package research/root-unit-decoder-lemmas (F-star, the cert(M) definition, L8 labellings, the proven chain) is from PR 1590 by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance. TASK.json's predecessor_authors field and TASK-CARD.md's predecessor line carried the same wrong wording the README had, "Douglas Colkitt with OpenAI Codex assistance lineage" (fixed there in 2aac4d27), crediting the package to the wrong author. Citation text only; no numbers, results, original_card or other prose changed. --- research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md | 2 +- research/fstar-proof-lemmas-seed3096ed3f/TASK.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md b/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md index 54fbddb4e2..987dadffde 100644 --- a/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md +++ b/research/fstar-proof-lemmas-seed3096ed3f/TASK-CARD.md @@ -7,4 +7,4 @@ Method; explicit parameter ranges/candidate alphabet: stdlib exact integer/F2 ar 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; Douglas Colkitt with OpenAI Codex assistance lineage), 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. +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. diff --git a/research/fstar-proof-lemmas-seed3096ed3f/TASK.json b/research/fstar-proof-lemmas-seed3096ed3f/TASK.json index af5b58ea45..0a59ee78e4 100644 --- a/research/fstar-proof-lemmas-seed3096ed3f/TASK.json +++ b/research/fstar-proof-lemmas-seed3096ed3f/TASK.json @@ -53,7 +53,7 @@ "success_evidence": "Written proofs of the structural lemmas (each demoted where incomplete) plus PASS markers from verify.py: engine/brute agreement at v = 3, the diagonal control, corrupted-witness rejection, the named-instance certificate reproduction (tied_min 11/12 and cex_min_1 18/19 machine-checked witnesses, matching PR 2111's recorded one-copy L8 maxima), exact cert values at v = 5, the chain engine recomputed on PR 2111's stored cost-22 pairing, structural lemma checks on every searched instance, and the declared-domain search summary with falsifier count.", "falsification_test": "Side A of the search is itself the falsifier test for F-star: an explicit admissible pairing B with cost(B) < floor(2v/3) refutes F-star (the chain cost >= cert(M) is proven). Side B witnesses are rejected by the independent checker if any K_tt = 1 fails or any before-pair constraint fails; corrupted copies of stored witnesses must fail verification (checked).", "time_compute_cap": "One session; compute capped at about 90 minutes single-process stdlib Python; no SAT solver, no third-party packages, no large downloads; each registered verify command capped at 600 seconds per the research_package.py limit.", - "predecessor_authors": "F-star, the cert(M) definition, L8 labellings and the proven chain cost >= sum_j r_j >= cert(M): the merged research/root-unit-decoder-lemmas package (Douglas Colkitt with OpenAI Codex assistance lineage). The rank-3 configuration model, the named instances tied_min and cex_min_1 and their recorded certificate limits: DreamingOfClouds, https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and https://github.com/CrocSwap/integer-mult-bounds/pull/2162. The falsifier census this session builds on: Aaron Wang, https://github.com/CrocSwap/integer-mult-bounds/pull/2335. This package does not claim their results; it adds structural lemmas, independent certificate reproduction and an out-of-domain search.", + "predecessor_authors": "F-star, the cert(M) definition, L8 labellings and the proven chain cost >= sum_j r_j >= cert(M): the merged research/root-unit-decoder-lemmas package (PR 1590 (https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance). The rank-3 configuration model, the named instances tied_min and cex_min_1 and their recorded certificate limits: DreamingOfClouds, https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and https://github.com/CrocSwap/integer-mult-bounds/pull/2162. The falsifier census this session builds on: Aaron Wang, https://github.com/CrocSwap/integer-mult-bounds/pull/2335. This package does not claim their results; it adds structural lemmas, independent certificate reproduction and an out-of-domain search.", "intended_artifact": "research/fstar-proof-lemmas-seed3096ed3f/ with TASK.json, SOURCES.json pins, VERIFY.json, verify.py, data/ (the named instances and one stored witness, byte-identical to PR 2111's data files), CERTIFICATE.json (written by verify.py) and 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.", "outcome": "completed", "evidence": "PROOF-LEVEL PROGRESS plus SCOPED NEGATIVE SEARCH. PROVEN (written proofs in README.md): Lemma SF (support-forced incidences vanish: K_ts = 0 whenever pi(t) intersect sigma(s) is empty, hence cert(M) >= MAS(H), cert(M) = v for acyclic block-incidence digraph H, cert(M) >= v - fvs(H)); Lemma MP (matched-pivot certificate cert(M) >= sum_i MAS(Z[C_i]) for every pivot map into D(t), cert(M) = v when the zero digraph is 3-dichromatic with pivots in D(t)); Lemma RK (mutual-zero graph K4-free, zero digraph free of transitive 4-tournaments, no incidence with |pi(t) intersect sigma(s)| = 1); Lemma AN (mod-2 anchor: for 2-integral factorizations cert(M) >= #{t : M_tt odd}, so F-star holds for dyadic decoders with at most floor(v/3) even diagonals). CHECKED by verify.py (stdlib, deterministic, 17.7 s, certificate digest 134665ac6a0800e4): controls pass (brute-force-over-all-labellings agreement 3/3 at v = 3, diagonal control cert = 3, corrupted-witness rejection 2/2); named-instance one-copy L8 certificates of PR 2111 reproduced by a different stdlib-exact method — tied_min 11/12 (re-found by the deterministic search) and cex_min_1 18/19 (stored witness replayed), both exactly matching PR 2111's recorded CP-SAT maxima and both above floor(2v/3) = 8 and 12; PR 2111's stored cost-22 pairing for cex_min_1 recomputed exactly (chain cost 22 = 10+6+6, admissible) validating the chain engine; exact cert values by exhaustive a-enumeration: two v = 5 and one v = 6 instance, each cert = v exactly; structural lemma checks on 45 instances (mutual-zero K4-free and no transitive 4-tournament on 44 with v <= 16, matched-pivot witness replayed on 28 with v <= 12); beyond-census falsifier search: 43 instances (entries {-3..3} at v = 4..12, 27 instances; v = 13..16 entries3 8 instances; v = 13..16 tied-heavy 2-adic 8 instances), falsifiers = 0, minimum witness ratio 0.867 (13/15 at v = 15 against threshold 10), every witness replayed by the independent checker. NOT PROVED: F-star itself; the residue is stated exactly (tied-minimum/isotropic lines not covered by the anchor, zero digraphs that are not 3-dichromatic, non-dyadic entries); the B-search values are bounded-search upper bounds, not exact minima.",