F-star family gap: the box floor FAILS minimally at v = 3 - surviving tau >= 1 form exact (no kappa)

research/fstar-boxfloor-minimal-seed758ae8fe/CERTIFICATE.json

@@ -0,0 +1,29 @@
+{
+ "certificate_digest": "fb29a75bde520732",
+ "digests": {
+  "README.md": "1003d77e3d9991ccbfaba9e8f6735d0eace7eb19276ddbdd9f4710c8832c4516",
+  "TASK-CARD.md": "ab37ad3d39b5359cf51dc09c293e74d10d0fc55deb5079b005e82083e4781adc",
+  "TASK.json": "241b28a33dc5c8eaac7ea480f8a0af1c219f13e3865ca1493a3a21ce92262319",
+  "anchor_replay.py": "6104a326cd35231f312a6fc134eb25a356f7b10f2178a58260d1f94dc5eaa925",
+  "box_floor_min.py": "81c3f1c12fc4e00d2ab8c22f70e88120396d77cc63f3c93a10f3a5540acf759b",
+  "data/km-receipt.json": "6e40c9ecd2d2c0fe82ef31f77014bda09b3ed2525dec8aa6553164ab5eaf4c20",
+  "data/pivot-v5-receipt.json": "9490d06c7041e58e6eeb8e032e13a008fed6cef88d8d129cc23e6e6543a038e9",
+  "make_meta.py": "cd27ce131c594c51579d6fd3321b7633cf3dff2b78a4d4149f4698c990252734",
+  "pivot_v5.py": "268d564f5608c48a5b51d654976bc717627d1829ef98449a0edf5bfc5532d80f",
+  "verify.py": "9547c904dc90f184f4d0bd41e2c3e2d40520c69f6f0cf6c33a29f213346d72c0"
+ },
+ "markers": [
+  "PASS_KM_PINS",
+  "PASS_KM_FALSIFIER_V2",
+  "PASS_KM_FALSIFIER_V3",
+  "PASS_KM_FALSIFIER_V3B",
+  "PASS_KM_FALSIFIER_V4",
+  "PASS_KM_LB2",
+  "PASS_KM_MIXEDTAU",
+  "PASS_KM_V3TAU1",
+  "PASS_KM_PIVOT_V5",
+  "PASS_KM_ALL"
+ ],
+ "package": "fstar-boxfloor-minimal-seed758ae8fe",
+ "schema_version": 1
+}

research/fstar-boxfloor-minimal-seed758ae8fe/SOURCES.json

@@ -0,0 +1,24 @@
+{
+ "base_commit": "066f57ff795dbe6d0a0ecc11fe742eadcec00c39",
+ "files": [
+  {
+   "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+   "path": "certificates/selected-result.json",
+   "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129",
+   "usage": "provenance"
+  },
+  {
+   "git_blob": "889b95d936746df124872133ae1e7cc339adcb92",
+   "path": "docs/research/agent-task-catalog.json",
+   "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6",
+   "usage": "provenance"
+  },
+  {
+   "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb",
+   "path": "research/root-unit-decoder-lemmas/README.md",
+   "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9",
+   "usage": "input"
+  }
+ ],
+ "schema_version": 1
+}

research/fstar-boxfloor-minimal-seed758ae8fe/TASK-CARD.md

