diff --git a/research/h-boundary-budget/README.md b/research/h-boundary-budget/README.md new file mode 100644 index 0000000000..654e4f6e6e --- /dev/null +++ b/research/h-boundary-budget/README.md @@ -0,0 +1,183 @@ +# The p3 H branch: exact boundary budget and three closed decoder routes + +**Negative result, no new κ.** zxv's H branch of +[PR4359](https://github.com/CrocSwap/integer-mult-bounds/pull/4359) replaces the +local response by an involution `H = I + BC` (`CB = -2I`). Its raw rank surplus +is far above the current frontier, but the noncommuting p3 controller leaves three +interval endpoints of the form `Q K Q`. Their direct correction costs 672 +rank-one requests in complex and 666 in BIT, more than the whole surplus. +[PR4431](https://github.com/CrocSwap/integer-mult-bounds/pull/4431) closed +completion-only fresh inverses. This package asks how much a corrected boundary +may cost and which decoders cannot meet that price. + +## 1. Exact budget at the selected conditional κ + +Each rank-one call has weight exactly 1 in the moment at every saving `s`, so +the largest affordable boundary bill is the certified moment of the uncorrected +profile. The profiles are the retained ones: complex +`controller_tariff.geometry(3, 43)` with kernel H, surplus 616, and BIT with +the three-row minimum completion, surplus 645 = 603 + 42. + +| Saving | complex budget | BIT budget | +|---|---:|---:| +| 0.0023 | 392 | 456 | +| **0.00302015** (#4470) | **322** | **397** | +| 0.004 | 228 | 317 | + +Saving roots for each boundary bill (certified brackets in `RESULT.json`): + +| Boundary bill | complex | BIT | +|---|---:|---:| +| free | 0.0063799 | 0.0079333 | +| one shared head conjugation (224 / 222) | **0.0040422** | 0.0051761 | +| two (448 / 444) | 0.0017248 | 0.0024471 | +| direct, three (672 / 666) | negative at s = 0 | negative at s = 0 | + +So a corrected H branch beats the frontier only if all three endpoints are +repaired for at most 322 complex requests, roughly 1.44 head conjugations. +These are raw rank screens. Outer rows, tails, compiler gates and the scalar and +movement costs of a new decoder are not included, so they are ceilings. + +## 2. Whole-bank Q events cannot fit + +One Q event on a complete bank costs 112 complex requests, so the budget admits +at most two (`224 <= 322 < 336`). PR4359's `universal_two_query_screen` already +shows that two complete-bank events give a coefficient span of at most 1 against +the required 3. Even three events would cost 336 and give a complex root near +0.0029, below the frontier. + +## 3. Port subsets cannot be skipped + +For the native H112, `rank(H - I) = 8` exactly, but all 112 rows and all 112 +columns of `H - I` are nonzero. Every interval product `K` therefore moves data +on every port, so a correction touching only part of a bank leaves a nonzero +`Q`-dependent block. + +## 4. Gather decoders through the rank-8 bottleneck cost at least the direct bill + +The low rank suggests compressing: since `Q^2 = I`, + +``` +Q K Q - K = Q M Q - M, M = K - I, +``` + +and `M` factors through 8 fields per stage. This fails for an elementary reason. +On port `p`, `Q` is one rank-one request along that port's own line `q_p`. Two +ports' requests can be merged by linearity only when their lines agree, because a +request along `q_p` and a request along `q_r` are different transforms. The +stage routes (`rho`, `Gamma_s`) fix each port's line, and the commutation +`[H_s, Q b_s] = 0` only provides the full call `Q b_s` on the compressed side. + +The data leave no room: + +| | complex | BIT | +|---|---:|---:| +| ports | 112 | 111 | +| distinct query lines | **112** | **111** | +| ports touched by `H - I` | 112 | (not computed) | + +Computing `M (Q w)` for an arbitrary input therefore needs one request on every +port that `M` reads: 112. Writing `Q (M ...)` back needs one on every port that +`M` writes: another 112. The three bad roles have independent inputs, and a +request on a sum cannot be separated afterwards. Any decoder of this kind, +meaning free scalars and routes plus rank-one requests applied to linear +combinations, costs at least `3 * 2 * 112 = 672`, which is exactly the direct +bill. The direct correction is optimal within this class. + +**Scope.** This is a lower bound for linear gather decoders at fixed H112, fixed +owners and the fixed p3 controller. It is not a theorem about every possible +algorithm. A construction that changes the local family, sends several ports' +lines to a shared line before the request, or changes the controller is outside +it. + +## 5. No controller of this family has fewer Q-conjugated roles + +The verifier enumerates the free noncommuting controller of +`bit/pr589_h_global_probe.py` for p = 1..4 and every idle keep mask. It keeps +those that diagonalize exactly with parity-preserving (Q-free) boundaries: +2, 3, 8 and 20 controllers. **Every one has exactly p roles ending as `Q K Q` +with nonempty K.** Each local call stamps its stage letter on both streams of +its pair, so the odd (Q-carrying) stream always has a nonempty word. The +p3 keep-43 controller reproduces the probe's parity `[0,1,0,1,1,0]`. + +The H surplus of `mixed_forest_search.verify` is `224p - 8(2p+1)` (616 for +p = 3). A direct repair costs 224 per bad role, so after it + +``` +224p - 8(2p+1) - 224p = -8(2p+1) < 0 for every p. +``` + +Each pair brings exactly as much rank credit as its own endpoint repair costs. +Changing p or the idle mask cannot fund the direct boundary. Section 6 shows +that shared query lines do not help either. + +## 6. Shared query lines do not escape either bound + +Sections 4 and 5 left one escape: ports that share a query line. It closes as well. + +The local call realizes the identity `I = K + BA`. The pair reads `K` act only on +pairs of ports whose F2 labels are orthogonal, and `BA` (rank `h`) is decoded +through `h` centres (compare the source construction in +`research/e8-direct-source/PROOF.md`). The verifier checks this on the native H112: +all 112 labels `q_p` are odd, and `J` has zero diagonal and vanishes on all +6,608 ordered non-orthogonal label pairs. A mutated even label is rejected. + +Since `q.q = 1`, two ports with the same label are non-orthogonal. So `K` is zero +on any class of `m` copies, and `BA` restricted to that class is `I_m`. A free +rotation `X_p +- X_p'` inside the class keeps it `I_m`. Two consequences follow. + +* `h` is at least the total multiplicity of any clique of non-orthogonal labels, + so `m` copies of E8 lines need `h >= 8m`. That is exactly the rank of `m` + independent copies of the unit. +* On a copy class, `H - I` equals `-I_m` up to the `h` completion rows. So a gather + decoder needs at least `V - h` requests on input and `V - h` on output. Exactly: + P112 needs 112 + 112, and the doubled unit (224 ports, 112 lines) needs 224 + 224, + which is 2 per port in both cases. Merging all ports into one class would need + only 8 + 8 (control), so the bound really comes from the labels. + +For any unit with `V` ports, rank `h` and `p` pairs, the H surplus is +`2Vp - h(2p+1)` and the tails cost at least `2p(V - h)`: + +``` +2Vp - h(2p+1) - 2p(V - h) = -h < 0. +``` + +The H branch is unfunded whatever the line layout, shared or not, for every +local call of the form `I = K + BA`. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/h-boundary-budget --check-only +python3.12 -B scripts/research_package.py --package research/h-boundary-budget +``` + +`verify.py` uses only the standard library and imports the pinned +`research/kappa-rebuild` modules. Those modules expect `research/kappa-next-regime` +at the repository root; on main that tree is vendored under +`research/kappa-0023-productive-jobs/dependencies/kappa-next-regime`, and the +verifier adds that path. It runs in about 3.5 minutes on Windows / CPython 3.12. +Controls: a budget one above the certified value is certified negative, a +perturbed `H - I` is rejected, a duplicated query line is detected, the +p3 keep-43 controller reproduces the probe parity, an even label is rejected, +and a single merged class gives only rank 8. + +## Open next questions + +The structured versions are in `TASK.json`. + +1. **A local call outside `I = K + BA`.** Section 6 closes shared query lines + for every unit of this form. An escape needs a local identity whose pair + reads are not tied to label orthogonality. +2. **A controller not built from Q-gauged pairs.** Section 5 closes controllers + with fewer Q-conjugated roles for p <= 4, since each pair's repair costs + exactly its credit. A different pair structure would be a new complex + supplier, not an H repair. + +## Credit + +The H construction, the endpoint obstruction, the retained profiles and +receipts are zxv's (PR4359, PR4431) together with their cited predecessors. +This package adds the budget, the root table, the native rank/support and +query-line counts, the gather argument, the controller parity census and the shared-line closure. Prepared by Matarener (Mark) with +substantial Claude Code assistance. Apache-2.0. No independent human review. diff --git a/research/h-boundary-budget/RESULT.json b/research/h-boundary-budget/RESULT.json new file mode 100644 index 0000000000..3277be0433 --- /dev/null +++ b/research/h-boundary-budget/RESULT.json @@ -0,0 +1,97 @@ +{ + "bit": { + "budget_at_record": 397, + "direct_correction": 666, + "one_shared_head": 222, + "raw_surplus": 645, + "roots": { + "0": { + "negative_at": "0.0079333535", + "positive_at": "0.0079333532" + }, + "222": { + "negative_at": "0.0051761597", + "positive_at": "0.0051761594" + }, + "444": { + "negative_at": "0.0024471107", + "positive_at": "0.0024471104" + } + } + }, + "complex": { + "budget_at_record": 322, + "direct_correction": 672, + "one_shared_head": 224, + "raw_surplus": 616, + "roots": { + "0": { + "negative_at": "0.0063799044", + "positive_at": "0.0063799042" + }, + "224": { + "negative_at": "0.0040422294", + "positive_at": "0.0040422291" + }, + "448": { + "negative_at": "0.0017248836", + "positive_at": "0.0017248833" + } + } + }, + "controller_parity": { + "1": { + "after_direct": -24, + "bad_roles": 1, + "gauge_compatible_controllers": 2, + "h_surplus": 200 + }, + "2": { + "after_direct": -40, + "bad_roles": 2, + "gauge_compatible_controllers": 3, + "h_surplus": 408 + }, + "3": { + "after_direct": -56, + "bad_roles": 3, + "gauge_compatible_controllers": 8, + "h_surplus": 616 + }, + "4": { + "after_direct": -72, + "bad_roles": 4, + "gauge_compatible_controllers": 20, + "h_surplus": 824 + } + }, + "native_H112": { + "nonzero_cols": 112, + "nonzero_rows": 112, + "ports": 112, + "rank_H_minus_I": 8 + }, + "new_kappa": false, + "query_lines": { + "bit_distinct_lines": 111, + "bit_ports": 111, + "complex_distinct_q": 112, + "complex_ports": 112 + }, + "record_kappa": "60403/20000000", + "schema": "h-boundary-budget/1", + "shared_lines": { + "net_after_tail_floor": "2Vp - h(2p+1) - 2p(V-h) = -h", + "nonorthogonal_label_pairs": 6608, + "odd_labels": true, + "tail_gather_P112": [ + 112, + 112 + ], + "tail_gather_doubled": [ + 224, + 224 + ] + }, + "status": "PASS_H_BOUNDARY_BUDGET_AND_SCOPED_DECODER_CLOSURES" +} diff --git a/research/h-boundary-budget/SOURCES.json b/research/h-boundary-budget/SOURCES.json new file mode 100644 index 0000000000..d21f2dedf6 --- /dev/null +++ b/research/h-boundary-budget/SOURCES.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "usage": "input", + "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7", + "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/native_common.py", + "usage": "input", + "git_blob": "df276cc71f954b72ac4de4f07d2172d547772ba6", + "sha256": "ca1f913d6c104d456fdbebcecfdaf9a1ea12d647d74fe009b69689b9e678f0a4" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/kappa-rebuild/architecture/controller_tariff.py", + "usage": "input", + "git_blob": "21fe4799f7d9db9f32f0e92db8ae3c1c925dcb76", + "sha256": "62d2479c41c64a58275857b884f1eb68d36ee4f755d7d393363ba8cc233251f3" + }, + { + "path": "research/kappa-rebuild/architecture/identity_mixed_certificate.py", + "usage": "input", + "git_blob": "f4b51b358eff3cc43ea200503d16e7b75f67c7bc", + "sha256": "e1795294fa4d3100352bfda787ecb1efc2468ff11cbcbaca2476eb642b8d2a0a" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_forest_search.py", + "usage": "input", + "git_blob": "9b5213bf3f164664a36f81592740801f79b3c97d", + "sha256": "2dcec76840b437c67125af5b6d3529577f8c38851c792d0ffd9fa928c473e23b" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + { + "path": "research/kappa-rebuild/bit/PR589-H-GLOBAL-PROBE.json", + "usage": "input", + "git_blob": "cbebedba1df5297a3eb98783cc1814bd3773f8a5", + "sha256": "15c1a7912a4d5ee463459ca9a5fc24ee37674eaa0c1650438ffc302c0d0cd05e" + }, + { + "path": "research/kappa-rebuild/bit/bit_native_binding.py", + "usage": "input", + "git_blob": "f4c4082d89969ea311219d9af8013082d599f6f1", + "sha256": "bf6374225f388e7531fa6475cc255bd430100ff62c38d582c41601f0739de7b7" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497" + }, + { + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "usage": "input", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e" + }, + { + "path": "research/kappa-rebuild/bit/pr589_h_global_probe.py", + "usage": "input", + "git_blob": "60bfc974da92fc5b5b15463c261a78064cd7ecd2", + "sha256": "f0b9a6ac10b99c1a204fc3d9a0d26f20c6c413c436054b076ab2d9398864d391" + }, + { + "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/kappa-rebuild/complex/rebuild_native.py", + "usage": "input", + "git_blob": "78a7b1b0e6e43a1347fb361f45c6e0eaff8dd27b", + "sha256": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5" + }, + { + "path": "research/kappa-rebuild/transfer-audit/h-branch/BIT-MINIMUM-COMPLETION-AUDIT.json", + "usage": "input", + "git_blob": "553d3a166e13530ef1350a2947ed959694a8c36e", + "sha256": "c5203c00dc7f6cc20e36113cf87998fec0a6afc4c3927950d207309938fe02ff" + } + ] +} diff --git a/research/h-boundary-budget/TASK.json b/research/h-boundary-budget/TASK.json new file mode 100644 index 0000000000..849c3fa2d9 --- /dev/null +++ b/research/h-boundary-budget/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "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": "changed", + "actual_scope": "Price the boundary debt of zxv's p3 H branch (the PR4359 H local response with its three interval endpoint corrections) against the selected conditional kappa 0.00302015, and close three decoder routes for that debt: whole-bank Q events, port-subset corrections, gather/compression decoders through the rank-8 bottleneck of H-I, and controllers with fewer Q-conjugated roles (p <= 4).", + "scope_change_reason": "The card asks for a new local cost interface; the H local response is such an interface, but this package does not construct one. It screens the existing H interface with exact moments and records why the boundary decoders available at fixed H, owners and controller cannot fund it.", + "bottleneck_link": "The H branch is the only open proposal with a raw ceiling far above the frontier (complex root 0.00638 with a free boundary, 0.00404 with one shared head correction). Its sole blocker is the three-interval boundary correction; this package states the exact budget (322 complex / 397 BIT rank-one calls at kappa 0.00302015) and shows which decoder classes cannot meet it.", + "budget_minutes": 180, + "stop_rule": "Stop after the exact budget, the root table and the three scoped closures; no new decoder, controller or H construction is attempted here.", + "outcome": "negative-result", + "evidence": "RESULT.json: raw surpluses 616/645, budgets 322/397 at 0.00302015 with budget+1 certified negative, roots for k=0/one/two shared corrections and failure of the direct correction at s=0; native H112 has rank(H-I)=8 with all 112 rows and columns nonzero and H^2=I; all 112 complex q lines and all 111 BIT port lines are distinct. README.md gives the arguments and their scope. Controller census p=1..4: 2, 3, 8, 20 gauge-compatible controllers, each with exactly p Q K Q roles; H surplus 224p-8(2p+1) leaves -8(2p+1) after the direct repair. Shared lines (section 6): H112 labels are odd and the pair reads J vanish on all 6608 non-orthogonal label pairs, so copies of a line are served as independent ports; tail gather 112+112 (P112) and 224+224 (doubled unit); net after the tail floor is -h for any unit of the form I = K + BA.", + "author": "Matarener (Mark), with Claude Code assistance", + "ai_assistance": "Substantial Claude Code assistance in analysis, code and writing; exact standard-library arithmetic; no independent human review.", + "open_questions": [ + { + "question": "Is there a local call outside the form I = K + BA, with pair reads not tied to label orthogonality, that carries an H-type involutive response?", + "why_it_matters": "README section 6 shows that within I = K + BA shared query lines are served as independent copies, so the H branch nets at most -h for any port layout.", + "first_step": "Find a small exact local identity (D4 scale) in which two ports with equal labels are read by one pair read, and check whether every output is still a full independent transform.", + "blocked_by": "It is a new supplier: native word, helpers, owners and tariff all change." + }, + { + "question": "Can a controller not built from Q-gauged pairs carry an H-type involutive response?", + "why_it_matters": "README section 5 shows that with pair controllers every endpoint repair costs at least the rank credit its pair brings (p <= 4).", + "first_step": "Write the free noncommuting controller algebra for a three-stream (non-pair) local call and count its Q-conjugated roles.", + "blocked_by": "Needs a local call that acts on three streams at once; none exists in the retained suppliers." + } + ] +} diff --git a/research/h-boundary-budget/VERIFY.json b/research/h-boundary-budget/VERIFY.json new file mode 100644 index 0000000000..a3cf367ae4 --- /dev/null +++ b/research/h-boundary-budget/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/native_common.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/certificate.json.gz", + "research/kappa-rebuild/architecture/controller_tariff.py", + "research/kappa-rebuild/architecture/identity_mixed_certificate.py", + "research/kappa-rebuild/architecture/mixed_forest_search.py", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/kappa-rebuild/bit/PR589-H-GLOBAL-PROBE.json", + "research/kappa-rebuild/bit/bit_native_binding.py", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/kappa-rebuild/bit/mixed_productive_bit.py", + "research/kappa-rebuild/bit/pr589_h_global_probe.py", + "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "research/kappa-rebuild/complex/rebuild_native.py", + "research/kappa-rebuild/transfer-audit/h-branch/BIT-MINIMUM-COMPLETION-AUDIT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Complex and BIT p3 H raw surpluses 616/645; exact budgets 322/397 at kappa 0.00302015 with budget+1 certified negative (control); saving roots for free, one and two shared corrections and failure of the direct 672/666 correction at s=0; native H112 rank(H-I)=8 with full row/column support and H^2=I, perturbed H rejected (control); 112 distinct complex query lines and 111 distinct BIT lines, duplicated line detected (control). Controller census p=1..4 (2, 3, 8, 20 gauge-compatible noncommuting controllers): each has exactly p Q K Q roles, so the direct repair leaves -8(2p+1); p3 keep43 reproduces the probe parity (control). Shared lines: H112 labels odd and J zero on all 6608 non-orthogonal label pairs (even label rejected, control); tail gather 112+112 for P112 and 224+224 for a doubled unit (one merged class gives 8+8, control); net after the tail floor is -h." + } + ] +} diff --git a/research/h-boundary-budget/verify.py b/research/h-boundary-budget/verify.py new file mode 100644 index 0000000000..ab2c8d976e --- /dev/null +++ b/research/h-boundary-budget/verify.py @@ -0,0 +1,306 @@ +#!/usr/bin/env python3 +"""Boundary budget of the p3 H branch and three scoped closures of its decoder routes. + +Checks, from pinned repository sources and with exact interval arithmetic: + +1. The complex and BIT p3 H rank surpluses (616 and 645) and the largest number + of extra rank-one calls each side can pay while its moment stays positive at the + selected conditional kappa 0.00302015 (#4470): 322 complex, 397 BIT. +2. The saving root for each boundary-correction cost: free, one shared head + conjugation (224/222), two (448/444), and the direct three (672/666). +3. rank(H - I) = 8 for the native complex H112, with all 112 rows and columns + nonzero (no port can be skipped). +4. All 112 complex port query lines q and all 111 BIT port lines are distinct + (no two ports' rank-one queries can share one call). +5. Every free noncommuting p-pair controller of the retained H probe, for p = 1..4 + and every idle keep mask, that diagonalizes with gauge-compatible boundaries + leaves exactly p roles of the form Q K Q with nonempty K. With the H surplus + 224p - 8(2p+1) of mixed_forest_search.verify, the direct bill 224p leaves + -8(2p+1) for every p. +6. Ports sharing a line: H112 pair reads live on orthogonal odd labels, so copies + are served as independent ports; tail gather 2 per port, net after it -h. + +Controls: a budget one above the certified value is rejected; a mutated q list +with a duplicate is detected; a rank-8 check on a perturbed H fails; the p3 +keep-43 controller reproduces the probe's parity [0,1,0,1,1,0]; an even +label is rejected; one merged port class needs only rank 8. +Standard library only. Prepared by Matarener with Claude Code assistance. +Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import gzip +import importlib.util +import json +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +KR = ROOT/'research/kappa-rebuild' +# kappa-rebuild imports research/kappa-next-regime; on main that tree is vendored here. +DEP = ROOT/'research/kappa-0023-productive-jobs/dependencies/kappa-next-regime' +sys.path[:0] = [str(KR/'architecture'), str(KR/'bit'), + str(DEP/'bit-compression/carrier-reuse/reference')] + +RECORD = Q('0.00302015') # selected conditional kappa, #4470 +EXPECTED = { + 'complex': dict(margin=616, budget=322, one=224, direct=672, + roots={0: '0.0063799', 224: '0.0040422', 448: '0.0017248'}), + 'bit': dict(margin=645, budget=397, one=222, direct=666, + roots={0: '0.0079333', 222: '0.0051761', 444: '0.0024471'}), +} + + +def need(ok, why): + if not ok: + raise SystemExit('FAIL: ' + why) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def bounds(signed, s, h_interval): + lo = hi = Q(0) + for r, n in signed.items(): + a, b = h_interval(r, s) + lo += n*(a if n >= 0 else b) + hi += n*(b if n >= 0 else a) + return lo, hi + + +def budget(signed, s, h_interval): + """Largest k with certified moment(s) - k > 0; each rank-one call weighs exactly 1.""" + lo, _ = bounds(signed, s, h_interval) + need(lo > 0, 'moment positive before correction') + k = lo.numerator//lo.denominator + return int(k-1 if Q(k) == lo else k) + + +def root(signed, k, h_interval, steps=26): + prof = Counter(signed) + prof[1] -= k + if bounds(prof, Q(0), h_interval)[0] <= 0: + return None + pos, neg = Q(0), Q('0.02') + need(bounds(prof, neg, h_interval)[1] < 0, 'bracket') + for _ in range(steps): + mid = (pos+neg)/2 + lo, hi = bounds(prof, mid, h_interval) + if lo > 0: + pos = mid + elif hi < 0: + neg = mid + else: + break + return pos, neg + + +def complex_profile(): + import controller_tariff as T + import mixed_forest_search as F + import mixed_target_probe as E + windows, targets, _ = T.geometry(3, 43) + case = F.verify(3, 6, T.simple_p3(), 'H', custom_windows=windows, custom_targets=targets) + return Counter(case['signed']), E.h_interval + + +def bit_profile(): + import mixed_productive_bit as B + probe = json.loads((KR/'bit/PR589-H-GLOBAL-PROBE.json').read_text()) + audit = json.loads((KR/'transfer-audit/h-branch/BIT-MINIMUM-COMPLETION-AUDIT.json').read_text()) + targets = Counter({int(r): n for r, n in probe['targets'].items()}) + nine = Counter({int(r): n for r, n in probe['raw_paid'].items()}) + three = Counter({int(r): n for r, n in audit['p3']['raw_paid'].items()}) + mass = lambda c: sum(r*n for r, n in c.items()) + need(mass(targets)-mass(nine) == 603, 'nine-row BIT surplus 603') + need(mass(nine)-mass(three) == 42 and nine-three == Counter({1: 42}), 'three-row saves 42 rank-one calls') + signed = Counter(targets) + signed.subtract(three) + return signed, B.h_interval + + +def side(name, signed, h_interval): + e = EXPECTED[name] + margin = sum(r*n for r, n in signed.items()) + need(margin == e['margin'], f'{name} raw surplus {e["margin"]}') + b = budget(signed, RECORD, h_interval) + need(b == e['budget'], f'{name} budget {e["budget"]} at {RECORD}') + over = Counter(signed) + over[1] -= b+1 + need(bounds(over, RECORD, h_interval)[1] < 0, f'{name}: budget+1 is certified negative (control)') + roots = {} + for k, prefix in e['roots'].items(): + r = root(signed, k, h_interval) + need(r is not None and f'{float(r[0]):.7f}'.startswith(prefix[:8]), f'{name} root for k={k}') + roots[str(k)] = dict(positive_at=f'{float(r[0]):.10f}', negative_at=f'{float(r[1]):.10f}') + need(root(signed, e['direct'], h_interval) is None, f'{name}: direct correction fails at s=0') + return dict(raw_surplus=int(margin), budget_at_record=b, roots=roots, + direct_correction=e['direct'], one_shared_head=e['one']) + + +def rank(rows): + rows = [list(r) for r in rows] + r = 0 + for c in range(len(rows[0])): + piv = next((i for i in range(r, len(rows)) if rows[i][c]), None) + if piv is None: + continue + rows[r], rows[piv] = rows[piv], rows[r] + for i in range(len(rows)): + if i != r and rows[i][c]: + f = rows[i][c]/rows[r][c] + rows[i] = [x-f*y for x, y in zip(rows[i], rows[r])] + r += 1 + return r + + +def native_h(): + n = load(DEP/'direct-decoder/native_common.py', 'hbb_native_common') + reb = load(KR/'complex/rebuild_native.py', 'hbb_rebuild_native') + packet, _ = n.load_sources() + geo = reb.geometry(packet) + size = len(geo['H']) + h = [[Q(row.get(j, 0)) for j in range(size)] for row in geo['H']] + m = [[h[i][j]-(i == j) for j in range(size)] for i in range(size)] + out = dict(ports=size, rank_H_minus_I=rank(m), + nonzero_rows=sum(any(r) for r in m), + nonzero_cols=sum(any(m[i][j] for i in range(size)) for j in range(size))) + need(out == dict(ports=112, rank_H_minus_I=8, nonzero_rows=112, nonzero_cols=112), + 'H112: rank(H-I)=8 with full row and column support') + hh = [[sum(h[i][k]*h[k][j] for k in range(size)) for j in range(size)] for i in range(size)] + need(all(hh[i][j] == (i == j) for i in range(size) for j in range(size)), 'H^2 = I') + bad = [row[:] for row in m] + bad[0][0] += 1 + need(rank(bad) != 8, 'perturbed H is rejected (control)') + return out + + +def distinct_lines(): + phases = json.loads((DEP/'direct-decoder/sources/DATA-PHASES.json').read_text()) + qs = [r['q'] for r in phases['recipes']] + need([r['port'] for r in phases['recipes']] == list(range(112)), 'complex recipes per port') + need(len(qs) == 112 and len(set(qs)) == 112 and all(0 < q < 512 for q in qs), + 'complex: 112 distinct nonzero 9-bit query lines') + mutated = qs[:] + mutated[1] = mutated[0] + need(len(set(mutated)) == 111, 'duplicate line detected (control)') + word = json.loads(gzip.decompress((KR/'bit/sources/pr589-regenerated/WORD.json.gz').read_bytes())) + lines = [tuple(Q(x) for x in q) for q in word['lines']] + need(len(lines) == 111 and all(sum(x*x for x in q) == 4 for q in lines), 'BIT root lines') + canonical = {max(q, tuple(-x for x in q)) for q in lines} + need(len(canonical) == 111, 'BIT: 111 distinct port lines up to sign') + return dict(complex_ports=112, complex_distinct_q=112, bit_ports=111, bit_distinct_lines=111) + + +def controller_parity(): + import pr589_h_global_probe as P + census = {} + for p in range(1, 5): + compatible, bad_counts = 0, set() + for keep in range(1 << (3*(p-1)) if p > 1 else 2): + try: + _, factor, _, _ = P.controller(p, keep) + except ValueError: # no exact noncommuting diagonalization + continue + n, left = 2*p, factor['left_rows'] + parities = [{j % 2 for j in range(n) if left[i] >> j & 1} for i in range(n)] + if any(len(x) != 1 for x in parities): + continue + parity = [x.pop() for x in parities] + words = factor['diagonal_monomials'] + bad = sum(1 for i in range(n) if parity[i] == 0 and len(words[i])) + compatible += 1 + bad_counts.add(bad) + if (p, keep) == (3, 43): + need(parity == [0, 1, 0, 1, 1, 0], 'p3 keep43 reproduces the probe parity (control)') + need(compatible > 0 and bad_counts == {p}, f'p={p}: every compatible controller has exactly p bad roles') + margin = 224*p-8*(2*p+1) + need(margin-224*p == -8*(2*p+1) < 0, 'direct bill exceeds the H surplus') + census[str(p)] = dict(gauge_compatible_controllers=compatible, bad_roles=p, + h_surplus=margin, after_direct=margin-224*p) + need([census[k]['gauge_compatible_controllers'] for k in '1234'] == [2, 3, 8, 20], + 'controller census 2, 3, 8, 20') + return census + + +def shared_lines(): + """Section 6: ports that share a query line are served as independent copies. + + The local identity is I = K + BA with the pair reads K supported on pairs of + orthogonal F2 labels. Every label is odd, so equal labels are non-orthogonal + and BA restricted to a class of copies is the identity. Checked on H112; the + gather bound for a doubled unit is then 2 requests per port, as for P112. + """ + n = load(DEP/'direct-decoder/native_common.py', 'hbb_native_common') + reb = load(KR/'complex/rebuild_native.py', 'hbb_rebuild_native') + packet, _ = n.load_sources() + geo = reb.geometry(packet) + phases = json.loads((DEP/'direct-decoder/sources/DATA-PHASES.json').read_text()) + qs = [r['q'] for r in phases['recipes']] + odd = lambda x: bin(x).count('1') & 1 + J = geo['J'] + + def rule(labels): + return (all(odd(q) for q in labels) and + all(J[t].get(t, 0) == 0 for t in range(112)) and + not any(v and s != t and odd(labels[t] & labels[s]) for t in range(112) for s, v in J[t].items())) + need(rule(qs), 'H112: odd labels, pair reads K = J only on orthogonal label pairs, zero diagonal') + nonorth = sum(1 for t in range(112) for s in range(112) if s != t and odd(qs[t] & qs[s])) + need(nonorth == 6608, '6608 ordered non-orthogonal label pairs') + bad = qs[:] + bad[0] ^= 1 + need(not rule(bad), 'an even label is rejected (control)') + m = [[Q(geo['H'][i].get(j, 0))-(i == j) for j in range(112)] for i in range(112)] + + def gather(mat, classes): + cols = sum(rank([[mat[i][j] for j in c] for i in range(len(mat))]) for c in classes) + rows = sum(rank([mat[i] for i in c]) for c in classes) + return cols, rows + single = gather(m, [[p] for p in range(112)]) + doubled = [[Q(0)]*224 for _ in range(224)] + for i in range(112): + for j in range(112): + doubled[i][j] = doubled[112+i][112+j] = m[i][j] + double = gather(doubled, [[p, 112+p] for p in range(112)]) + need(single == (112, 112) and double == (224, 224), 'tail gather: P112 112+112, doubled unit 224+224') + merged = gather(m, [list(range(112))]) + need(merged == (8, 8), 'merging all ports into one class would need only rank 8 (control)') + balance = {} + for p in range(1, 5): + for v, h in ((112, 8), (224, 16)): + net = 2*v*p-h*(2*p+1)-2*p*(v-h) + need(net == -h < 0, 'H branch net after the tail floor is -h') + balance[str(p)] = -8 + return dict(odd_labels=True, nonorthogonal_label_pairs=nonorth, + tail_gather_P112=list(single), tail_gather_doubled=list(double), + net_after_tail_floor='2Vp - h(2p+1) - 2p(V-h) = -h') + + +def main(): + result = dict(schema='h-boundary-budget/1', record_kappa=str(RECORD)) + signed, h = complex_profile() + result['complex'] = side('complex', signed, h) + signed, h = bit_profile() + result['bit'] = side('bit', signed, h) + result['native_H112'] = native_h() + result['query_lines'] = distinct_lines() + result['controller_parity'] = controller_parity() + result['shared_lines'] = shared_lines() + result['status'] = 'PASS_H_BOUNDARY_BUDGET_AND_SCOPED_DECODER_CLOSURES' + result['new_kappa'] = False + if len(sys.argv) > 2 and sys.argv[1] == '--out': + Path(sys.argv[2]).write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + print(json.dumps(dict(status=result['status'], + budgets=dict(complex=result['complex']['budget_at_record'], + bit=result['bit']['budget_at_record'])), sort_keys=True)) + + +if __name__ == '__main__': + main()