KB5L: tau >= 1 box floor PROVEN at v = 5 - shareable class narrowed - no kappa

research/fstar-boxfloor-v5-seedab80f07c/CERTIFICATE.json

@@ -0,0 +1,31 @@
+{
+ "certificate_digest": "0d393ada94fd3809",
+ "digests": {
+  "README.md": "fb544434d7c16709edf4cfad92d504fe542db119c9b9842eb848080c6496512a",
+  "TASK-CARD.md": "403bf9c44bff892a46614d254a7edb2fd87b0e6f8d3723bbe1e2e1a8c09f6645",
+  "TASK.json": "f83842bd1f77fc169a09446d4707983d0643bebb9f1c18643a367b9ba5f7e9cc",
+  "data/family-v5-receipt.json": "501828e06d23457d691bc1e0fbc1e1709188a2dcbd0a8ac1535229ce7fcf7f1c",
+  "data/floor-v5-receipt.json": "818accb5b25db4e9f7eecc84d705778800f867b068cc1554fbe4d2262945cf65",
+  "data/shareable-v3-receipt.json": "547e4d5b43cdbbd8a4a31359707f08c38662360debef5dfb8176a733a392aaca",
+  "family_v5.py": "f2e05b6ea6f1e3c9fd9ab8bee760f4f4d396e48c6ae58ddeff13147f926d8acd",
+  "floor_v5.py": "a2c1fbd92748ef01ffdf9e773aec0f6c5867dcda690a63d90f09740e6b452807",
+  "make_meta.py": "6db28ba420588d8ebf78f21365d1fdcbec916f04c44482155ab4ac21122542c4",
+  "shareable_v3.py": "21ee9d93e415a3f14945a2f9593354c4eda32672f65e1c281dfdffec58cf7f25",
+  "verify.py": "915efe9931dcef57d1242252d5a40a69eb0a5152e474ed28e654db88aca65b8b"
+ },
+ "markers": [
+  "PASS_KL_PINS",
+  "PASS_KL_PIN",
+  "PASS_KL_V5",
+  "PASS_KL_REALIZABLE_V5",
+  "PASS_KL_ALL",
+  "PASS_KL_PROBE",
+  "PASS_KL_SHAPES",
+  "PASS_KL_HUNT",
+  "PASS_KL_FAMILY_ALL",
+  "PASS_KJ_V3",
+  "PASS_KL_SHAREABLE"
+ ],
+ "package": "fstar-boxfloor-v5-seedab80f07c",
+ "schema_version": 1
+}

research/fstar-boxfloor-v5-seedab80f07c/SOURCES.json

@@ -0,0 +1,24 @@
+{
+ "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641",
+ "files": [
+  {
+   "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+   "path": "certificates/selected-result.json",
+   "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129",
+   "usage": "provenance"
+  },
+  {
+   "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+   "path": "docs/research/agent-task-catalog.json",
+   "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0",
+   "usage": "provenance"
+  },
+  {
+   "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb",
+   "path": "research/root-unit-decoder-lemmas/README.md",
+   "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9",
+   "usage": "input"
+  }
+ ],
+ "schema_version": 1
+}

research/fstar-boxfloor-v5-seedab80f07c/TASK-CARD.md

@@ -0,0 +1,48 @@
+# Drawn task card (verbatim): complex-new-helper-inventory
+
+Scope changed to kappa-blocker KB5L (explicit open request from discussion 1166); see TASK.json `scope_change_reason` and `actual_scope`.
+
+```json
+{
+ "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+ "allowed_variations": [
+  "Narrow to one changed boundary or helper type with explicit counts.",
+  "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+ ],
+ "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.",
+ "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.",
+ "first_step": {
+  "command": [
+   "python3",
+   "-B",
+   "research/complex-local-word-ceiling/verify.py"
+  ],
+  "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+  "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+  "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+ },
+ "id": "complex-new-helper-inventory",
+ "methods": [
+  "Propose a changed helper inventory and derive an optimistic exact moment.",
+  "Design a small completed instance and independently verify its endpoint and rank bill."
+ ],
+ "overlap_terms": [
+  "helper inventory",
+  "heterogeneous-owner",
+  "mutable leaver"
+ ],
+ "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+ "scope_change_triggers": [
+  "Mixing only providers already inside the pinned catalogue.",
+  "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+  "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+ ],
+ "starting_points": [
+  "docs/research/research-family-status.md",
+  "research/complex-local-word-ceiling/README.md",
+  "research/heterogeneous-owner-assembly/README.md",
+  "certificates/selected-result.json",
+  "research/selected-k8-unrestricted-ends/README.md"
+ ]
+}
+```