@@ -0,0 +1,70 @@
+# Local task card (KB5k) - written before substantial computation
+
+```text
+Task ID / proposed scope key: KB5k box-floor / fstar-boxfloor-minimal-seed758ae8fe
+  (chooser seed 758ae8fe94f704eed3a4bb471ba333b5, track verifier-engineering,
+  drawn cards portable-replay / replay-runtime; explicit-open-request scope change)
+Base commit; exact predecessor and dependency heads:
+  base 066f57ff795dbe6d0a0ecc11fe742eadcec00c39 (origin/main at worktree creation);
+  predecessor PR 2978 head 12eb7b832de9239a314a7cddf6c6033d618cd8f2 (agent-78,
+  vendored tree + engine lineage: PR 2963 ee755e682, PR 2936 f0ef06f13,
+  PR 2914 3f7781efc); frozen source pins untouched.
+Concrete object and question:
+  Object: the sub-anchor box value box(M) of exact 3-total rational decoders
+  M = sum_{j<=3} p_j q_j^T on v lines (M_tt != 0).
+  Question (a): does box(M) >= floor(2v/3) hold for ALL such decoders (the
+  surviving box-floor link of the PR 2914/2978 chain)? If not: the minimal
+  decoder with box < floor(2v/3), exact both sides, cert reported alongside.
+  Then (one bounded pivot): the tau >= 1 restriction of the same floor
+  (PR 2978's stated surviving domain), and the structural control of box by
+  the tau pattern, the shareable count r_box = |{j : c_j = gamma}| and tied
+  totals (the shareable-class vocabulary of PR 2978 Lemma RT).
+Scope status: changed (authorized explicit open request from discussion 1166);
+  reason: the recorded remainder of PR 2978 (agent-78) - the box-floor route
+  plus shareable-class completeness - was assigned to this session; the drawn
+  verifier-engineering cards do not match this object.
+Existing restriction being changed (or exact claim being audited):
+  Audits PR 2978's stated surviving chain link "box >= floor(2v/3) would close
+  F-star" as a claim about ALL exact 3-total rational decoders (its own
+  counterexample has box = 2 = floor(2v/3) at v = 3, so it did not test the
+  floor); and PR 2936's tau >= 1 necessity pin (its tau = 0 demo is v = 2,
+  box = 1 = floor(2v/3), also not a floor falsifier).
+Method; explicit parameter ranges/candidate alphabet:
+  (1) Smallest falsifying instance first: construct exact integer decoders at
+  v = 2, 3 with prescribed tau patterns; exact cert/box by the vendored PR 2914
+  engine AND an independent section-7/box definition enumeration; int-only.
+  (2) Exhaustive combinatorial box census at v = 3 over all Lemma-SG-consistent
+  (a0, b0, Z) patterns INCLUDING lines with tau = 0 (PR 2978 job B restricted
+  to tau >= 1 per line); box exact per config; min box per tau-pattern class.
+  (3) Written lower-bound lemmas (two-line repair; tied-bit matched pivot) and
+  their machine checks; then the tau >= 1 pivot at v = 5 (floor 3): bounded
+  search for box <= 2 with exact obstruction records per route.
+Nearest overlapping PRs and why this adds something:
+  PR 2914 (sub-anchor box, Lemmas SB/LB), PR 2936 (Lemma BPP, tau >= 1 needed
+  for box = cert), PR 2963 (tied_min v = 11, box weak cell), PR 2978 (Lemma V2,
+  Lemma RT + shareable totals, minimal box = cert counterexample v = 3).
+  None tests the box FLOOR against decoders with tau = 0 lines, and none states
+  a box lower bound in terms of the tau pattern; this package does both.
+Declared milestone: local module (scoped obstruction / exact falsifier + exact
+  structural bounds; no kappa, no supplier).
+Optimistic full cost budget; required observable improvement:
+  No kappa claim; the deliverable is the settled floor question. Compute cap:
+  combinatorial v = 3 census (seconds), realization and v = 5 pivot bounded
+  (minutes), every number replayed exactly.
+Unresolved consumer/restoration costs; family expansion decision if continuing:
+  Not applicable (no physical construction). Family expansion: none; the
+  shareable-class completeness question (PR 2978's 21 patterns) stays open and
+  is recorded as the next question unless resolved incidentally.
+Success evidence; falsification test; time/compute cap:
+  Success: exact minimal falsifier (both sides replayed + independent
+  enumeration) or a proof of the floor; every claim labelled PROVEN/CHECKED/
+  DEMOTED. Falsification: replay stored witnesses; re-enumerate cert and box
+  from the definitions; any v = 3 config with a different exact box refutes the
+  census. Cap: registered replay under 600 s; one bounded pivot maximum.
+Predecessor authors; intended artifact and reproduction command:
+  PR 1590 DreamingOfClouds (Claude Opus 5.5 (Anthropic) via Claude Code
+  assistance); PR 2111 DreamingOfClouds; PRs 2717/2747/2774/2869/2890/2901/
+  2914/2936/2963/2978 Aaron Wang (navinor) - verify each at current ground
+  truth before writing. Artifact: research/fstar-boxfloor-minimal-seed758ae8fe/
+  with verify.py (python3 -B research/fstar-boxfloor-minimal-seed758ae8fe/verify.py).
+```

research/fstar-boxfloor-minimal-seed758ae8fe/TASK.json

