diff --git a/research/window-break-even-4470/README.md b/research/window-break-even-4470/README.md new file mode 100644 index 0000000000..89b5e4150e --- /dev/null +++ b/research/window-break-even-4470/README.md @@ -0,0 +1,132 @@ +# Short label windows under the #4470 invoice: break-even line counts vs the Theorem B cap + +**Optimistic model screen; no new κ, no supplier, no native word.** Under the +productive-helper accounting of the selected #4470 word, a shorter label window +h (fewer fresh axes d = h − 1 per thick stage) lowers the cost a line system may +pay per line. It also raises the number of lines per dimension the system needs. +For dense units with one deleted frame (the case of every built complex +supplier), the windows h = 3, 4, 5 and 7 need more lines per dimension than the +proven cap v/T ≤ 2^k′ + 1 of +[line-system-saturation](../line-system-saturation/README.md) (Theorem B) allows. +h = 6 misses by about 2%. So a "smaller fresh block" does not by itself pay. +The live cells are the even windows h = 6 and h = 8, and deleting more than one +frame. + +## Model + +[verify.py](verify.py) rebuilds the complex invoice of +[joint-helper-lattice](../joint-helper-lattice/README.md) (#4470) **exactly** +from its `RESULT.json` local data: 18 full calls, 16 pairs with prefix 7, +15 query shears per port, local helpers and local paid, and a centre of 8 jobs of rank 8. +The targets and paid histograms match bit for bit, and the root is +0.003020165977 (recorded rounding 0.00302015). + +It then replaces E8/P112 by a line system with v lines of rank T, window h +(fresh block d = h − 1), decoder cost D, and k deleted lines that become centres: + +- ports V = v − k, centre per call D − k (the E8 floor 72 − k of PR968), paid as T jobs; +- the same #4440 controller (main targets 1 + d(p+2), idle pairs d(j+1) → d(j+1)+1, V(p − 1) query shears); +- the #4470 local native word with counts scaled by V/112 and ranks by d/8, which keeps the exact mass neutrality of the fresh-axis work; +- p and a re-optimised (p = 3..40). + +The surplus is then exactly **S = (p+2)(v − D) − V** (checked in exact arithmetic +on 16 instances). For E8/P112, (p+2)(v − D) − V = 18·48 − 112 = 752. + +This is an optimistic screen, not a lower bound. It assumes that a native word +with free central shears exists for the new unit and that its local profile +scales like the E8 one. The dense estimate D = hT is used where no better +decoder is known. + +## Results (RESULT.json) + +Named systems, with (v, T, h, D) taken from +[char2-threshold](../char2-threshold/README.md) §2 and +[line-system-saturation](../line-system-saturation/README.md) §8: + +| system | v | T | h | D | x = D/v | C | / record | +|---|---:|---:|---:|---:|---:|---:|---:| +| E8 P112 (selected) | 120 | 8 | 9 | 72 | .600 | .00302017 | 1.000 | +| E8 P111 (k = 9) | 120 | 8 | 9 | 72 | .600 | .00305122 | 1.010 | +| E8 P104 (k = 16, not built) | 120 | 8 | 9 | 72 | .600 | .00328625 | 1.088 | +| E7 | 63 | 7 | 7 | 49 | .778 | .00214394 | 0.710 | +| E7, two frames deleted | 63 | 7 | 7 | 49 | .778 | .00249251 | 0.825 | +| E6, D4, D5, D6, Z8 (ties) | | | | = v | 1 | 0 | 0 | +| E8+A3 | 140 | 11 | 11 | 121 | .864 | .00071929 | 0.238 | +| D16⁺ (256 spinors / Delsarte cap 557) | 496 / 557 | 16 | 17 | 272 | .548 / .488 | .00170 / .00196 | 0.565 / 0.649 | +| D24⁺ | 728 | 24 | 25 | 600 | .824 | .00039395 | 0.130 | + +The P111 and P104 rows only show the model's dependence on V. They are not +claims about those words. + +Dense units **at the Theorem B cap** (lines per dimension 2^k′ + 1 for odd h, 2^k′ for even h), +as a multiple of the record, for k = T, 2T and 3T deleted lines: + +| h | cap v/T | dense x | k = T | k = 2T | k = 3T | +|---:|---:|---:|---:|---:|---:| +| 3 | 3 | 1 | 0 | 0 | – | +| 4 | 4 | 1 | 0 | 0 | 0 | +| 5 | 5 | 1 | 0 | 0 | 0 | +| 6 | 8 | .75 | 0.980 | 1.166 | 1.435 | +| 7 | 9 | .778 | 0.710 | 0.825 | 0.983 | +| 8 | 16 | .5 | 1.460 | 1.580 | 1.720 | +| 9 | 17 | .529 | 1.194 | 1.285 | 1.391 | + +At k′ ≤ 2 a saturated dense unit has D = hT = v, so it has no saving at all, +whatever the accounting. + +Break-even lines per dimension (k = T) to tie the record. Columns: h, needed v/T, cap. +3: 3.34 / 3; 4: 4.72 / 4; 5: 6.29 / 5; 6: 8.05 / 8; 7: 10.06 / 9; 8: 12.36 / 16; +9: 15.0 / 17 (E8 has 15); 11: 21.7 / 33; 13: 31.2 / 65; 15: 45.5 / 129; 17: 69.9 / 257; +19: 119.5 / 513. At h ≥ 21 no v/T up to 200 ties the record. The best known +systems above h = 9 (line-system-saturation §8.1: 12.7 at h = 11, 12.8 at h = 13, 31 at h = 17) +are far below these needs. + +Compared with the pre-#4359 fit x\*(h) = .5385 − .01495(h − 9) used by +line-system-saturation, the new break-even dense ratio is much looser at short +windows (h = 7: .696 vs .568) and much stricter at long ones (h = 17: .243 vs .419). +Shorter windows help per line, but the cap on lines per dimension takes it back. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3.12 scripts/research_package.py --package research/window-break-even-4470 --check-only +python3.12 scripts/research_package.py --package research/window-break-even-4470 +``` + +`verify.py` takes about 3 minutes on one core and replays `RESULT.json` +(`--write` regenerates it). `test_verify.py` has rejecting controls (a changed helper count, +a dropped centre, a wrong pair count) and positive controls (a tie unit has no saving, +the saving grows with lines per dimension, the Theorem B caps, the root lies near S/G). + +## Limits + +- The scaled local word is a proxy. A real native word for E7 or a new unit can price differently, + and its central shears may not be free. +- Only dense pairings and the D − k centre rule are modelled. Sparser admissible pairings + (line-system-saturation §11.4) and overcomplete decoders are outside this screen. +- The BIT side (κ = min(complex, BIT)) is not rebuilt. A complex gain above the BIT gate + needs the same change there. +- The overlap search (`scripts/find_overlap.py`, 2026-10-23, open PRs and discussions refreshed, + closed PRs from a 2026-10-18 cache) found the earlier paper-side screens (#2244, #2873, + discussion #3622) and no re-pricing of label windows under the #4470 invoice. + +## Open next questions + +1. **Even windows h = 6 and h = 8.** Does a saturated even-window system exist (v = 8T with + 1 ∈ col Ā at k′ = 3, or v = 16T at k′ = 4)? These are the only short windows whose + cap clears the record here. h = 6 needs two deleted frames (×1.17 at the cap), + h = 8 needs 12.4 of the 16 allowed lines per dimension. First step: extend the + realisability numerics of line-system-saturation §10 to even windows. +2. **Deleted frames.** Is the centre floor D − k attainable beyond one deleted frame? The h = 6 + and h = 7 verdicts change between k = T and k = 2T or 3T, and for E8 only P112 and P111 are built. + First step: state the E7 analogue of the PR968 floor and test it on the 63-line unit. + +## Credit + +Prepared by Mark (Matarener) with substantial Claude Code (Claude) assistance. +It uses the #4470 invoice of joint-helper-lattice (built on zxv's native supplier and the +PR4440/PR4441/PR4447 contributions credited there), +the cost table of char2-threshold and the Theorem B cap and construction table of +line-system-saturation, all unchanged and referenced without vendoring. New work is Apache-2.0. diff --git a/research/window-break-even-4470/RESULT.json b/research/window-break-even-4470/RESULT.json new file mode 100644 index 0000000000..408a16fdcd --- /dev/null +++ b/research/window-break-even-4470/RESULT.json @@ -0,0 +1,336 @@ +{ + "record_rounded": "60403/20000000", + "calibration_root": 0.003020165977, + "surplus_identity": "S = (p+2)(v-D) - V, checked exactly on 16 instances", + "systems": { + "E8 P112 (selected #4470)": { + "v": 120, + "T": 8, + "h": 9, + "D": 72, + "k": 8, + "x": 0.6, + "C": 0.00302017, + "ratio": 1.0, + "p": 16, + "a": 7, + "source": "char2-threshold G1.E8-gain; line-system-saturation c1" + }, + "E8 P111": { + "v": 120, + "T": 8, + "h": 9, + "D": 72, + "k": 9, + "x": 0.6, + "C": 0.00305122, + "ratio": 1.0103, + "p": 16, + "a": 7, + "source": "centre 63 (selected bit P111 analogue)" + }, + "E8 P104": { + "v": 120, + "T": 8, + "h": 9, + "D": 72, + "k": 16, + "x": 0.6, + "C": 0.00328625, + "ratio": 1.0881, + "p": 15, + "a": 7, + "source": "centre 56; complex P104 not built" + }, + "E7 roots": { + "v": 63, + "T": 7, + "h": 7, + "D": 49, + "k": 7, + "x": 0.7778, + "C": 0.00214394, + "ratio": 0.7099, + "p": 31, + "a": 15, + "source": "char2-threshold G1.E7-gain" + }, + "E7 roots, two frames deleted": { + "v": 63, + "T": 7, + "h": 7, + "D": 49, + "k": 14, + "x": 0.7778, + "C": 0.00249251, + "ratio": 0.8253, + "p": 27, + "a": 13, + "source": "same, k = 2T" + }, + "E6 roots": { + "v": 36, + "T": 6, + "h": 7, + "D": 36, + "k": 6, + "x": 1.0, + "C": 0.0, + "ratio": 0.0, + "p": null, + "a": null, + "source": "char2-threshold G1.E6-tie" + }, + "D6 roots": { + "v": 30, + "T": 6, + "h": 5, + "D": 30, + "k": 6, + "x": 1.0, + "C": 0.0, + "ratio": 0.0, + "p": null, + "a": null, + "source": "char2-threshold G1.D-ties" + }, + "D5 roots": { + "v": 20, + "T": 5, + "h": 5, + "D": 20, + "k": 5, + "x": 1.0, + "C": 0.0, + "ratio": 0.0, + "p": null, + "a": null, + "source": "char2-threshold G1.D-ties" + }, + "D4 roots": { + "v": 12, + "T": 4, + "h": 3, + "D": 12, + "k": 4, + "x": 1.0, + "C": 0.0, + "ratio": 0.0, + "p": null, + "a": null, + "source": "char2-threshold G1.D-ties" + }, + "Z8 (56 lines)": { + "v": 56, + "T": 8, + "h": 7, + "D": 56, + "k": 8, + "x": 1.0, + "C": 0.0, + "ratio": 0.0, + "p": null, + "a": null, + "source": "line-system-saturation 8.1, dense" + }, + "E8+A3 (norms 6)": { + "v": 140, + "T": 11, + "h": 11, + "D": 121, + "k": 11, + "x": 0.8643, + "C": 0.00071929, + "ratio": 0.2382, + "p": 40, + "a": 19, + "source": "line-system-saturation 8.1, dense" + }, + "D16+ roots + 256 spinors": { + "v": 496, + "T": 16, + "h": 17, + "D": 272, + "k": 16, + "x": 0.5484, + "C": 0.00170492, + "ratio": 0.5645, + "p": 15, + "a": 7, + "source": "line-system-saturation 8.1, dense" + }, + "D16+ Delsarte cap 557": { + "v": 557, + "T": 16, + "h": 17, + "D": 272, + "k": 16, + "x": 0.4883, + "C": 0.00195854, + "ratio": 0.6485, + "p": 13, + "a": 6, + "source": "line-system-saturation 8.2 upper bound" + }, + "D24+ roots + 176 spinors": { + "v": 728, + "T": 24, + "h": 25, + "D": 600, + "k": 24, + "x": 0.8242, + "C": 0.00039395, + "ratio": 0.1304, + "p": 40, + "a": 19, + "source": "line-system-saturation 8.1, dense" + } + }, + "at_theorem_B_cap": { + "3": { + "cap_v_per_T": 3, + "dense_x": 1.0, + "k=1T": 0.0, + "k=2T": 0.0, + "k=3T": null + }, + "4": { + "cap_v_per_T": 4, + "dense_x": 1.0, + "k=1T": 0.0, + "k=2T": 0.0, + "k=3T": 0.0 + }, + "5": { + "cap_v_per_T": 5, + "dense_x": 1.0, + "k=1T": 0.0, + "k=2T": 0.0, + "k=3T": 0.0 + }, + "6": { + "cap_v_per_T": 8, + "dense_x": 0.75, + "k=1T": 0.9797, + "k=2T": 1.1663, + "k=3T": 1.4348 + }, + "7": { + "cap_v_per_T": 9, + "dense_x": 0.7778, + "k=1T": 0.7099, + "k=2T": 0.8253, + "k=3T": 0.9825 + }, + "8": { + "cap_v_per_T": 16, + "dense_x": 0.5, + "k=1T": 1.4602, + "k=2T": 1.5803, + "k=3T": 1.7204 + }, + "9": { + "cap_v_per_T": 17, + "dense_x": 0.5294, + "k=1T": 1.1935, + "k=2T": 1.2848, + "k=3T": 1.3905 + } + }, + "break_even_k_eq_T": { + "3": { + "v_per_T": 3.34, + "cap": 3, + "dense_x": 0.8991 + }, + "4": { + "v_per_T": 4.72, + "cap": 4, + "dense_x": 0.8473 + }, + "5": { + "v_per_T": 6.29, + "cap": 5, + "dense_x": 0.7955 + }, + "6": { + "v_per_T": 8.05, + "cap": 8, + "dense_x": 0.7452 + }, + "7": { + "v_per_T": 10.06, + "cap": 9, + "dense_x": 0.6958 + }, + "8": { + "v_per_T": 12.36, + "cap": 16, + "dense_x": 0.6474 + }, + "9": { + "v_per_T": 15.0, + "cap": 17, + "dense_x": 0.6 + }, + "10": { + "v_per_T": 18.07, + "cap": 32, + "dense_x": 0.5533 + }, + "11": { + "v_per_T": 21.68, + "cap": 33, + "dense_x": 0.5073 + }, + "12": { + "v_per_T": 25.98, + "cap": 64, + "dense_x": 0.462 + }, + "13": { + "v_per_T": 31.16, + "cap": 65, + "dense_x": 0.4172 + }, + "14": { + "v_per_T": 37.53, + "cap": 128, + "dense_x": 0.373 + }, + "15": { + "v_per_T": 45.54, + "cap": 129, + "dense_x": 0.3294 + }, + "16": { + "v_per_T": 55.92, + "cap": 256, + "dense_x": 0.2861 + }, + "17": { + "v_per_T": 69.87, + "cap": 257, + "dense_x": 0.2433 + }, + "18": { + "v_per_T": 89.52, + "cap": 512, + "dense_x": 0.2011 + }, + "19": { + "v_per_T": 119.5, + "cap": 513, + "dense_x": 0.159 + }, + "20": { + "v_per_T": 170.27, + "cap": 1024, + "dense_x": 0.1175 + }, + "21": { + "v_per_T": null, + "cap": 1025 + } + } +} diff --git a/research/window-break-even-4470/SOURCES.json b/research/window-break-even-4470/SOURCES.json new file mode 100644 index 0000000000..7d8e8a2af0 --- /dev/null +++ b/research/window-break-even-4470/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/char2-threshold/README.md", + "usage": "provenance", + "git_blob": "33f55f270d2676aaabd094176e2b52cde7c5c5de", + "sha256": "65e4b34276b5b6c31f105d4c36fa5a8a5f530f4a8bc1f41711f2e73dee1f8ea1" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/line-system-saturation/README.md", + "usage": "provenance", + "git_blob": "8e998ee15db765ce90d52d53d4a61f3fd75e5dae", + "sha256": "a99a58bc58e42348596534ce8f73809255ac89b330589b0f4d9cf2199d669e87" + } + ] +} diff --git a/research/window-break-even-4470/TASK.json b/research/window-break-even-4470/TASK.json new file mode 100644 index 0000000000..7c5045a87b --- /dev/null +++ b/research/window-break-even-4470/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "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" + ], + "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." + ], + "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.", + "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." + }, + "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.", + "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.", + "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." + ], + "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." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "Optimistic screen of changed line systems (label window h, rank T, lines v, decoder cost D) under the #4470 joint-helper-lattice invoice with its local word scaled to the new port count and fresh block, and comparison of the resulting break-even lines per dimension with the proven Theorem B cap of research/line-system-saturation.", + "scope_change_reason": "Earlier line-system screens (line-system-saturation x*(h), discussion #3622) used the pre-#4359 break-even fit; under productive helpers the saving is C ~ S/G with fresh-axis work in G, so a shorter window h looked like a large lever (optimistic x1.36..x3.47 for fresh block 7..4 at a fixed lines-per-port ratio). This package checks that lever against the line-count cap.", + "bottleneck_link": "Side result: no new kappa. Tells a new-helper-inventory search which label windows can still pay under the selected accounting.", + "budget_minutes": 60, + "stop_rule": "Stop after the named systems, the Theorem B cap rows h = 3..9 (k = T, 2T, 3T) and the break-even curve h = 3..21; no native word synthesis.", + "outcome": "completed", + "evidence": "verify.py rebuilds the #4470 targets and paid histograms exactly from RESULT.json local data, checks the root, checks the surplus identity S = (p+2)(v-D) - V exactly on 16 instances, optimises p and a for 14 named systems, the cap rows and the break-even curve, and replays RESULT.json; test_verify.py has 8 positive and rejecting controls.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Does a saturated even-window system exist at h = 6 (v = 8T, 1 in col of the adjacency) or h = 8 (v = 16T)?", + "why_it_matters": "These are the only short windows whose Theorem B cap clears the record in this model: h = 6 needs two deleted frames (x1.17 at the cap), h = 8 needs 12.4 lines per dimension against a cap of 16 (x1.46 at the cap).", + "first_step": "Extend the realisability numerics of line-system-saturation section 10 to the even-window case with k' = 3 and 4.", + "blocked_by": "none; existence of a native word with free central shears on such a unit is a separate, larger obligation" + }, + { + "question": "Is the centre floor D - k (one rank unit saved per deleted line) attainable beyond one deleted frame?", + "why_it_matters": "The h = 6 and h = 7 verdicts flip between one and two or three deleted frames; for E8 only P112 and P111 are built and P104 (k = 2T) is still open.", + "first_step": "State the deletion rule for E7 analogous to the E8 PR968 floor and test it on the 63-line unit.", + "blocked_by": "none" + } + ] +} diff --git a/research/window-break-even-4470/VERIFY.json b/research/window-break-even-4470/VERIFY.json new file mode 100644 index 0000000000..d2a3eb1bec --- /dev/null +++ b/research/window-break-even-4470/VERIFY.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-helper-lattice/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exact rebuild of the #4470 invoice and its root; exact surplus identity; p/a optimisation for 14 named line systems, Theorem B cap rows h = 3..9 with k = T, 2T, 3T and the break-even curve h = 3..21; receipt replay of RESULT.json (about 3 minutes on one core)." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Rejecting controls (changed helper count, dropped centre, wrong pair count) and positive controls (tie unit has no saving, monotone in lines per dimension, Theorem B caps, root close to S/G)." + } + ] +} diff --git a/research/window-break-even-4470/test_verify.py b/research/window-break-even-4470/test_verify.py new file mode 100644 index 0000000000..226cbd1963 --- /dev/null +++ b/research/window-break-even-4470/test_verify.py @@ -0,0 +1,63 @@ +#!/usr/bin/env python3 +"""Rejecting and positive controls for verify.py (fast subset).""" +import sys +import unittest +from collections import Counter +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as v # noqa: E402 + +S = v.bind() + + +def exact(src, **kw): + args = dict(V=112, d=8, cjobs=src['centre_jobs'], crank=8, p=src['pairs'], a=src['prefix']) + args.update(kw) + return v.invoice(src, args['V'], args['d'], args['cjobs'], args['crank'], args['p'], args['a'], exact=True) + + +def as_int(c): + return {r: int(m) for r, m in c.items() if m} + + +class Controls(unittest.TestCase): + def test_reproduces_4470(self): + T, P = exact(S) + self.assertEqual(as_int(T), S['targets']) + self.assertEqual(as_int(P), S['paid']) + + def test_changed_helper_count_rejected(self): + bad = dict(S); bad['H'] = dict(S['H']); bad['H'][9] += 1 + self.assertNotEqual(as_int(exact(bad)[0]), S['targets']) + + def test_dropped_centre_rejected(self): + self.assertNotEqual(as_int(exact(S, cjobs=0)[1]), S['paid']) + + def test_wrong_pair_count_rejected(self): + self.assertNotEqual(as_int(exact(S, p=S['pairs'] + 1)[0]), S['targets']) + + def test_no_surplus_no_saving(self): + # D6-like tie unit (v = D = 30, T = 6, k = 6): S = -V < 0 for every controller + for p in (4, 16, 30): + self.assertEqual(v.root(*v.invoice(S, 24, 4, 6, 24 / 6, p, p // 2)), 0.0) + + def test_saving_increases_with_lines_per_dimension(self): + a = v.root(*v.invoice(S, 9 * 8 - 8, 6, 8, (56 - 8) / 8, 20, 9)) + b = v.root(*v.invoice(S, 11 * 8 - 8, 6, 8, (56 - 8) / 8, 20, 9)) + self.assertLess(a, b) + + def test_theorem_b_caps(self): + self.assertEqual([v.cap(h) for h in range(3, 10)], [3, 4, 5, 8, 9, 16, 17]) + + def test_root_matches_linearisation(self): + T, P = v.invoice(S, 112, 8, 8, 8, 16, 7) + surplus = sum(r * m for r, m in T.items()) - sum(r * m for r, m in P.items()) + G = sum(m * r * __import__('math').log(r) for r, m in T.items()) - \ + sum(m * r * __import__('math').log(r) for r, m in P.items()) + self.assertAlmostEqual(surplus, 752, places=6) + self.assertLess(abs(v.root(T, P) - surplus / G), 3e-5) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/window-break-even-4470/verify.py b/research/window-break-even-4470/verify.py new file mode 100644 index 0000000000..43ac6071d7 --- /dev/null +++ b/research/window-break-even-4470/verify.py @@ -0,0 +1,180 @@ +#!/usr/bin/env python3 +"""Break-even line counts per dimension for short label windows under the #4470 invoice. + +Standard library only. Rebuilds the joint-helper-lattice (#4470) complex invoice from its +local data, generalises it to a line system (v lines, rank T, window h, decoder cost D, +k deleted lines), and compares the lines-per-dimension needed to tie the record with the +Theorem B cap of research/line-system-saturation (v/T <= 2^k'+1 at odd window h = 2k'+1, +v/T <= 2^k' at even window h = 2k'). Writes and replays RESULT.json. +""" +import json +import math +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SRC = ROOT / 'research/joint-helper-lattice/RESULT.json' +BASE_PORTS, BASE_D = 112, 8 + + +def bind(): + d = json.loads(SRC.read_text(encoding='utf-8')) + H = {int(r): n for r, n in d['local_helpers'].items()} + LP = {int(r): n for r, n in d['local_paid'].items()} + centre = LP.pop(BASE_D) + return dict(H=H, LP=LP, centre_jobs=centre, calls=d['full_calls'], pairs=d['pairs'], + prefix=d['prefix_pairs'], shears=d['query_shears'], + targets={int(r): n for r, n in d['targets'].items()}, + paid={int(r): n for r, n in d['paid'].items()}, + kappa=Q(d['kappa_decimal'])) + + +def invoice(S, V, d, cjobs, crank, p, a, exact=False): + """#4440 controller with p pairs (prefix a), local word scaled by V/112 (counts), d/8 (ranks).""" + num = Q if exact else float + n, s = num(V) / BASE_PORTS, num(d) / BASE_D + T, P = Counter(), Counter() + T[1 + d * (p + 2)] += 2 * V + for j in list(range(1, a + 1)) + list(range(1, p - a)): + T[1 + d * (j + 1)] += 2 * V + P[d * (j + 1)] += 2 * V + for r, m in S['H'].items(): + T[r * s] += (p + 2) * m * n + for r, m in S['LP'].items(): + P[r * s] += (p + 2) * m * n + P[crank] += (p + 2) * cjobs + P[1] += V * (p - 1) + return T, P + + +def root(T, P): + """Positive root of sum_T r^(1-c) - sum_P r^(1-c); 0 if the surplus is not positive.""" + TT = [(math.log(r), m * r) for r, m in T.items() if m] + PP = [(math.log(r), m * r) for r, m in P.items() if m] + + def f(c): + return (sum(w * math.exp(-c * L) for L, w in TT) - sum(w * math.exp(-c * L) for L, w in PP), + -sum(w * L * math.exp(-c * L) for L, w in TT) + sum(w * L * math.exp(-c * L) for L, w in PP)) + lo, hi = 0.0, 0.5 + if f(1e-13)[0] <= 0: + return 0.0 + c = 0.003 + for _ in range(60): + v, dv = f(c) + if v > 0: + lo = c + else: + hi = c + nc = c - v / dv if dv < 0 else (lo + hi) / 2 + if not lo < nc < hi: + nc = (lo + hi) / 2 + if abs(nc - c) < 1e-16: + break + c = nc + return c + + +def best(S, v, T, h, D, k): + V, d, c = v - k, h - 1, D - k + out = (0.0, None, None) + for p in range(3, 41): + for a in range(1, p - 1): + C = root(*invoice(S, V, d, T, c / T, p, a)) + if C > out[0]: + out = (C, p, a) + return out + + +def cap(h): + kp = h // 2 + return 2 ** kp + 1 if h % 2 else 2 ** kp + + +SYSTEMS = [ # name, v, T, h, D, deleted lines k, source of (v, T, h, D) + ('E8 P112 (selected #4470)', 120, 8, 9, 72, 8, 'char2-threshold G1.E8-gain; line-system-saturation c1'), + ('E8 P111', 120, 8, 9, 72, 9, 'centre 63 (selected bit P111 analogue)'), + ('E8 P104', 120, 8, 9, 72, 16, 'centre 56; complex P104 not built'), + ('E7 roots', 63, 7, 7, 49, 7, 'char2-threshold G1.E7-gain'), + ('E7 roots, two frames deleted', 63, 7, 7, 49, 14, 'same, k = 2T'), + ('E6 roots', 36, 6, 7, 36, 6, 'char2-threshold G1.E6-tie'), + ('D6 roots', 30, 6, 5, 30, 6, 'char2-threshold G1.D-ties'), + ('D5 roots', 20, 5, 5, 20, 5, 'char2-threshold G1.D-ties'), + ('D4 roots', 12, 4, 3, 12, 4, 'char2-threshold G1.D-ties'), + ('Z8 (56 lines)', 56, 8, 7, 56, 8, 'line-system-saturation 8.1, dense'), + ('E8+A3 (norms 6)', 140, 11, 11, 121, 11, 'line-system-saturation 8.1, dense'), + ('D16+ roots + 256 spinors', 496, 16, 17, 272, 16, 'line-system-saturation 8.1, dense'), + ('D16+ Delsarte cap 557', 557, 16, 17, 272, 16, 'line-system-saturation 8.2 upper bound'), + ('D24+ roots + 176 spinors', 728, 24, 25, 600, 24, 'line-system-saturation 8.1, dense'), +] + + +def compute(S): + rec = float(S['kappa']) + out = {'record_rounded': str(S['kappa'])} + # 1. exact reconstruction of #4470 + T0, P0 = invoice(S, BASE_PORTS, BASE_D, S['centre_jobs'], BASE_D, S['pairs'], S['prefix'], exact=True) + assert {r: int(m) for r, m in T0.items() if m} == S['targets'], 'targets not reproduced' + assert {r: int(m) for r, m in P0.items() if m} == S['paid'], 'paid not reproduced' + c0 = root(*invoice(S, BASE_PORTS, BASE_D, S['centre_jobs'], BASE_D, S['pairs'], S['prefix'])) + assert S['kappa'] < Q(c0) < S['kappa'] + Q(1, 10**7), c0 + out['calibration_root'] = round(c0, 12) + # 2. surplus identity S = (p+2)(v-D) - V on exact counts + for (v, T, h, D, k) in [(120, 8, 9, 72, 8), (63, 7, 7, 49, 7), (63, 7, 7, 49, 14), (40, 4, 6, 24, 8)]: + for p in (3, 9, 16, 30): + Tp, Pp = invoice(S, v - k, h - 1, T, Q(D - k, T), p, p // 2, exact=True) + surplus = sum(r * m for r, m in Tp.items()) - sum(r * m for r, m in Pp.items()) + assert surplus == (p + 2) * (v - D) - (v - k), (v, T, h, D, k, p) + out['surplus_identity'] = 'S = (p+2)(v-D) - V, checked exactly on 16 instances' + # 3. named systems + rows = {} + for name, v, T, h, D, k, src in SYSTEMS: + C, p, a = best(S, v, T, h, D, k) + rows[name] = dict(v=v, T=T, h=h, D=D, k=k, x=round(D / v, 4), C=round(C, 8), + ratio=round(C / rec, 4), p=p, a=a, source=src) + out['systems'] = rows + # 4. dense units at the Theorem B cap, k = T, 2T, 3T deleted lines (T = 8 is w.l.o.g.) + capped = {} + for h in range(3, 10): + r = cap(h) + capped[h] = {'cap_v_per_T': r, 'dense_x': round(h / r, 4)} + for m in (1, 2, 3): + if m >= r: + capped[h][f'k={m}T'] = None + continue + C = best(S, r * 8, 8, h, 8 * h, 8 * m)[0] + capped[h][f'k={m}T'] = round(C / rec, 4) + out['at_theorem_B_cap'] = capped + # 5. break-even lines per dimension for k = T + be = {} + for h in range(3, 22): + lo, hi = float(h), 200.0 + if best(S, hi * 8, 8, h, 8 * h, 8)[0] < rec: + be[h] = {'v_per_T': None, 'cap': cap(h)} + continue + for _ in range(30): + mid = (lo + hi) / 2 + lo, hi = (mid, hi) if best(S, mid * 8, 8, h, 8 * h, 8)[0] < rec else (lo, mid) + if hi - lo < 0.005: + break + be[h] = {'v_per_T': round(hi, 2), 'cap': cap(h), 'dense_x': round(h / hi, 4)} + out['break_even_k_eq_T'] = be + return out + + +def main(): + S = bind() + got = compute(S) + path = HERE / 'RESULT.json' + if '--write' in sys.argv: + path.write_text(json.dumps(got, indent=1) + '\n', encoding='utf-8', newline='\n') + print('wrote', path) + want = json.loads(path.read_text(encoding='utf-8')) + assert json.loads(json.dumps(got)) == want, 'receipt mismatch' + print('PASS_WINDOW_BREAK_EVEN_4470_MODEL_SCREEN_NO_KAPPA') + + +if __name__ == '__main__': + main()