research/fstar-boxfloor-v5-seedab80f07c/TASK.json

@@ -0,0 +1,85 @@
+{
+ "actual_scope": "Kappa-blocker KB5L (authorized explicit open request): the FIRST OPEN CASE of the tau >= 1 box floor (v = 5) and the shareable-class remainder - as recorded by PR 3012 (agent-79). (a) prove box(M) >= floor(2v/3) = 3 for every exact 3-total rational decoder with v = 5 and tau >= 1, or find the minimal counterexample with box < 3 (exact both sides); (b) settle some or all of PR 2978's 21 unrealized v = 3 combinatorial patterns (shareable-class completeness); (c) report honestly what remains for F-star. 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": "d8e0f83f00191df62174b641e9fff055c357f641",
+ "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. After PR 3012 the box-floor route survives exactly on the tau >= 1 domain, PROVEN for v <= 4 and open first at v = 5 (threshold 3). This package settles v = 5 (PROVEN) and narrows the shareable-class remainder.",
+ "evidence": "VERDICT (a): the tau >= 1 box floor HOLDS at v = 5 - PROVEN. Chain: (1) exhaustive combinatorial envelope classification over all 749398 multisets of 5 raw line types with tau >= 1 (joint bit structure preserved): box = 2 on the envelope forces exactly 33 families, all of the rank-2-cap + all-pairs-even shape; (2) the anchor-attainment screen (a0 omits bit j everywhere => p_j == 0; b0 omits bit j everywhere <=> q_j == 0 or c_j > gamma) rejects 15 of the 33 as unrealizable and leaves 6 shapes up to total relabeling (5 unshareable-total rank-3 shapes + 1 zero-p-column rank-2 shape); (3) exact blocking-Z enumeration per surviving shape (per-triple kept-3 feasibility tables, all 2^20 arc subsets): the ONLY zero-arc set blocking every triple is the complete digraph; complete Z forces M diagonal, rank(M) = 5 > 3, impossible for any 3-total decoder. Hence box >= 3 = floor(2v/3) for every exact 3-total rational decoder with v = 5 and tau >= 1. Corroboration: 120 realizable tau >= 1 v = 5 decoders (tau-forced generator) all have exact box >= 5 with replayed in-box witnesses; a 35-instance hunt (tau-targeted, PR 2978-core extensions, nullspace-dense) finds 0 falsifiers. VERDICT (b): PR 2978's 3/3/21 classification replayed exactly (same seed and stages); the cap push (exact kernel q-solver, 10000 P-restarts per pattern, plus the vendored big alphabet at 2000) realizes none of the 21; one pattern is PROVEN unrealizable ((a0,b0) = (3^3,3^3) with complete Z: A1 gives p_2 == 0 so rank(M) <= 2, but complete Z forces diagonal rank 3); the remaining 20 stay CHECKED not-found-in-cap (all 20 are shareable class r_box = 3; the proven-unrealizable one forces r_box = 2, correcting PR 3012's 'all 21' framing). VERDICT (c): F-star is NOT proved and NOT refuted; cert >= floor(2v/3) has survived every falsifier test in the lineage, and the box floor is now PROVEN on the full tau >= 1 domain for v <= 5.",
+ "existing_restriction_being_changed": "PR 3012 recorded the tau >= 1 box floor as 'PROVEN for v <= 4, bounded at v = 5 (240 instances, 0 below threshold), first open case v = 5'. This package converts the bounded v = 5 evidence into a proof by exhaustive envelope classification plus exact blocking-Z enumeration, and settles one of the 21 shareable-class patterns.",
+ "falsification_test": "The v = 5 floor claim is falsified by any exact 3-total rational decoder with v = 5, tau >= 1 everywhere and exact box <= 2 (ladder-exact; both sides certified by replayed witnesses). The envelope classification is falsified by any 5-line type multiset with envelope box = 2 outside the 33 recorded families (the enumeration is exhaustive over 749398 multisets and re-runs from scratch). The blocking-Z claim is falsified by any surviving shape and any non-complete arc subset that blocks all ten triples (per-triple tables are exact kept-3 feasibility). The shareable replay is falsified by a pattern whose replay status differs from 3 realized / 3 unrealizable-column / 21 not-found-in-cap.",
+ "intended_artifact": "research/fstar-boxfloor-v5-seedab80f07c/ with verify.py (python3 -B research/fstar-boxfloor-v5-seedab80f07c/verify.py) and the vendored predecessor/pr3012/anchor_replay.py.",
+ "method": "Smallest falsifying instance first. (1) Written reduction: box depends only on (a0, b0, Z) and is monotone non-increasing in Z; Lemma SG forces Z inside the even pairs; so a realizable box-2 decoder must sit inside a box-2 combinatorial envelope. (2) Exhaustive envelope enumeration at v = 5 (749398 raw-type multisets; cheap singleton-witness test memoized, exact kept-set ladder as fallback; ladder pinned to the independent definition-level brute enumeration on 400 random configs). (3) Anchor-attainment screen (engine-definition facts) on the 33 families. (4) Exact blocking-Z enumeration per surviving shape (2^20 subsets against exact per-triple blocking tables) with the rank obstruction recorded. (5) Realizable replay on 120 tau-forced decoders; bounded falsifier hunt (35 instances). (6) Shareable class: exact replay of PR 2978's realize pipeline (same seed), then a cap push with an exact kernel q-solver. Int-only arithmetic; every acceptance engine-checked with replayed witnesses.",
+ "nearest_overlapping_prs": "PR 3012 (Lemma K, Lemma LB2, Lemma TB, the four tau = 0 falsifiers and the recorded v = 5 obstruction shape - the predecessor and handoff source), PR 2978 (Lemma V2, Lemma RT + shareable totals, the v = 3 combinatorial census and realize_kj), PR 2963, PR 2936, PR 2914 (sub-anchor box, Lemmas SB/LB). None enumerates the v = 5 combinatorial envelope, none gives the anchor-attainment screen, and none settles any of the 21 patterns.",
+ "open_questions": [
+  {
+   "blocked_by": "The same reduction works at v = 6 but the blocking-Z enumeration grows (2^30 arc subsets needs smarter propagation); no obstruction is recorded yet.",
+   "first_step": "Run the envelope classification at v = 6 (threshold 4) and enumerate blocking Z per surviving shape with constraint propagation; smallest falsifying instance first.",
+   "question": "The tau >= 1 box floor at v = 6: box >= 4 on that domain?",
+   "why_it_matters": "v = 6 is now the first open case of the tau >= 1 floor; the same envelope + blocking-Z pipeline should decide it."
+  },
+  {
+   "blocked_by": "The 20 patterns survive an exact kernel q-solver at 10000 P-restarts and the big alphabet at 2000; unrealizability needs a valuation-level argument beyond the anchor screen.",
+   "first_step": "Characterize the (a0, b0, Z) patterns forced by rank-3 factorizations with prescribed odd/even valuations (the kernel feasibility condition p(t) not in span{p(u) : (u, s) in Z} for all non-arcs is necessary and sufficient for the Z side; the anchor side needs valuations).",
+   "question": "Are the remaining 20 v = 3 combinatorial gap patterns realizable (shareable-class completeness at v = 3)?",
+   "why_it_matters": "All 20 lie in the shareable class (r_box = 3); a realization refutes box-completeness there; unrealizability would prove it."
+  },
+  {
+   "blocked_by": "The named/box/cert relations are mapped but the last rung cost >= cert has no proof-level improvement in reach.",
+   "first_step": "Use the tau-pattern control (Lemma K, LB2, TB plus this package's envelope classification) to state a joint lower bound in the shareable-class vocabulary.",
+   "question": "F-star itself: cert(M) >= floor(2v/3) at general v.",
+   "why_it_matters": "It is the named route to closing every open T = 3 window; it has survived every falsifier test in the lineage."
+  }
+ ],
+ "optimistic_full_cost_budget": "No kappa claim; the milestone is the settled v = 5 floor question. Compute cap: envelope enumeration ~25 s; blocking-Z enumeration ~6 s per shape (6 shapes); shareable replay + push ~70 s; anchor replay ~120 s; every registered command well under the 600 s cap, all blocking with periodic receipts.",
+ "original_card": {
+  "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+  "allowed_variations": [
+   "Narrow to one changed boundary or helper type with explicit counts.",
+   "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+  ],
+  "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.",
+  "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.",
+  "first_step": {
+   "command": [
+    "python3",
+    "-B",
+    "research/complex-local-word-ceiling/verify.py"
+   ],
+   "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+   "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+   "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+  },
+  "id": "complex-new-helper-inventory",
+  "methods": [
+   "Propose a changed helper inventory and derive an optimistic exact moment.",
+   "Design a small completed instance and independently verify its endpoint and rank bill."
+  ],
+  "overlap_terms": [
+   "helper inventory",
+   "heterogeneous-owner",
+   "mutable leaver"
+  ],
+  "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+  "scope_change_triggers": [
+   "Mixing only providers already inside the pinned catalogue.",
+   "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+   "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+  ],
+  "starting_points": [
+   "docs/research/research-family-status.md",
+   "research/complex-local-word-ceiling/README.md",
+   "research/heterogeneous-owner-assembly/README.md",
+   "certificates/selected-result.json",
+   "research/selected-k8-unrestricted-ends/README.md"
+  ]
+ },
+ "outcome": "completed",
+ "parameter_ranges": "v = 5 (floor) and v = 3 (shareable class); three totals; label space F2^3 bit masks; 5-line type multisets over 37 raw (a0, b0) types with tau >= 1 (749398 multisets, all joint bit structures up to line relabeling); all 2^20 arc subsets per surviving shape; integer P, Q entries in {-7..7} for the hunt and {-3,-1,1,3}/{-2,2} odd/even recipe alphabets for realization.",
+ "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/3012 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 KB5L, recorded per the assignment (discussion 1166; the first open case of the tau >= 1 box floor at v = 5 plus the shareable-class remainder, as recorded by PR 3012, is the named open request). The chooser draw (seed 77e4d785b77ca4c31a99b98a9b8143d4, track complex-mechanisms) proposed complex-new-helper-inventory, p104-side-correction and complex-rank-shape-decoder; none is this object, and the assignment takes the KB5L request instead. Pair collision check at entry (discussions 1166/1317 via disc-comments --grep, complete windows through 2026-10-16 18:00 UTC, and find_overlap.py with the object's proper names) found no CLAIM on this object: KB5k (PR 3012) was released at 17:37 UTC and KB5L was unclaimed.",
+ "scope_status": "changed",
+ "stop_rule": "Stop when the v = 5 tau >= 1 floor is settled (proved or exact minimal falsifier) and the shareable-class remainder is pushed with any settled pattern recorded. Achieved: floor PROVEN; 1 of 21 patterns PROVEN unrealizable; 20 remain CHECKED not-found-in-cap under the pushed cap. No further search without a new hypothesis.",
+ "task_id": "complex-new-helper-inventory",
+ "time_compute_cap": "One bounded pivot maximum (the v = 5 tau >= 1 floor); registered replay under 600 s per command (observed: verify.py ~250 s, anchor_replay.py ~120 s); all searches deterministic (fixed seeds and instance counts, not wall-clock caps)."
+}