@@ -0,0 +1,79 @@
+{
+ "actual_scope": "Kappa-blocker KB5k (authorized explicit open request): THE SURVIVING BOX-FLOOR ROUTE to F-star, plus shareable-class completeness - the recorded remainder of PR 2978 (agent-78). (a) Does the sub-anchor box satisfy box(M) >= floor(2v/3) for every exact 3-total rational decoder (a proof would close F-star directly via cert >= box), or what is the MINIMAL decoder with box < floor(2v/3) (cert reported alongside, exact both)? (b) the shareable-class question of PR 2978 (its 21 unrealized v = 3 combinatorial gap patterns). (c) if the box floor fails but cert survives, the replacement lower bound linking named/box to cert in the shareable-class vocabulary. One bounded pivot maximum; smallest falsifying instance first.",
+ "ai_assistance": "Substantial AI assistance: this package was produced by Aaron Wang with help from opencode (opencode agent harness). No model named per orchestrator attribution rules. No independent human review claimed.",
+ "author": "Aaron Wang (with help from opencode)",
+ "base_commit": "066f57ff795dbe6d0a0ecc11fe742eadcec00c39",
+ "bottleneck_link": "F-star (cert(M) >= floor(2v/3), research/root-unit-decoder-lemmas section 7) is the named route to closing every open T = 3 window at once. PR 2978 killed the completeness link of the PR 2914 chain and left the box-floor link (box >= floor(2v/3)) as the surviving route. This package settles that route: the floor FAILS on the full class (minimal falsifier v = 3, cert = 3 >= 2 = floor > box = 0), so the route needs the tau >= 1 restriction; there the floor is PROVEN for v <= 4 (Lemma LB2) and stays open at v >= 5 (bounded exact search: 240 instances, 0 violations).",
+ "evidence": "VERDICT: the box-floor route as stated (all exact 3-total rational decoders) is REFUTED, minimally at v = 3 in the rank-3 class. PROVEN: box = 0 iff every line has tau = 0 (a kept line needs a tied bit); the minimal falsifier F3-tau0 P = [[1,1,0],[1,0,1],[0,1,1]], Q = [[2,2,1],[2,1,2],[1,2,2]], M = I + 3J (rank 3, tau = (0,0,0), r_box = 3, no zero arcs) has cert = 3 (replayed witness; trivial upper bound v) > 2 = floor(2v/3) > 0 = box, both sides exact by the vendored engine AND an independent definition-level enumeration. PROVEN minimal: rank 3 forces v >= 3; a rank-2 wide-class falsifier exists at v = 2 (box = 0 < 1 = floor(2v/3)); v = 3 gradient tau = (1,0,0) gives cert = 3 > 2 > 1 = box; v = 4 tau = (0,0,0,0) gives cert = 4 > 2 > 0 = box. F-star is NOT refuted (cert >= floor on every falsifier). PROVEN (Lemma LB2, two-line repair): any two lines with tau >= 1 are jointly box-keepable, so box >= min(2, #keepable lines); machine-checked on 16761 canonical v = 3 configs and 160 random realizable decoders v = 4..6. Consequences: the tau >= 1 box floor is PROVEN for v <= 4 (threshold <= 2) and first open at v = 5 (threshold 3). CHECKED: v = 3 tau >= 1 domain min box = 2 = floor (3023 canonical configs recomputed, 27 gap candidates all exactly 2); mixed-tau formula on 240 realizable decoders; bounded v = 5 tau >= 1 search (240 exact instances, 97 with r_box = 2, 0 below threshold). Exact obstruction to a v = 5 falsifier recorded: Lemma RT caps a kept set at r_box only when all its forward pairs are zero arcs, so box <= 2 needs every 3-subset blocked in every order - Z-complete triples (all 6 ordered pairs zero arcs) are the only rank route and rank(M) = 3 permits them only for |S| <= 3; every other order must fail bilinearly. Shareable-class completeness (PR 2978's 21 patterns) remains open.",
+ "existing_restriction_being_changed": "Audits PR 2978's stated surviving chain link 'a box floor box >= floor(2v/3) ... would close F-star' as a claim about ALL exact 3-total rational decoders. PR 2978's own counterexample has box = 2 = floor(2v/3) at v = 3 (not a floor falsifier), and PR 2936's tau = 0 demonstration is v = 2 with box = 1 = floor(2v/3) (also not one), so the floor itself was never tested against decoders with tau = 0 lines. This package tests it, refutes it minimally, and states the exact surviving form (tau >= 1 domain) with its proved range and bounded open range.",
+ "falsification_test": "Every falsifier claim is falsified by replaying the stored witnesses and recomputing both rungs from the definitions: verify.py reruns the vendored PR 2914 engine (exhaustive) AND an independent definition-level enumeration (brute over all label assignments for v <= 3, trivial upper bound v for cert = v), asserts identities (tie parity, scope identity), rank = 3, and box == min(2, #keepable) on each falsifier. Lemma LB2 is falsified by any of the 16761 enumerated configs where its explicit construction fails the from-definition check. The v = 5 bounded claim is falsified by any tau >= 1 instance with box <= 2 (the search is bounded, NOT a non-existence result).",
+ "intended_artifact": "research/fstar-boxfloor-minimal-seed758ae8fe/ with verify.py (python3 -B research/fstar-boxfloor-minimal-seed758ae8fe/verify.py) and anchor_replay.py.",
+ "method": "Smallest falsifying instance first. (1) Exact integer constructions with prescribed tau patterns at v = 2, 3, 4; exact cert/box by the vendored PR 2914 engine plus an independent section-7/box definition enumeration; int-only arithmetic; rank checked exactly over Q. (2) Written lower bounds: the keepable-line characterization (box = 0 iff all tau = 0), Lemma LB2 (two-line repair, constructive), and the Lemma RT/shareable-totals upper bound of PR 2978 for the obstruction picture; machine replay of the LB2 construction on every canonical v = 3 config with >= 2 keepable lines (including tau = 0 lines, which PR 2978 job B excluded) and on random realizable decoders v = 4..6. (3) Recomputation of PR 2978 job B (3023 canonical configs; the vendored receipt ships empty, so everything is recomputed from scratch). (4) One bounded pivot: exact kept-set feasibility ladder at v = 5 (threshold 3) over 240 realizable decoders from three generators (random valuation-tuned, extensions of PR 2978's counterexample core with r_box = 2, unit-role templates), exact box/cert on every would-be hit.",
+ "nearest_overlapping_prs": "PR 2978 (Lemma V2, Lemma RT + shareable totals, minimal box = cert counterexample v = 3 - the predecessor and handoff source), PR 2963 (tied_min v = 11 exact, box weak cell), PR 2936 (Lemma BPP, tau >= 1 necessary for box = cert, tau = 0 demo at v = 2), PR 2914 (sub-anchor box, Lemmas SB/LB). None tests the box FLOOR against tau = 0 lines and none gives a box LOWER bound in terms of the tau pattern; this package does both and settles the floor's minimal failure.",
+ "open_questions": [
+  {
+   "blocked_by": "No realizability characterization beyond Lemma SG + the column-attainment condition; PR 2978's search is bounded (not-found-in-cap is not unrealizable).",
+   "first_step": "Characterize the (a0,b0,Z) patterns forced by rank-3 factorizations with prescribed odd/even valuations; extend PR 2978's realize_kj.py with a valuation-level enumeration.",
+   "question": "Are PR 2978's 21 remaining v = 3 combinatorial gap patterns realizable (shareable-class completeness at v = 3)?",
+   "why_it_matters": "All 21 lie in the shareable class (r_box = 3); a realization refutes box-completeness there too, unrealizability proves it."
+  },
+  {
+   "blocked_by": "The exact obstruction recorded here: Lemma RT blocks a kept set only via all-forward-zero-arc orders capped at r_box, and rank(M) = 3 allows Z-complete triples only at |S| <= 3; all other orders must fail bilinearly, which no search domain has exhausted.",
+   "first_step": "Either prove box >= 3 for every tau >= 1 decoder at v = 5 (e.g. a three-line repair generalizing Lemma LB2 with the rank-3 constraint), or construct one with box = 2 exactly (r_box <= 2 is necessary by Lemma RT).",
+   "question": "The tau >= 1 box floor at v >= 5: is box >= floor(2v/3) on that domain? First open case v = 5 (threshold 3).",
+   "why_it_matters": "It is the exact surviving form of the box-floor route once the tau = 0 falsifiers of this package are excluded; a proof would close F-star on the tau >= 1 domain (the domain all prior evidence lives in)."
+  },
+  {
+   "blocked_by": "The shareable-class vocabulary is new; the right lower bound is not yet stated.",
+   "first_step": "State and test a candidate bound in terms of the tau pattern, r_box and the tied-bit coloring MAS sums (Lemma TB sketch: box >= max over tied-bit colorings of sum_j MAS(Z[C_j])).",
+   "question": "The replacement lower bound linking named/box to cert after the box floor died: what structural features control box?",
+   "why_it_matters": "PR 2978's chain now needs a different lower rung; this package supplies the tau-pattern control (box = 0 iff all tau = 0; box >= min(2, #keepable)) and the shareable-count upper cap as the first pieces."
+  }
+ ],
+ "optimistic_full_cost_budget": "No kappa claim; the milestone is the settled floor question. Compute cap: falsifier jobs seconds; LB2 replay ~150 s of canonical configs (v = 3, one pass); v = 5 pivot 240 exact instances ~290 s; anchor replay ~120 s; every command under the 600 s cap, all blocking.",
+ "original_card": {
+  "acceptance_gate": "Preserve immutable source hashes and proof-relevant content; a different compressed byte stream alone is not a mathematical mismatch.",
+  "allowed_variations": [
+   "One interpreter/version mismatch or one payload field comparison."
+  ],
+  "bottleneck_link": "Portable exact checks prevent environment failures from blocking valid contributions.",
+  "first_experiment": "Reproduce one specific mismatch or audit one canonical comparison for omitted proof-relevant fields.",
+  "first_step": {
+   "command": [
+    "python3",
+    "-B",
+    "scripts/research_baseline.py"
+   ],
+   "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+   "inspect": "Read the gzip-container reproducibility examples and distinguish frozen source bytes from regenerated payloads.",
+   "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+  },
+  "id": "portable-replay",
+  "methods": [
+   "Reproduce one portability failure and add a minimal cross-environment fix.",
+   "Audit one canonical-payload comparison for omitted proof-relevant fields."
+  ],
+  "overlap_terms": [
+   "gzip container",
+   "reproducibility",
+   "canonical payload"
+  ],
+  "question": "Can one reproducible environment or artifact-comparison failure be repaired?",
+  "scope_change_triggers": [
+   "Removing immutable-source pins because generated compressed bytes differ."
+  ],
+  "starting_points": [
+   "research/gzip-container-reproducibility/README.md",
+   "docs/ci-verification.md"
+  ]
+ },
+ "outcome": "completed",
+ "parameter_ranges": "v = 2..5; three totals; label space F2^3 bit masks; integer P, Q entries in {-4..4}; 2-adic valuations 0..3; falsifiers at v = 2, 3, 4 with tau patterns (0,0), (0,0,0), (1,0,0), (0,0,0,0); LB2 replay on 16761 canonical v = 3 configs (all Lemma-SG-consistent (a0,b0,Z) with >= 2 keepable lines, up to line/total relabeling) and 160 random realizable decoders v = 4..6; mixed-tau sweep 240 realizable decoders v = 3..4; v = 5 pivot 240 realizable tau >= 1 decoders (80 random + 80 PR 2978-core extensions + 80 unit-role templates).",
+ "predecessor_authors": "PR 1590 DreamingOfClouds (Claude Opus 5.5 (Anthropic) via Claude Code assistance); PR 2111 DreamingOfClouds; PRs 2717/2747/2774/2869/2890/2901/2914/2936/2963/2978 Aaron Wang (navinor); all verified at current ground truth with gh pr view --json author,title on 2026-10-16.",
+ "schema_version": 1,
+ "scope_change_reason": "Authorized 'explicit open request' scope change to kappa-blocker KB5k, recorded per the assignment (discussion 1166; the recorded remainder of PR 2978 - the surviving box-floor route plus shareable-class completeness - is the named open request). The chooser OS draw (seed 758ae8fe94f704eed3a4bb471ba333b5, track verifier-engineering) proposed portable-replay and replay-runtime; neither is this object, and the assignment takes the KB5k request instead.",
+ "scope_status": "changed",
+ "stop_rule": "Stop when the box floor is settled (proved, minimal falsifier, or exact obstruction with minimal demo) and the one bounded pivot is recorded. Achieved: minimal falsifier PROVEN at v = 3 (rank-3 class), tau >= 1 floor PROVEN for v <= 4, bounded at v = 5 (240 instances, 0 hits). No further search without a new hypothesis.",
+ "task_id": "portable-replay",
+ "time_compute_cap": "One bounded pivot maximum (the tau >= 1 v = 5 question); registered replay under 600 s per command (observed: verify.py ~300 s, anchor_replay.py ~120 s); all searches deterministic (fixed seeds, instance counts, not wall-clock caps)."
+}