diff --git a/research/p104-surplus-hub-form-note/LICENSE b/research/p104-surplus-hub-form-note/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p104-surplus-hub-form-note/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/p104-surplus-hub-form-note/NOTICE b/research/p104-surplus-hub-form-note/NOTICE new file mode 100644 index 0000000000..b621b4223a --- /dev/null +++ b/research/p104-surplus-hub-form-note/NOTICE @@ -0,0 +1,4 @@ +Surplus bound, hub rank law and form-capacity lemma for the P104 word: statements, proofs and checks (no new kappa). +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. Apache-2.0. + +check.py reads the repository files named in data/quotes.json (read-only) and files inside this package. The Theorem 5 cells use numpy. diff --git a/research/p104-surplus-hub-form-note/README.md b/research/p104-surplus-hub-form-note/README.md new file mode 100644 index 0000000000..79dfd4750e --- /dev/null +++ b/research/p104-surplus-hub-form-note/README.md @@ -0,0 +1,34 @@ +# Surplus bound, hub rank law and form-capacity lemma for the P104 word (no kappa) + +**No new kappa.** No word is built and nothing is priced beyond stated arithmetic. This package states, with an explicit hypothesis ledger, three conditional structural results about the P104 caller and the checks that back them. Statements and proofs are in `THEOREM.md`. + +Tag discipline (as in `THEOREM.md`): **[C]** exact computation reproduced by `check.py` (one PASS line per claim); **[P]** hand proof; **[P+C]** both; **CONDITIONAL** stated but not proved, or not checkable here. A verifier or package restriction is never called a law: the labels are SPEC (outer framework or paper), package convention, verifier behaviour, derived, family assumption. + +## Results + +1. **Surplus identity [C].** At the selected record (13,444 productive fields, 66,834 paid calls) the rank-mass surplus is `S = 760 = v(L-1) - Lc = 104*17 - 18*56`, recomputed from the stored profile. The pricer's own assertion at `research/p104-helper470-twin-rung-removal/pricing.py:75` is quoted and its line is checked. +2. **Ratio lemma [P+C].** For any word made of invertible Q-independent maps and `N` isotropic rank-one units, `N >= 1 + dim ker(R+I)` with `R = P(-1)P(1)^-1`. The identities in the proof hold exactly over Q on random isotropic instances; the chain roots attain the bound. CONDITIONAL on exactness at `Q = +-1`, isotropic rank-one units, and credited fields equal to `ker(R+I)`. +3. **Surplus bound, Theorem 2 [P, sweeps C], CONDITIONAL on H1-H6.** `S <= sum_p (L_p - 1) - sum_j c_j`, which is `v(L-1) - Lc` for uniform ports; the target size cancels. H1 and H4 are hand arguments (H4's "mains pay exactly the stage rank" step is not re-audited), H5 (one hosted Q-odd unit per LOCAL) is a family assumption, and with two the same arithmetic would allow 2632. The bound concerns the numerator only. +4. **Typed query, Proposition 3 [C, P], scoped.** A rank-one Q-odd unit realised by a Clifford operator has Bruhat rank one and lies in a single `F H F` cell; the plane kernel `K_P` is a rank-two job in the cell of `C (x) C`. The cost-model reading (a thin query costs one rank-one paid call per port) is CONDITIONAL; the non-unitary shear factorisation lies outside the lemma and whether a shear-typed supplier can be priced below a leaf is open. The check runs in exact Gaussian-rational arithmetic with the standard library only. +5. **Hub rank law, Theorem 4 [P+C], CONDITIONAL on the coordinate-mask grammar.** rank `Z(D) = v`, the cocycle relation, divisibility `Z_fl(D) = Z_fl(1) prod D_k^-1`, and at least `v` coordinates in every LOCAL mask, at every nonzero `D`. The checked instances are gauge-equivalent to a direct sum and cannot exhibit a non-gauge coupling; the proof, not the replays, carries the claim. +6. **Form-capacity lemma, Theorem 5 [P, tested by C], scoped.** In the stated one-pass stop family, if `Y' = c x`, `T[Y,K] = 0` and `X', K'` span `(y - a x, k)`, then `ku >= v` for every `kd` and `a`. The numerical cells (v = 3, eight cells; v = 2, four cells) are generic-solution evidence for the invariant, and unsolved cells are not evidence; a control family with down rows landing at a line exceeds the bound, as the scope says. +7. **Label corrections and retained arithmetic [C].** The identical-representative requirement is a package convention, not SPEC; symbolic exactness in `D` and ascend-only public paths are verifier behaviour. For words multi-affine in `D`, vanishing on `{+1,-1}^k` is equivalent to vanishing as a polynomial (evaluation matrix rank `2^k`, `k = 2, 3, 4`). Invoice-total arithmetic uses typed-in constants, not a recomputation from a word; the two partial sums differ by 4 from the quoted total (226,935 versus 226,939) from rounding. + +## Scope and what is not claimed + +No bound on kappa; no statement about the denominator; nothing about non-diagonal Gram structure; Lemma 1 and Theorem 2 do not cover in-place units, words with leak, or words exact only in a limit; Theorem 4 and Theorem 5 are as scoped above. No word from any pull request is replayed or checked here. + +## Exact checks + +`python3.12 -I -B research/p104-surplus-hub-form-note/check.py` from the repository root (or `verify.sh` from anywhere). About 20 s. Exact parts use the standard library only (`fractions`). The Theorem 5 numerical cells need numpy, pinned in `VERIFY.json` (`numpy==2.4.2`). The quote checks read six repository files named in `data/quotes.json` (19 lines) and fail if a file is absent or a line changed; the same files are pinned in `SOURCES.json`. The run ends with `PASS_P104_SURPLUS_HUB_FORM_NOTE`. + +## Open next questions + +1. Can a LOCAL host two Q-odd units per port (H5), and does any word then reach the 2632 value the same arithmetic allows? +2. Can a shear-typed supplier realise the thin queries below one rank-one paid call per port (H6)? +3. Does the hub rank law survive outside coordinate masks with one scalar per LOCAL, and is a half-width hub possible there? +4. Does the form-capacity bound extend to down-row landings at a line after X reached V, and to targets with `T[Y,Y] != 0`? + +The structured form with first steps and blockers is in `TASK.json`. + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code. diff --git a/research/p104-surplus-hub-form-note/SOURCES.json b/research/p104-surplus-hub-form-note/SOURCES.json new file mode 100644 index 0000000000..cf3e95e499 --- /dev/null +++ b/research/p104-surplus-hub-form-note/SOURCES.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper470-twin-rung-removal/pricing.py", + "usage": "input", + "git_blob": "65bb723f8558dc60ff92764db1a43d8bf438aa09", + "sha256": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710" + }, + { + "path": "research/p104-productive-controller/PROOF.md", + "usage": "input", + "git_blob": "e0bb34fbef6b412b572818d669150b54a13ea30d", + "sha256": "f4c4e400092954562252df6c4dd157a9b4c1642252168ce72738cdbecfc5ad41" + }, + { + "path": "research/p104-productive-controller/local.py", + "usage": "input", + "git_blob": "dbb3d56a4f5b733bb0c32a91249d1f6a7e1ab5d2", + "sha256": "878734dfd64c4b9d362d0ae476cc5c2a19fe93e48b7378763b23f3e0dd0a5a71" + }, + { + "path": "notes/general-clifford-frames.tex", + "usage": "input", + "git_blob": "0367eeb005298601f28a673861d6f71bf1d0ebbb", + "sha256": "c9bb9655b594583c6b4bab8cb485233f1d1e588f83858cf1e4c3530cee8fed54" + }, + { + "path": "research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md", + "usage": "input", + "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca", + "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8" + }, + { + "path": "upstream/build/sections/05-layers.tex", + "usage": "input", + "git_blob": "5ce8b3c83c455f221bb84858a97230b0285644aa", + "sha256": "20cfc8d12099d4e4ed9e3e7eeb6162edd9b6e0e076f24693364cd24377252594" + } + ], + "source_availability": "Every listed file is a blob of the base commit. The quote checks in check.py read the six files with usage \"input\" from the repository root and compare the quoted line numbers and text; all other inputs are inside this package." +} diff --git a/research/p104-surplus-hub-form-note/TASK.json b/research/p104-surplus-hub-form-note/TASK.json new file mode 100644 index 0000000000..d4f743e362 --- /dev/null +++ b/research/p104-surplus-hub-form-note/TASK.json @@ -0,0 +1,143 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Proof note on the selected P104 record under a stated hypothesis ledger (H1-H6): the rank-mass surplus S = 760 = v(L-1) - Lc and a conditional upper bound S <= sum_p (L_p - 1) - sum_j c_j; the ratio lemma N >= 1 + dim ker(R+I) for words of isotropic rank-one units; a hub rank law (Theorem 4) in the coordinate-mask grammar; a form-capacity lemma (Theorem 5, ku >= v) for the stated one-pass stop family, with a numerical cross-check on small cells; a scoped typed-query proposition (a rank-one Q-odd unit has Bruhat rank one); and label corrections (package convention versus SPEC versus verifier behaviour). Arithmetic on stated invoice totals is retained and labelled as typed-in constants. No word is built and no kappa is claimed.", + "scope_change_reason": "The card asks for a joint helper basis and a legal causal split on the complete invoice. This package builds no word and prices no supplier; it states conditional structural bounds on the surplus numerator, a hub rank law and a capacity lemma for one stop family, each with its hypotheses, and keeps every open door at a named hypothesis.", + "bottleneck_link": "docs/research/research-family-status.md; the statements bound the surplus numerator S and constrain the hub and helper-form structure of any word in the stated grammar. They say nothing about the denominator or about kappa.", + "stop_rule": "No kappa claim and no new word. Open and stated: two hosted Q-odd units per LOCAL (H5); a cheaper realisation of thin queries (H6) and whether a shear-typed supplier can be priced below a rank-one leaf; c below 56 outside the Gram class; words with leak, in-place units, or exactness only in a limit; hub grammars other than coordinate masks with one scalar per LOCAL; Theorem 5 outside the stated stop shape (down-row landings at a line after X reached V, T[Y,Y] != 0, non-diagonal port Gram, rank-one crossings at mid frames).", + "evidence": "README.md and THEOREM.md (statements, proofs, hypothesis ledger), check.py with checks/ (exact certificates over the rationals and one numpy-based numerical cross-check for Theorem 5) and data/ (selected-record profile, quoted-line table).", + "author": "DreamingOfClouds", + "ai_assistance": "Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code.", + "outcome": "completed", + "open_questions": [ + { + "question": "Can a LOCAL host two Q-odd units per port (H5), and if so does any word reach the 2632 value that the same arithmetic allows?", + "why_it_matters": "H5 is a family assumption, not a consequence of rank conservation; Theorem 2 depends on it, and with two hosted units per LOCAL the surplus arithmetic would allow 2632.", + "first_step": "State the verifier conditions under which one LOCAL can contain two independent Q-odd units of one port path, then test whether rank conservation forbids it.", + "blocked_by": "No proof or counterexample either way; the hosted-unit count is only a family assumption." + }, + { + "question": "Can a shear-typed supplier realise the thin queries below one rank-one paid call per port (H6, shear exponent)?", + "why_it_matters": "The bound S <= v(L-1) - Lc prices an unhosted Q-odd unit at one uncredited rank-one query; a cheaper accounting would raise the numerator bound.", + "first_step": "Decide whether the non-unitary shear factorisation C = U(i) W U(i), which lies outside the Clifford rank lemma, has a priced realisation below a leaf in the finite compiler's cost model.", + "blocked_by": "The pricer and the finite compiler's base case both charge a rank-one leaf; no cited text excludes or supplies a cheaper accounting." + }, + { + "question": "Does the hub rank law (Theorem 4) survive outside the coordinate-mask grammar, and is a half-width hub possible there?", + "why_it_matters": "The replays are gauge-equivalent to direct sums and cannot exhibit a non-gauge coupling; the proof carries the claim only inside the grammar.", + "first_step": "Find the weakest grammar change (non-coordinate masks, or two scalars per LOCAL) under which the Schur-complement and divisibility steps fail, then test a v = 2 instance.", + "blocked_by": "No exact decision tool outside coordinate masks." + }, + { + "question": "Does the form-capacity bound ku >= v extend to landings of down rows after X has reached V, and to targets with T[Y,Y] != 0?", + "why_it_matters": "A control family with such landings exceeds the bound, so the lemma is exactly as wide as the stated stop shape.", + "first_step": "Find the invariant that replaces the pi-rank count when a down row lands at a line, and check it on the control family.", + "blocked_by": "The numerical cells are generic-solution evidence only; unsolved cells are not evidence." + } + ], + "research_context": { + "sources": [ + "research/p104-helper470-twin-rung-removal/pricing.py (selected-record pricer)", + "research/p104-productive-controller/PROOF.md and local.py (public path and frame rules)", + "notes/general-clifford-frames.tex (Fourier rank d(U,W))", + "upstream/build/sections/05-layers.tex and research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md (rank-one leaf)" + ], + "credit": "DreamingOfClouds." + }, + "selected_frontier_changed": false +} \ No newline at end of file diff --git a/research/p104-surplus-hub-form-note/THEOREM.md b/research/p104-surplus-hub-form-note/THEOREM.md new file mode 100644 index 0000000000..cd368a9694 --- /dev/null +++ b/research/p104-surplus-hub-form-note/THEOREM.md @@ -0,0 +1,77 @@ +# Proof note: a surplus bound, a hub rank law, and a form-capacity lemma for the P104 word + +Every claim below carries one of: **[C]** exact computation reproduced by `check.py` (a PASS line per claim), **[P]** hand proof, re-derived and confirmed independently, **[P+C]** both, **CONDITIONAL** (stated, not proved or not checkable here). No kappa claim and no new word are made. Labels follow one rule: a verifier or package restriction is never called a law. + +Label vocabulary: **SPEC** = a premise of the outer framework or a statement in the paper; **package convention** = a choice of the existing construction that another legal object could replace; **verifier behaviour** = what the shipped checkers enforce; **derived** = follows from the others; **family assumption** = a hypothesis of this note only. + +## 1. Setting and notation + +A LOCAL call acts on v ports (v = 104). Each port path contains L native moves (L = 18) and each LOCAL owns mass c (c = 56). A "Q-odd unit" is a unit that separates the two real characters Q = +1 and Q = -1 of the shear variable. S denotes the rank-mass surplus: the sum of rank times count over productive targets minus the same sum over paid calls. At the selected record (conditional kappa 0.003125804, 13,444 productive fields, 66,834 paid calls) S = 760 [C: the surplus is recomputed from the record's profile; the shipped pricer asserts the same value at `research/p104-helper470-twin-rung-removal/pricing.py:75`], and 760 = v(L-1) - Lc = 104*17 - 18*56 [C]. + +## 2. Ratio lemma + +**Lemma 1 [P+C].** Let a word be any product, in any order, of arbitrary invertible Q-independent maps G_j and N rank-one units I + Q x_k y_k^T with y_k^T x_k = 0 (isotropic). Let P(Q) be its matrix, R = P(-1) P(1)^-1, and let n be the dimension. Then N >= 1 + dim ker(R + I). + +*Proof.* (1) Moving every G_j to the left turns each unit into I + Q x'_k y'^T_k with x' = G^-1 x, y'^T = y^T G, still isotropic. So P(Q) = G A(Q), A(Q) = prod_k (I + Q x_k y_k^T). (2) With X = [x_k], Y = [y_k] and L the strictly triangular part of Y^T X in time order, A(c) = I + c X (I - cL)^-1 Y^T. (3) Hence A(1) + A(-1) - 2I = 2 X (I-L)^-1 L (I+L)^-1 Y^T, of rank at most rank L <= N-1. (4) A(1) + A(-1) = G^-1 (I + R) P(1) has rank n - dim ker(R+I); subtracting 2I lowers rank by at most n, so rank(A(1)+A(-1)-2I) >= dim ker(R+I). Combine (3) and (4). QED. + +Checks: identity (2) and the rank bound (3) hold exactly on 48 random isotropic instances (n = 3, 4; N = 3..6; c in {1,-1,3}); the lemma holds on 90 further instances; it is attained by the chain root (n = 4, N = 5, R = -I) and by (n = 6, N = 7) [C]. + +Hypotheses of the lemma: exactness at both real characters (verifier behaviour: the package replay keeps Q as a formal invertible variable, `research/p104-productive-controller/PROOF.md:119`, so specialisation to Q = +-1 is valid); isotropic rank-one units (package convention: units write a register other than the one they read; the shipped endpoint is Y_r -> Y_r + X_r, `PROOF.md:31`, and the event alphabet fixes rank one); and that credited fields are exactly ker(R+I) (derived from whole-job credit, a framework premise, plus the no-leak family assumption below). CONDITIONAL on those. + +## 3. Surplus bound + +**Theorem 2 (S bound), conditional on H1-H6 below.** For every target size r and every Q-independent network, the per-port surplus satisfies r_p - thin_p <= L_p - 1, hence +**S <= sum_p (L_p - 1) - sum_j c_j**, which is v(L-1) - Lc for uniform ports. Equality requires r >= L-1 and thin = 1 + r - L (thin = 0 at r = L-1). Here thin = N - hosted is the number of Q-odd units that no LOCAL hosts. + +*Proof.* Lemma 1 gives N >= 1 + r. By H5 each LOCAL hosts at most one Q-odd unit per port, so hosted <= L and thin >= 1 + r - L. By H4, S per port = r - thin - Lc/v. The target size r cancels. QED [P; the sweep over r = 0..80 and the non-uniform-port form are [C]]. + +| # | hypothesis | label | +|---|---|---| +| H1 | credited fields = ker(R+I) per port | derived from whole-job credit (framework premise) and the Gaussian endpoint family; the endpoint derivation is a hand argument, CONDITIONAL | +| H2 | units isotropic and rank one | package convention | +| H3 | exact at Q = +-1 | verifier behaviour (see Section 2) | +| H4 | ledger: outer credit = stage rank + r; S/port = r - thin - Lc/v | derived from the invoice shape; the identity 884 = 576 + 288 + 20 is [C] for the record's invoice; the "mains pay exactly the stage rank" step is a hand argument not re-audited, CONDITIONAL | +| H5 | a LOCAL hosts at most one Q-odd unit per port | family assumption (not proved by rank conservation); with two hosted units per LOCAL the same arithmetic would allow 2632 [C] | +| H6 | an unhosted Q-odd unit costs one uncredited rank-one query; natives and Q-independent moves are Q-free; c >= 56 | pricing: package (`pricing.py:48-49`); Q-freeness: package convention; c >= 56: family assumption (Gram-class result), the bound is parametric in c | + +Supporting package facts used by the ledger: the price of a native boundary move equals |dim U - dim W| for nested frames (verifier, `local.py:229`) which is the Fourier rank d(U,W) = dim U + dim W - 2 dim(U cap W) of the paper (`notes/general-clifford-frames.tex:16,27`; the inequality d >= |dim U - dim W| used by the ledger is exhaustively checked on F2^4 [C]); public paths are nested and ascending (verifier, `local.py:126`); end frames are pinned (verifier, `local.py:242-243`). + +**Open doors, all at hypotheses.** Two hosted Q-odd units per LOCAL (H5); a cheaper realisation of the thin queries (H6, Section 4); c below 56 outside the Gram class; words that leave H1-H3 (scratch with leak, units that read and write one register, exactness only in a limit). The bound concerns the numerator S only; kappa depends equally on the denominator. + +## 4. Typed query + +**Proposition 3 (scoped).** A rank-one Q-odd unit realised by a Clifford operator has Bruhat rank one: C = aI + bX with b/a = -i, symplectic matrix [[1,1],[0,1]], rank_F2 B = 1, and C lies in a single H-cell F H F with C not in the free monomial group F [C]. For symplectic matrices rank B(UV) <= rank B(U) + rank B(V), and free pieces (B = 0, A and D invertible) leave rank B unchanged [P: B(M1 U M2) = A1 B_U D2], so any factorisation into free pieces and Clifford jobs has Clifford ranks summing to at least one. The plane kernel K_P is a rank-two job in the cell of C (x) C [C]; it does not lower the rank. + +**Cost-model reading, CONDITIONAL.** The pricer charges a query shear one rank-one paid call per port (`pricing.py:48-49`), and the finite compiler's base case is a rank-one leaf (`FINITE-PRECOMPILATION.md:139,169`; `05-layers.tex:431,640`). A cheaper accounting for thin queries is not excluded by any text cited here; none exists in the package. + +**Not covered.** The non-unitary shear factorisation C = U(i) W U(i) is exact [C] and lies outside the Clifford lemma. Whether a shear-typed supplier can be priced below a leaf (the shear exponent beta) is open. + +## 5. Hub rank law + +**Theorem 4 (conditional on H-grammar).** Setting: coordinate masks in one frame; units I - 2 x_k y_k^T with y_k x_k = 0 and x_k, y_k inside the mask M_k; one scalar D_k at each LOCAL site and none on thin units; the word equals -diag(prod D^eps) with eps the masks and equals -I at D = 1; characteristic not 2; the total excess N - n equals v; every LOCAL is a width-v block with y_a x_b = 0 for all a, b. Then, at every nonzero D: +(1) rank Z(D) = v; (2) Z_kl = (1/2) Z_km Z_ml for LOCAL blocks k, m, l (Z normalised with diagonal LOCAL blocks 2I); (3) for the first and last LOCAL f < l, Z_fl(D) = Z_fl(1) prod_{LOCAL k in [f,l)} D_k^-1 with Z_fl(1) invertible; (4) at least v coordinates lie in every LOCAL mask. + +*Proof sketch [P+C].* (1) Moving each scalar left, the primed word is a product of isotropic units equal to -I; writing the product as I - 2 X A^-1 Y^T with A = I + 2U unit triangular gives X A^-1 Y^T = I_n, so A^-1 Y^T X is idempotent of rank n and I + U - L has rank N - n = v (identity and rank verified exactly on the chain roots, n = 4 and 6 [C]). (2) A diagonal block 2I is invertible and rank Z = v, so the Schur complement of that block vanishes. (3) Entries of Z_{kk'} are sums of multilinear monomials in E = D^-1 and each is divisible by E_k; multiplying the chain over consecutive LOCALs gives divisibility by every E_k in [f,l) while multilinearity bounds each exponent by one. (4) Z_fl(1) is a sum over coordinates c of rank-one terms y_f[c] x_l[c], so rank v needs at least v coordinates. Exact replays at v = 1 (control) and v = 2 with port-coupling gauges, L = 2 and 4, at generic and degenerate nonzero D, all pass [C]. + +Scope: the checked instances are gauge-equivalent to a direct sum, so they cannot exhibit a non-gauge coupling; the proof, not the replays, carries the claim. The grammar (coordinate masks, unit inside its mask, one scalar per LOCAL) is what a different framework would change; a half-width hub needs one of those to fail, not a rank drop. + +## 6. Form-capacity lemma (one-pass family) + +**Theorem 5 [P, tested by C].** Family: stops in order Z (frame 0: Y, K, A, E), L_r (line r: X_r, helpers h_r*, scratch), V1 (X, A, B, scratch), Z2 (frame 0: Y, B, E), P_t (hyperplane q_t^perp: Y_t, helpers h_*t, scratch), V2 (X, K, A, scratch); helper h_rt (r != t) visits Z, L_r, P_t, V2; owned rows start at zero; kd = |B| down rows, ku = |A| up rows; any number of helpers per pair. Each stop applies a free invertible map. If Y' = c x with c != 0, T[Y,K] = 0, and X', K' span (y - a x, k) for some a, then **ku >= v**, for every kd and every a. + +*Proof.* Let pi project forms modulo span(x). (i) Before P_t the only register carrying x_t is Y_t (helper h_rt carries x-content of x_r only, r != t; scratch is zero), so Y'_t has a nonzero coefficient on Y_t. (ii) pi(Y'_t) = 0, so pi(Y_t before P_t) lies in span pi(h_*t). (iii) After L_r, pi of the helpers and of X_r lies in the span Omega_r of pi(h_r* at Z); with |K| helper registers, dim Omega <= |K|. (iv) By (ii), P_t adds nothing outside Omega; V1 adds only pi of the |A| = ku up rows, and down rows carry only these and x. (v) V2 must output pi-rank v + |K|, so v + |K| <= |K| + ku. QED. + +Check [C]: constraining only Y' = x and solving numerically with free X', K', the pi-rank of (X', K') equals |K| + ku (never above) in every solved cell tested (v = 3, kd in 0..6, ku in 0..3, and v = 2), independent of kd. This is generic-solution evidence for the invariant; the proof is the argument above. + +**Scope.** Covers the stated stop shape only: targets with T[Y,Y] = 0 and fixed toy pins with independent ports. It does not cover landings of down rows at a line after the register has reached V: a control family with that landing exceeds the bound [C]. It does not cover targets with T[Y,Y] != 0, non-diagonal port Gram matrices, rank-one crossings at mid frames, or real words that read X_r at many frames. + +## 7. Label corrections and retained arithmetic + +- The requirement that all incident registers at a scalar gate use one identical exact representative is a construction choice of the frame lemma (`notes/general-clifford-frames.tex:62`, "Choose ... use one identical exact representative"). It is sufficient for exactness, and no text I read shows it is necessary. It should be called a package convention, not SPEC. +- The requirement that the word be exact symbolically in D is verifier behaviour. For a word that is multi-affine in D, vanishing on the character grid {+1,-1}^k is equivalent to vanishing as a polynomial (evaluation matrix of full rank 2^k, k = 2, 3, 4) [C]. Replacing the symbolic replay by a character-grid replay therefore changes nothing for such words. +- Public ascend-only paths are verifier behaviour (`local.py:126`), not a law. +- Arithmetic on stated invoice totals (the inputs are hard-coded in the check, not recomputed from a word): root net of perfect mains 85,277 (37.6% of D); public stop tax 142,686 (62.9%); the hub term f(145)*v = 75,049 (33.1%); S = 864 - 104 = 760; a 14.3% cap needs a cut of 28,392 R0 in D (1,577 R0 per call). The two partial sums differ by 4 from the quoted total (226,935 versus 226,939) from rounding of the per-call taxes. + +## 8. What is not claimed + +No bound on kappa; no statement about the denominator D; no claim on non-diagonal Gram structure; Lemma 1 and Theorem 2 do not cover in-place units, words with leak, or words exact only in a limit; Theorem 5 and Theorem 4 are as scoped above; the shear exponent is open. diff --git a/research/p104-surplus-hub-form-note/VERIFY.json b/research/p104-surplus-hub-form-note/VERIFY.json new file mode 100644 index 0000000000..650ab84e2c --- /dev/null +++ b/research/p104-surplus-hub-form-note/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.4.2" + ], + "inputs": [ + "research/p104-helper470-twin-rung-removal/pricing.py", + "research/p104-productive-controller/PROOF.md", + "research/p104-productive-controller/local.py", + "notes/general-clifford-frames.tex", + "research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md", + "upstream/build/sections/05-layers.tex" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/check.py" + ], + "timeout_seconds": 300, + "checks": "19 quoted repository lines (pricer, path rules, frame notes, finite-compiler leaf); selected-record surplus 760 = 104*17 - 18*56 from the stored profile; ratio lemma identities and rank bound over Q on random isotropic instances and chain roots (tightness); hub rank law (rank, cocycle, divisibility, overlap) at generic and degenerate nonzero D with a v=1 control; surplus/seam/ledger script (F2^4 subspace inequality, S identity and sweeps); typed query over the Gaussian rationals; Theorem 5 pi-rank bound on one-pass cells by a numpy numerical solver (numpy only here) with a rowline control; retained invoice arithmetic; multi-affine evaluation-matrix ranks k = 2, 3, 4." + } + ] +} diff --git a/research/p104-surplus-hub-form-note/check.py b/research/p104-surplus-hub-form-note/check.py new file mode 100644 index 0000000000..a2849c10c6 --- /dev/null +++ b/research/p104-surplus-hub-form-note/check.py @@ -0,0 +1,164 @@ +#!/usr/bin/env python3 +"""Single driver: prints one PASS line per claim of THEOREM.md (exit 1 on any FAIL); ends with PASS_P104_SURPLUS_HUB_FORM_NOTE. +Run from anywhere: python3.12 -I -B research/p104-surplus-hub-form-note/check.py (writes nothing). +Dependencies: Python 3.12 standard library plus numpy (declared in VERIFY.json; used only by the Theorem 5 numerical cells). +The quote checks read the repository files named in data/quotes.json at the repository root (two levels above this package); +a missing file or a changed line is a FAIL, never a skip.""" +import os, sys, json, subprocess, itertools, random +from fractions import Fraction as Q +HERE = os.path.dirname(os.path.abspath(__file__)) +CH = os.path.join(HERE, 'checks') +PKG = os.path.dirname(os.path.dirname(HERE)) # repository root: HERE = /research/p104-surplus-hub-form-note +fails = [] +def PASS(tag, msg): print(f'PASS [{tag}] {msg}', flush=True) +def FAIL(tag, msg): fails.append(tag); print(f'FAIL [{tag}] {msg}', flush=True) +def ck(tag, cond, msg): (PASS if cond else FAIL)(tag, msg) +def run(script, *args, env=None): + e = dict(os.environ); e.update(env or {}) + p = subprocess.run([sys.executable, '-I', '-B', script, *args], cwd=CH, capture_output=True, text=True, env=e, timeout=600) + return p.stdout + p.stderr + +# ---- Q: quotes (relabel evidence) --------------------------------------------------------------- +quotes = json.load(open(os.path.join(HERE, 'data', 'quotes.json'))) +for grp, root in (('pkg', PKG),): + for rel, ln, sub in quotes[grp]: + path = os.path.join(root, rel) + if not os.path.isfile(path): + FAIL(f'Q-{grp}', f'{rel}:{ln} (file absent)'); continue + lines = open(path, encoding='utf-8', errors='replace').read().split('\n') + ck(f'Q-{grp}', ln <= len(lines) and sub in lines[ln-1], f'{rel}:{ln} contains {sub[:60]!r}') + +# ---- S: selected record profile -------------------------------------------------------------- +d = json.load(open(os.path.join(HERE, 'data', 'selected_record_profile.json'))) +tt = sum(int(k)*v for k, v in d['targets'].items()); pp = sum(int(k)*v for k, v in d['paid'].items()) +ck('S-record', tt - pp == 760 == d['rank_mass_surplus'], f'selected record: sum rank*targets - sum rank*paid = {tt}-{pp} = {tt-pp}') +ck('S-record', sum(d['targets'].values()) == d['productive_fields'] == 13444 and sum(d['paid'].values()) == d['paid_calls'] == 66834, 'fields 13444, paid calls 66834') +v, L, c = 104, 18, 56 +ck('S-formula', v*(L-1) - L*c == 760, 'v(L-1) - L c = 104*17 - 18*56 = 760 (equality at the selected record)') + +# ---- S: ratio lemma, independent exact re-derivation ------------------------------------------ +def rank(M): + M = [r[:] for r in M]; r = 0 + for cc in range(len(M[0]) if M else 0): + p = next((i for i in range(r, len(M)) if M[i][cc] != 0), None) + if p is None: continue + M[r], M[p] = M[p], M[r] + for i in range(len(M)): + if i != r and M[i][cc] != 0: + f = M[i][cc]/M[r][cc]; M[i] = [a-f*b for a, b in zip(M[i], M[r])] + r += 1 + return r +def mm(A, B): + Bt = list(zip(*B)); return [[sum(a*b for a, b in zip(r, cc)) for cc in Bt] for r in A] +def inv(A): + n = len(A); M = [A[i][:]+[Q(int(i == j)) for j in range(n)] for i in range(n)] + for cc in range(n): + p = next(r for r in range(cc, n) if M[r][cc] != 0); M[cc], M[p] = M[p], M[cc] + pv = M[cc][cc]; M[cc] = [x/pv for x in M[cc]] + for r in range(n): + if r != cc and M[r][cc] != 0: + f = M[r][cc]; M[r] = [a-f*b for a, b in zip(M[r], M[cc])] + return [r[n:] for r in M] +def eye(n): return [[Q(int(i == j)) for j in range(n)] for i in range(n)] +def unit(x, y, cq): + n = len(x); return [[Q(int(i == j)) + cq*x[i]*y[j] for j in range(n)] for i in range(n)] +random.seed(11) +def rand_iso(n): + while True: + x = [Q(random.randint(-3, 3)) for _ in range(n)]; y = [Q(random.randint(-3, 3)) for _ in range(n)] + if sum(a*b for a, b in zip(x, y)) == 0 and any(x) and any(y): return x, y +# step 1-3: A(c) = I + c X (I - cL)^-1 Y^T and A(1)+A(-1)-2I = 2X(I-L)^-1 L (I+L)^-1 Y^T, rank <= N-1 +okA = okB = True; trials = 0 +for n, N in ((4, 3), (4, 4), (4, 5), (3, 6)): + for _ in range(12): + us = [rand_iso(n) for _ in range(N)] + G = [[sum(us[k][1][i]*us[l][0][i] for i in range(n)) for l in range(N)] for k in range(N)] # y_k . x_l + Lm = [[G[k][l] if k < l else Q(0) for l in range(N)] for k in range(N)] # strict triangle, product order + X = [[us[k][0][i] for k in range(N)] for i in range(n)]; Yt = [[us[k][1][i] for i in range(n)] for k in range(N)] + def Aprod(cq): + P = eye(n) + for x, y in us: P = mm(P, unit(x, y, cq)) + return P + for cq in (Q(1), Q(-1), Q(3)): + IL = [[Q(int(i == j)) - cq*Lm[i][j] for j in range(N)] for i in range(N)] + R_ = mm(mm(X, inv(IL)), Yt); F = [[Q(int(i == j)) + cq*R_[i][j] for j in range(n)] for i in range(n)] + okA &= (F == Aprod(cq)) + S_ = [[Aprod(1)[i][j] + Aprod(-1)[i][j] - 2*(i == j) for j in range(n)] for i in range(n)] + okB &= rank(S_) <= N-1; trials += 1 +ck('S-ratio', okA, f'A(c) = I + cX(I-cL)^-1 Y^T exact, {trials} random isotropic instances, c in {{1,-1,3}}') +ck('S-ratio', okB, 'rank(A(1)+A(-1)-2I) <= N-1 on the same instances') +# the chain: dim ker(R+I) <= N-1 on exact root instances (R = A(-1)A(1)^-1 up to the Q-even factor) +sys.path.insert(0, CH) +from chain_root import units, T as Tf +tight = [] +for gL, gR in ((1, 1), (2, 2)): + n, Ls, Rs, th = units(gL, gR); N = len(Ls)+len(Rs)+len(th) + found = False + for pos in itertools.combinations(range(N), len(th)): + for perm in itertools.permutations(range(len(th))): + seq = []; li = iter(Ls+Rs); ti = iter(perm) + for k in range(N): seq.append(th[next(ti)] if k in pos else next(li)) + P = eye(n) + for (x, y, m) in seq: P = mm(Tf(x, y, Q(2)), P) + if P == [[Q(-1) if i == j else Q(0) for j in range(n)] for i in range(n)]: + found = True; break + if found: break + ck('S-tight', found and N == n+1, f'chain root (gL,gR)=({gL},{gR}): n={n}, product = -I with N={N} = 1 + r units (r=n): equality in N >= 1 + dim ker(R+I) = 1+n') + # hub law part (1), independent: W = prod(I-2xy^T) = I - 2 X A^-1 Y^T, A = I+2U ; W=-I => A-G has rank N-n + us = [(x, y) for (x, y, m) in reversed(seq)] # W = T_N ... T_1, left to right = reversed(seq) + W = eye(n) + for x, y in us: W = mm(W, unit(x, y, Q(-2))) + G = [[sum(us[k][1][i]*us[l][0][i] for i in range(n)) for l in range(N)] for k in range(N)] + U = [[G[k][l] if k < l else Q(0) for l in range(N)] for k in range(N)] + Ls_ = [[G[k][l] if k > l else Q(0) for l in range(N)] for k in range(N)] + A = [[Q(int(i == j)) + 2*U[i][j] for j in range(N)] for i in range(N)] + X = [[us[k][0][i] for k in range(N)] for i in range(n)]; Yt = [[us[k][1][i] for i in range(n)] for k in range(N)] + Wf = mm(mm(X, inv(A)), Yt); Wf = [[Q(int(i == j)) - 2*Wf[i][j] for j in range(n)] for i in range(n)] + Zm = [[Q(int(i == j)) + U[i][j] - Ls_[i][j] for j in range(N)] for i in range(N)] + ck('H-rank', Wf == W and rank(Zm) == N-n, f'({gL},{gR}): product formula exact; rank(I+U-L) = N-n = {rank(Zm)} (idempotent argument)') + +# ---- S: run the check scripts ------------------------------------------------------------------ +o = run('surplus_check.py'); ck('S-lemma', 'SURPLUS CHECK PASS' in o, 'ratio/seam/ledger script prints its PASS marker (exact; includes F2^4 subspace inequality, pin bookkeeping, S arithmetic, tightness)') +o = run('hub_law.py'); ck('H-law', 'PASS_HUB_LAW' in o and 'FAIL' not in o and o.count(': ok') == 10, 'hub law: rank, cocycle, divisibility, overlap at generic and degenerate nonzero D; v=1 control; 10 instances') +# ---- typed query --------------------------------------------------------------------------- +o = run('typed_query.py') +for sub in ('C=HSH == aI+bX: True | C^2==X: True', 'B-block rank_F2 = 1', 'C in F (free)? False | C in F*H*F (one H-cell, C-rank 1)? True', + 'check: True', 'K_P == H(x)H diag((-1)^(x1x2)) H(x)H : True', 'rank_F2 B: K_P = 2 | C(x)C = 2 | C(x)I = 1', + 'K_P in F*(C(x)C)*F (same Bruhat cell, rank 2)? True', + ): + ck('typed-query', sub in o, f'typed query output: {sub[:70]}') +# ---- Theorem C ---------------------------------------------------------------------------------- +def capacity(v, rs, dbl, cells, fam='onepass'): + out = run('form_capacity.py', str(v), str(rs), dbl, *[f'{a},{b}' for a, b in cells], env={'FAM': fam}) + res = [] + for ln in out.splitlines(): + if ln.startswith('v='): + kd = int(ln.split('kd=')[1].split()[0]); ku = int(ln.split('ku=')[1].split()[0]) + K = int(ln.split('|K|=')[1].split()[0]); solved = int(ln.split('solved ')[1].split('/')[0]) + t_ = ln.split('pirank max=')[1].split()[0]; mx = -1 if t_ == 'None' else int(t_); res.append((kd, ku, K, solved, mx)) + return res +cells = [(1, 0), (1, 1), (2, 1), (3, 0), (3, 1), (3, 2), (3, 3), (6, 2)] +r = capacity(3, 4, 'nodbl', cells) +ntight = sum(1 for kd, ku, K, sv, mx in r if mx == K+ku) +ck('thm5', len(r) == len(cells) and all(sv >= 1 and mx <= K+ku for kd, ku, K, sv, mx in r), f'one-pass v=3: pi-rank <= |K|+ku in all {len(r)} cells with a solution (equality in {ntight})') +ck('thm5', all(mx < 3+K for kd, ku, K, s, mx in r if ku < 3), 'hence ku < v = 3 never reaches the target pi-rank v+|K|') +r2 = capacity(2, 4, 'nodbl', [(0, 1), (2, 1), (3, 0), (2, 2)]) +ck('thm5', sum(1 for *_, s, mx in r2 if s >= 1) >= 2 and all(mx <= K+ku for kd, ku, K, s, mx in r2), f'one-pass v=2: bound holds in all solved cells ({sum(1 for *_, s, mx in r2 if s >= 1)} of {len(r2)} solved; unsolved cells are not evidence)') +rr = capacity(3, 4, 'nodbl', [(2, 1), (3, 2)], fam='rowline') +ck('thm5-scope', any(mx > K+ku for kd, ku, K, s, mx in rr), 'control: the rowline landing family exceeds the bound (outside the stated family, as stated)') + +# ---- retained arithmetic on stated numbers -------------------------------------------------------------- +o = run('ledger_arith.py') +for sub in ('f(145)*v 75049 share 0.331', 'public stop tax*18 142686 share 0.629', 'sum check 226935 vs 226939', + 'BIT cap +14.3%: needs D cut 28392 R0 = 1577 R0/call', '+2% variant: (7927-7690)*18 = 4266 share 0.0188', + 'S parts: L*Omega 864 delta*v 104 S 760', 'DONE_LEDGER'): + ck('ledger-arith', sub in o, sub) +# multi-affine vanishing on a two-point grid (symbolic D versus character grid) +for k in (2, 3, 4): + pts = list(itertools.product((1, -1), repeat=k)) + mons = list(itertools.product((0, 1), repeat=k)) + M = [[Q(1) if True else 0 for _ in mons] for _ in pts] + M = [[Q(__import__('math').prod(p[i] for i in range(k) if m[i])) for m in mons] for p in pts] + ck('multiaffine', rank(M) == 2**k, f'{k} variables: multi-affine polynomial vanishing on {{+1,-1}}^{k} is zero (evaluation matrix rank {2**k})') +print('PASS_P104_SURPLUS_HUB_FORM_NOTE' if not fails else f'FAILED: {sorted(set(fails))}') +sys.exit(1 if fails else 0) diff --git a/research/p104-surplus-hub-form-note/checks/chain_root.py b/research/p104-surplus-hub-form-note/checks/chain_root.py new file mode 100644 index 0000000000..16fdd17b7b --- /dev/null +++ b/research/p104-surplus-hub-form-note/checks/chain_root.py @@ -0,0 +1,54 @@ +# Find an ordering of chain-nested root units with product = -I (exact rationals). +import sys, itertools +from fractions import Fraction as Q +def thin_vectors(gL,gR,n,fL,fR,A,E): + sL,sR=gL%2,gR%2 + def vec(a,u,p=0,q=0): + x=[Q(0)]*n;y=[Q(0)]*n + x[A]=Q(a);y[A]=Q(u) + for i,f in enumerate(fL): x[f]=Q(a+1);y[f]=Q((1-u)*(-1)**i) + for r,h in enumerate(reversed(fR)): x[h]=Q(1-a);y[h]=Q((u-1)*(-1)**r) + if E is not None: x[E]=Q(q);y[E]=Q(p) + return x,y + if sL==sR==1: return [vec(0,1,0,1),vec(-1,2,1,0),vec(-1,3,1,-1)] + if sL==sR==0: return [vec(0,1,0,1),vec(-1,0,1,0),vec(-1,-1,1,-1)] + if sL==1: return [vec(0,1),vec(-1,0)] + return [vec(0,1),vec(1,2)] +def mm(A,B): + Bt=list(zip(*B)); return [[sum(a*b for a,b in zip(r,c)) for c in Bt] for r in A] +def units(gL,gR): + nf=1+gL+gR;e=nf%2;n=nf+e;A=0 + fL=list(range(1,1+gL));fR=list(range(1+gL,1+gL+gR));E=nf if e else None + Ls=[];Rs=[] + for i in range(gL): + x=[Q(0)]*n;y=[Q(0)]*n + x[A]=Q(1);y[A]=Q(1);x[fL[i]]=Q(1);y[fL[i]]=Q(-1) + for j in range(i): x[fL[j]]=Q(2) + Ls.append((x,y,{A}|set(fL[:i+1]))) + for m in range(gR): + x=[Q(0)]*n;y=[Q(0)]*n + x[A]=Q(-1);y[A]=Q(1);x[fR[m]]=Q(1);y[fR[m]]=Q(1) + for l in range(m+1,gR): x[fR[l]]=Q(2) + Rs.append((x,y,{A}|set(fR[m:]))) + th=[(x,y,None) for x,y in thin_vectors(gL,gR,n,fL,fR,A,E)] + return n,Ls,Rs,th +def T(x,y,c): + n=len(x);return [[Q(int(i==j))-c*x[i]*y[j] for j in range(n)] for i in range(n)] +def search(gL,gR): + n,Ls,Rs,th=units(gL,gR) + N=len(Ls)+len(Rs)+len(th) + sols=[] + for pos in itertools.combinations(range(N),len(th)): + for perm in itertools.permutations(range(len(th))): + seq=[];li=iter(Ls+Rs);ti=iter(perm) + for k in range(N): + seq.append(th[next(ti)] if k in pos else next(li)) + for c in (Q(2),Q(1)): + P=[[Q(int(i==j)) for j in range(n)] for i in range(n)] + for (x,y,m) in seq: P=mm(T(x,y,c),P) + if all(P[i][j]==(-1 if i==j else 0) for i in range(n) for j in range(n)): + sols.append((pos,perm,c)) + return sols +if __name__=="__main__": + for g in [(1,1),(2,2)]: + s=search(*g);print(g,len(s),s[:4]) diff --git a/research/p104-surplus-hub-form-note/checks/form_capacity.py b/research/p104-surplus-hub-form-note/checks/form_capacity.py new file mode 100644 index 0000000000..43218af8bf --- /dev/null +++ b/research/p104-surplus-hub-form-note/checks/form_capacity.py @@ -0,0 +1,45 @@ +"""Numerical test of the form-capacity lemma (Theorem 5 of the note). +Constrain ONLY the Y outputs (Y'_t = x_t exactly: T[Y,X]=I, T[Y,Y]=0, T[Y,K]=0); X', K' free. +Lemma: then the pi-rank (forms mod span x) of (X',K') is <= |K| + ku, for every kd. +Target needs v+|K|. So generic solutions must have pirank <= |K|+ku (and ku1e8:return Ms,np.sqrt(c),S + S,_=forward(Ms,stops,nreg,npub) + return Ms,np.sqrt(c),S +def pirank(S,v,npub,nk,tol=1e-7): + # public register order: X(v), Y(v), K(nk). columns = inputs x(v),y(v),k(nk). pi: drop x columns + XK=np.vstack([S[:v],S[2*v:npub]])[:,v:] + return np.linalg.matrix_rank(XK,tol=tol) +def run(v,kd,ku,dbl,rs,fam='onepass',seed=0): + names,npub,stops,nk=skel(v,kd,ku,fam,dbl);nreg=len(names);rng=np.random.default_rng(seed) + T=np.eye(npub);T[v:2*v,:]=0;T[v:2*v,:v]=np.eye(v) + rows=list(range(v,2*v));out=[] + for i in range(rs): + Ms,res,S=solve_masked(rows,T,stops,nreg,npub,rng) + if res<1e-9:out.append(pirank(S,v,npub,nk)) + else:out.append(None) + return nk,out +if __name__=='__main__': + v=int(sys.argv[1]);rs=int(sys.argv[2]);dbl=sys.argv[3]=='dbl' + for kd,ku in [(int(a),int(b)) for a,b in (s.split(',') for s in sys.argv[4:])]: + nk,out=run(v,kd,ku,dbl,rs,fam=os.environ.get('FAM','onepass'),seed=kd*10+ku) + ok=[o for o in out if o is not None] + print(f'v={v} dbl={dbl} kd={kd} ku={ku} |K|={nk} bound |K|+ku={nk+ku} need v+|K|={v+nk}: solved {len(ok)}/{rs} pirank max={max(ok) if ok else None} all={out}',flush=True) diff --git a/research/p104-surplus-hub-form-note/checks/hub_law.py b/research/p104-surplus-hub-form-note/checks/hub_law.py new file mode 100644 index 0000000000..fad4edd96b --- /dev/null +++ b/research/p104-surplus-hub-form-note/checks/hub_law.py @@ -0,0 +1,150 @@ +"""Hub rank law, exact check, v=2 (two ports share D), L=2 and L=4. stdlib + fractions. python3 -I -B hub_law.py +Model (hypotheses of Theorem 4): coordinate masks, units I-2xy^T (yx=0), x,y inside mask, product=-I at D=1, +D enters as Phi_k=Delta_k T_k. Port-coupling gauges: (g1) per-field GL2 mixing of the two port copies, +(g2) conjugation of the thin units alone by Omega(x)I on the port index (thin units become cross-port). +Claims tested at generic AND degenerate nonzero D: + (A) rank Z(D)=N-n=2 (B) Z_kl=1/2 Z_km Z_ml for LOCAL blocks (C) Z_fl(D)=Z_fl(1)*prod E_k, rank Z_fl(1)=2 + (D) overlap coordinates of y_l,x_f lie in every LOCAL mask, >=2 of them. +Control: same pipeline on a v=1 root must give rank 1 (known).""" +import random, itertools, sys +from fractions import Fraction as Q +import os +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +from chain_root import units, mm +random.seed(7) +fails=[] +def ck(c,m): + if not c: fails.append(m); print("FAIL",m) + return c +def rank(M): + M=[r[:] for r in M]; r=0; nr=len(M); nc=len(M[0]) if M else 0 + for c in range(nc): + p=next((i for i in range(r,nr) if M[i][c]!=0),None) + if p is None: continue + M[r],M[p]=M[p],M[r] + for i in range(nr): + if i!=r and M[i][c]!=0: + f=M[i][c]/M[r][c]; M[i]=[a-f*b for a,b in zip(M[i],M[r])] + r+=1 + return r +def inv(A): + n=len(A); M=[A[i][:]+[Q(int(i==j)) for j in range(n)] for i in range(n)] + for c in range(n): + p=next(r for r in range(c,n) if M[r][c]!=0); M[c],M[p]=M[p],M[c] + pv=M[c][c]; M[c]=[v/pv for v in M[c]] + for r in range(n): + if r!=c and M[r][c]!=0: + f=M[r][c]; M[r]=[a-f*b for a,b in zip(M[r],M[c])] + return [r[n:] for r in M] +def matvec(A,x): return [sum(a*b for a,b in zip(r,x)) for r in A] +def build(gL,gR,v,coupling): + n,Ls,Rs,th=units(gL,gR) + nn=v*n + def lift(x,p): # port p copy: coordinate (c,p) -> c*v+p + out=[Q(0)]*nn + for c in range(n): out[c*v+p]=x[c] + return out + # blocks: list of (kind, [(x,y)...], mask-set-of-big-coords or None, siteindex) + sites=[] + for kind,seq in (('L',Ls),('T',th),('R',Rs)): pass + seq=Ls+th+Rs + # order: Ls, thin, Rs + for idx,(x,y,m) in enumerate(seq): + pairs=[(lift(x,p),lift(y,p)) for p in range(v)] + mask=None if m is None else {c*v+p for c in m for p in range(v)} + sites.append(dict(pairs=pairs,mask=mask,local=m is not None)) + if 'g2' in coupling: + while True: + Om=[[Q(random.randint(-3,3)) for _ in range(v)] for _ in range(v)] + if rank(Om)==v: break + O=[[Q(0)]*nn for _ in range(nn)] + for c in range(n): + for a in range(v): + for b in range(v): O[c*v+a][c*v+b]=Om[a][b] + Oi=inv(O) + for s in sites: + if not s['local']: + s['pairs']=[(matvec(O,x),[sum(y[i]*Oi[i][j] for i in range(nn)) for j in range(nn)]) for x,y in s['pairs']] + # gauge g1: per-field GL_v acting on port copies + if 'g1' in coupling: + W=[[Q(int(i==j)) for j in range(nn)] for i in range(nn)] + for c in range(n): + while True: + B=[[Q(random.randint(-2,2)) for _ in range(v)] for _ in range(v)] + if rank(B)==v: break + for a in range(v): + for b in range(v): W[c*v+a][c*v+b]=B[a][b] + Wi=inv(W) + for s in sites: + s['pairs']=[(matvec(W,x),[sum(y[i]*Wi[i][j] for i in range(nn)) for j in range(nn)]) for x,y in s['pairs']] + return nn,sites +def Tm(x,y,nn): return [[Q(int(i==j))-2*x[i]*y[j] for j in range(nn)] for i in range(nn)] +def check_instance(gL,gR,v,coupling,Dlist): + nn,sites=build(gL,gR,v,coupling) + # product = -I at D=1 + P=[[Q(int(i==j)) for j in range(nn)] for i in range(nn)] + for s in sites: + for x,y in s['pairs']: P=mm(Tm(x,y,nn),P) + ck(all(P[i][j]==(-1 if i==j else 0) for i in range(nn) for j in range(nn)),f"{gL,gR,v,coupling}: product -I") + # unit list with site id + U=[(si,x,y) for si,s in enumerate(sites) for x,y in s['pairs']] + N=len(U); loc=[si for si,s in enumerate(sites) if s['local']] + ck(N-nn==v,"excess N-n=v") + def delta_inv_pref(D): + # diag of prod_{kj else -g) + return Z + # block index sets for LOCAL sites + blk={}; pos=0 + for si,s in enumerate(sites): + k=len(s['pairs']); blk[si]=list(range(pos,pos+k)); pos+=k + def sub(Z,a,b): return [[Z[i][j] for j in blk[b]] for i in blk[a]] + Z1=Zmat({si:Q(1) for si in loc}) + f,l=loc[0],loc[-1] + for D in Dlist: + Dd={si:D[t] for t,si in enumerate(loc)} + Z=Zmat(Dd) + ck(rank(Z)==N-nn,f"rank Z(D) {gL,gR,v,coupling} D={[str(d) for d in D]}: {rank(Z)}") + for a,m,b in itertools.product(loc,loc,loc): + if a==m or m==b: continue # a=m trivial identity needs Z_mm; skip degenerate + Zam,Zmb,Zab=sub(Z,a,m),sub(Z,m,b),sub(Z,a,b) + prod=mm(Zam,Zmb) + ck(all(Zab[i][j]==prod[i][j]/2 for i in range(v) for j in range(v)),f"cocycle {a,m,b}") + Zfl=sub(Z,f,l); Z1fl=sub(Z1,f,l) + pe=Q(1) + for si in loc: + if f<=si=v,"overlap >= v coords") + return len(ov),len(allm) +def Dsets(nl): + g=lambda: Q(random.randint(2,40),random.randint(2,40)) + out=[[g() for _ in range(nl)] for _ in range(3)] + out+= [[Q(1)]*nl, [Q(-1)]*nl, [Q(-1) if i%2 else Q(1) for i in range(nl)], + [Q(2)]*nl, [Q(2) if i%2 else Q(1,2) for i in range(nl)], # D_jD_k=1 + [Q(1)]*(nl-1)+[Q(3)], [Q(-1,3)]*nl, [Q(random.choice([1,-1,2,Q(1,2),-2])) for _ in range(nl)]] + return out +for (gL,gR) in [(1,1),(2,2)]: + nl=gL+gR + for v,cp in [(1,''),(2,''),(2,'g1'),(2,'g2'),(2,'g1g2')]: + r=check_instance(gL,gR,v,cp,Dsets(nl)); print(f"L={nl} v={v} coupling={cp or 'none'}: ok overlap={r[0]} allmask={r[1]}",flush=True) +print("PASS_HUB_LAW" if not fails else f"FAILS {len(fails)}") diff --git a/research/p104-surplus-hub-form-note/checks/ledger_arith.py b/research/p104-surplus-hub-form-note/checks/ledger_arith.py new file mode 100644 index 0000000000..b2f673dce0 --- /dev/null +++ b/research/p104-surplus-hub-form-note/checks/ledger_arith.py @@ -0,0 +1,84 @@ +#!/usr/bin/env python3 +# Short exact arithmetic on stated numbers (stdlib, seconds). The inputs below (D, root, taxes) are +# constants typed in from the reference invoice; they are NOT recomputed from a pricing file here. +# Prints DONE_LEDGER. +from math import log +from itertools import product +from fractions import Fraction as Fr + +f = lambda x: x * log(x) if x > 0 else 0.0 + +# 1. Ledger re-cut: D = root net of perfect mains + public stop tax - owned (stated numbers). +v, L, c = 104, 18, 56 +D = 226939 +root = 147560 +main_perfect = 2 * v * f(8) # both mains as one rank-8 job per port +tax_h, tax_x, tax_y = 5775, 1091, 1061 +print("f(145)*v", round(f(145) * v), "share", round(f(145) * v / D, 3)) +print("root net of perfect mains", round(root - L * main_perfect), "share", round((root - L * main_perfect) / D, 3)) +print("public stop tax*18", L * (tax_h + tax_x + tax_y), "share", round(L * (tax_h + tax_x + tax_y) / D, 3)) +print("sum check", round(root - L * main_perfect + L * (tax_h + tax_x + tax_y) - 1028), "vs", D) +print("BIT cap +14.3%: needs D cut", round(D * (1 - 1 / 1.143)), "R0 =", round(D * (1 - 1 / 1.143) / L), "R0/call") +print("+2% variant: (7927-7690)*18 =", (7927 - 7690) * 18, "share", round((7927 - 7690) * 18 / D, 4)) +print("floor public 5829 + ride 292 => R0/call", 5829 + 292, "gain share", round((7927 - 5829 - 292) * 18 / D, 4)) +print("S parts: L*Omega", L * (v - c), "delta*v", v, "S", L * (v - c) - v) + +# 2. Column fusion of two direct-sum copies of the chain root (candidate). +# Merging two copies of a field (rank r, idle w): dD = 2(r-w) ln 2 per port (first-order form f(2x)-2f(x)=2x ln2). +ln2 = log(2) +hub = 2 * 145 * ln2 +chain_field = 2 * 9 * ln2 # r=8n+1, idle=8n-8: r-w=9 for every n +local_gain_per_pair = 2 * ln2 * 1720 / v # native net mass 1720/call +print("merge hub", round(hub, 2), "chain field", round(chain_field, 2), "local gain/pair per port", round(local_gain_per_pair, 2)) +print("net per fused pair", round(local_gain_per_pair - chain_field, 2), "x18 =", round(18 * (local_gain_per_pair - chain_field), 2), "vs hub", round(hub, 2)) + +# 3. Non-flat toy: min rank of the partial matrix for the triangle of bases. +# Port types are pairs of bases {1,2},{2,3},{1,3}; rows (type,base), cols (type,base). +# Entry (a,b) has class P_a xor P_b; a cell's classes must cancel, identity class sums to 1. +types = [(1, 2), (2, 3), (1, 3)] +idx = [(t, a) for t in types for a in t] +P = 7 + + +def rank_mod(M): + M = [r[:] for r in M] + rk = 0 + n = len(M) + for col in range(n): + piv = next((i for i in range(rk, n) if M[i][col] % P), None) + if piv is None: + continue + M[rk], M[piv] = M[piv], M[rk] + inv = pow(M[rk][col], P - 2, P) + M[rk] = [(x * inv) % P for x in M[rk]] + for i in range(n): + if i != rk and M[i][col] % P: + g = M[i][col] + M[i] = [(x - g * y) % P for x, y in zip(M[i], M[rk])] + rk += 1 + return rk + + +def build(free): + Z = [[0] * 6 for _ in range(6)] + for i, (s, a) in enumerate(idx): + for j, (t, b) in enumerate(idx): + if s != t: + # different types share exactly one base; only that identity entry is nonzero. + common = set(s) & set(t) + Z[i][j] = 1 if a == b and a in common else 0 + k = 0 + for t in types: + i0 = idx.index((t, t[0])) + z11, z12 = free[k], free[k + 1] + k += 2 + Z[i0][i0] = z11 + Z[i0][i0 + 1] = z12 + Z[i0 + 1][i0] = (-z12) % P # the two cross entries share a class mod Pauli + Z[i0 + 1][i0 + 1] = (1 - z11) % P + return Z + + +best = min(rank_mod(build(fr)) for fr in product(range(P), repeat=6)) +print("triangle: flat registers 3, non-flat min rank mod", P, "=", best) +print("DONE_LEDGER") diff --git a/research/p104-surplus-hub-form-note/checks/stop_family.py b/research/p104-surplus-hub-form-note/checks/stop_family.py new file mode 100644 index 0000000000..dfcb1cb7d5 --- /dev/null +++ b/research/p104-surplus-hub-form-note/checks/stop_family.py @@ -0,0 +1,61 @@ +"""Stop families used by form_capacity.py (variants of the one-pass family). All compressed: no per-port crossing sets. + family 'rowline': down rows land at a line r (bottom dim 1, T3 style) on the helpers h_r*, after X reached V: stops L2_r. Zero-form helpers can then deliver x_t to Y_t. + family 'gather' : X_r climbs line -> block G_S -> V. Up rows land at G_S before the block helpers read X (multi-pass: X written then read). Down rows V->0 as before. + family 'both' : rowline + gather. + 'dbl' = 2 helpers per ordered pair. Controls: planted same size; F at (1,0).""" +import sys,os,time +sys.path.insert(0,os.path.dirname(os.path.abspath(__file__))) +import numpy as np +from stop_solver import solve,forward,legal,target,GS,assert_frames +def skel(v,kd,ku,fam,dbl=False,blocks=None): + V=frozenset(range(v));Z=frozenset() + X=['X%d'%r for r in range(v)];Y=['Y%d'%t for t in range(v)] + K=[f'h{r}_{t}' for r in range(v) for t in range(v) if r!=t] + if dbl:K+=[f'i{r}_{t}' for r in range(v) for t in range(v) if r!=t] + lk=lambda r:[k for k in K if k[1:].startswith(f'{r}_')] + pk=lambda t:[k for k in K if k.endswith(f'_{t}')] + B=[f'B{i}' for i in range(kd)];A=[f'A{i}' for i in range(ku)] + E=[f'E{i}' for i in range(v)];OV=[f'O{i}' for i in range(v)];OL=[f'Ol{r}' for r in range(v)];OP=[f'Op{t}' for t in range(v)] + pub=X+Y+K;own=B+A+E+OV+OL+OP;names=pub+own;idx={n:i for i,n in enumerate(names)};st=[] + blocks=blocks or [list(range(v))[:v//2],list(range(v))[v//2:]] + gather=fam in('gather','both');rowline=fam in('rowline','both') + st.append((Z,Y+K+E+A)) + for r in range(v):st.append((frozenset([r]),[X[r],OL[r]]+lk(r))) + if gather: + # block stop: only helpers leaving toward t outside the block may ride; a second visit of those helpers reads the X just written by the row + for bi,S in enumerate(blocks): + hs=[k for k in K if int(k[1:].split('_')[0]) in S and int(k.split('_')[1]) not in S] + st.append((frozenset(S),[X[r] for r in S]+[A[j] for j in range(ku) if j%len(blocks)==bi]+hs)) + st.append((V,X+A+B+OV)) + if rowline: + for r in range(v):st.append((frozenset([r]),lk(r)+[B[i] for i in range(kd) if i%v==r]+[OL[r]])) + else:st.append((Z,Y+B+E)) + for t in range(v):st.append((V-{t},[Y[t],OP[t]]+pk(t))) + st.append((V,X+K+A+OV)) + return names,len(pub),[(f,[idx[n] for n in r]) for f,r in st],len(K) +def go(v,kd,ku,fam,tg,rs,dbl=False,planted=False,seed=0,iters=800): + names,npub,stops,nk=skel(v,kd,ku,fam,dbl) + if fam not in('gather','both'):assert_frames(names,npub,stops,v) + else: + seen={} + for f,regs in stops: + for i in regs: + n=names[i] + if i4;t0=time.time() + print(v,fam,'dbl' if dbl else '','planted(1,1)',go(v,1,1,fam,'x',2,dbl,planted=True),'planted(2,1)',go(v,2,1,fam,'x',1,dbl,planted=True),flush=True) + for tg in ('FB','F','W','J'): + for kd in range(0,v+1): + print(tg,'kd',kd,' ku0..v:',' | '.join(go(v,kd,ku,fam,tg,rs,dbl,seed=kd*10+ku) for ku in range(0,v+1)),'t=%.0f'%(time.time()-t0),flush=True) diff --git a/research/p104-surplus-hub-form-note/checks/stop_solver.py b/research/p104-surplus-hub-form-note/checks/stop_solver.py new file mode 100644 index 0000000000..7fb7ec9d98 --- /dev/null +++ b/research/p104-surplus-hub-form-note/checks/stop_solver.py @@ -0,0 +1,126 @@ +"""Numeric solver: multilinear stop model, Levenberg-Marquardt on the dual (J J^T) system. +Word = ordered stops; each stop applies a free matrix M_i (superset of ADD/SCALE) to the registers at one common frame. +Owned regs init 0, dropped at end (dirty clear). Public finals must equal the target exactly. +Skeleton: v independent ports e_r in F_2^v, N = diag (r.t = 0 for r != t). +Frame paths are monotone for public regs and are checked by assert_frames. +Unsolved is NOT a proof. Every table row is preceded by same-size planted and known-feasible controls. +usage: stop_solver.py v kd ku target restarts [seed] [family]""" +import sys, numpy as np + +def skeleton(v, kd, ku, helpers=True, ee=None, family='onepass'): + """returns names, npub, stops (list of (frame, reglist)). + frames: frozenset of port indices = span of those e_r; pp(t) = all ports except t; V = all.""" + V = frozenset(range(v)); Z = frozenset() + X = ['X%d' % r for r in range(v)]; Y = ['Y%d' % t for t in range(v)] + K = ['h%d_%d' % (r, t) for r in range(v) for t in range(v) if r != t] if helpers else [] + B = ['B%d' % i for i in range(kd)] # down rows V -> Z + A = ['A%d' % i for i in range(ku)] # up rows Z -> V (read at Z, landing at V1) + A2 = [] + E = ['E%d' % i for i in range(v if ee is None else ee)] # owned erasure at frame 0, never moves + OV = ['O%d' % i for i in range(v if ee is None else ee)] # owned scratch at V, never moves + OL = ['Ol%d' % r for r in range(v)] # one owned scratch per line stop + OP = ['Op%d' % t for t in range(v)] # one owned scratch per pp stop + if family == 'twoup': # half of the up rows land only after a second read at Z2 + A2 = A[ku // 2:]; A = A[:ku // 2] + G = ['g%d' % t for t in range(v)] if family in ('land', 'landdual', 'landboth') else [] # public helpers that stay at 0 through Z2, then climb to pp_t, then V + if family in ('landdual', 'landboth'): K2 = ['u%d' % r for r in range(v)] # public helpers: 0 -> line r -> V, late to the line (dual role) + else: K2 = [] + K = K + G + K2 + pub = X + Y + K; own = B + A + A2 + E + OV + OL + OP + names = pub + own; idx = {n: i for i, n in enumerate(names)} + st = [] + st.append((Z, Y + K + A + A2 + E)) + for r in range(v): + st.append((frozenset([r]), [X[r], OL[r]] + [k for k in K if k.startswith('h%d_' % r)] + ([K2[r]] if K2 else []))) + st.append((V, X + A + B + OV)) + st.append((Z, Y + B + E + A2 + G)) + if family == 'pingpong': # one more X-top / Y-bottom exchange: rows are the only link + st.append((V, X + A + B + OV)); st.append((Z, Y + B + E + A2)) + for t in range(v): + st.append((frozenset(p for p in V if p != t), [Y[t], OP[t]] + [k for k in K if k.endswith('_%d' % t)] + ([G[t]] if G else []))) + st.append((V, X + K + A + A2 + OV)) # B rows are NOT here: a down row that returned to V would be an uncounted up crossing + return names, idx, len(pub), [(f, [idx[n] for n in regs]) for f, regs in st], (X, Y, K) + +def assert_frames(names, npub, stops, v): + """public regs must ascend, and X_r / Y_t must respect the pins; owned are free.""" + seen = {} + for f, regs in stops: + for i in regs: + n = names[i] + if i < npub: + if n in seen: assert seen[n] <= f, ('descent', n) + seen[n] = f + if n[0] == 'X': assert int(n[1:]) in f, ('X pin', n) + if n[0] == 'Y': assert int(n[1:]) not in f, ('Y pin', n) + +def target(v, g, nk): + a, b, c, d = g; n = 2 * v + nk; T = np.eye(n) + T[:v, :v] = a * np.eye(v); T[:v, v:2 * v] = b * np.eye(v) + T[v:2 * v, :v] = c * np.eye(v); T[v:2 * v, v:2 * v] = d * np.eye(v) + return T + +def forward(Ms, stops, nreg, npub): + S = np.zeros((nreg, npub)); S[:npub, :npub] = np.eye(npub); pres = [] + for M, (f, r) in zip(Ms, stops): + pres.append(S[r].copy()); S[r] = M @ S[r] + return S, pres + +def backward(Ms, stops, nreg, npub): + P = np.zeros((npub, nreg)); P[:npub, :npub] = np.eye(npub); posts = [None] * len(stops) + for i in range(len(stops) - 1, -1, -1): + r = stops[i][1]; posts[i] = P[:, r].copy(); P[:, r] = P[:, r] @ Ms[i] + return posts + +def solve(T, stops, nreg, npub, rng, iters=400, sigma=.4, tol=1e-10, verbose=False): + Ms = [np.eye(len(r)) + rng.normal(0, sigma, (len(r), len(r))) for f, r in stops] + lam = 1e-1; S, pres = forward(Ms, stops, nreg, npub); R = S[:npub] - T; c = np.sum(R * R) + n2 = npub * npub + for it in range(iters): + if c < tol * tol: break + posts = backward(Ms, stops, nreg, npub) + G = np.zeros((n2, n2)) + for P, Q in zip(posts, pres): + G += np.kron(P @ P.T, Q.T @ Q) + rhs = R.ravel() + while True: + W = np.linalg.solve(G + lam * np.eye(n2), rhs).reshape(npub, npub) + new = [M - P.T @ W @ Q.T for M, P, Q in zip(Ms, posts, pres)] + S2, pres2 = forward(new, stops, nreg, npub); R2 = S2[:npub] - T; c2 = np.sum(R2 * R2) + if c2 < c: + Ms, pres, R, c = new, pres2, R2, c2; lam = max(lam / 3, 1e-13); break + lam *= 4 + if lam > 1e8: return Ms, np.sqrt(c), it + if verbose and it % 20 == 0: print(it, np.sqrt(c), lam, flush=True) + return Ms, np.sqrt(c), it + +def legal(Ms, stops, nreg, npub): + """Each stop must keep the rank of the content it touches (else it would erase public content without an owned home).""" + S = np.zeros((nreg, npub)); S[:npub, :npub] = np.eye(npub); worst = 0 + for M, (f, r) in zip(Ms, stops): + a = np.linalg.matrix_rank(S[r], tol=1e-7); S[r] = M @ S[r]; b = np.linalg.matrix_rank(S[r], tol=1e-7) + worst = max(worst, a - b) + return worst == 0, max(np.abs(M).max() for M in Ms) + +GS = {'J': (0, -1, 1, 0), 'W': (1, -1, 1, 0), 'Wd': (0, -1, 1, 1), 'F': (1, 0, 1, 1), 'FB': (1, -1, 1, 0.5), 'I': (1, 0, 0, 1)} + +def run(v, kd, ku, tg, restarts, seed=0, family='onepass', helpers=True, planted=False, iters=600): + names, idx, npub, stops, (X, Y, K) = skeleton(v, kd, ku, helpers, family=family) + assert_frames(names, npub, stops, v); nreg = len(names); rng = np.random.default_rng(seed) + if planted: + Ms = [np.eye(len(r)) + rng.normal(0, .5, (len(r), len(r))) for f, r in stops] + T = forward(Ms, stops, nreg, npub)[0][:npub] + else: + T = target(v, GS[tg], len(K)) + hits = 0; best = 1e9; legalhits = 0; bm = None + for i in range(restarts): + Ms, res, it = solve(T, stops, nreg, npub, rng, iters=iters) + best = min(best, res) + if res < 1e-8: + hits += 1; ok, mx = legal(Ms, stops, nreg, npub); legalhits += ok + if ok and bm is None: bm = Ms + return dict(v=v, kd=kd, ku=ku, tg='planted' if planted else tg, fam=family, helpers=helpers, npub=npub, nreg=nreg, hits=hits, legal=legalhits, restarts=restarts, best=best), bm, stops, names + +if __name__ == '__main__': + v, kd, ku = map(int, sys.argv[1:4]); tg = sys.argv[4]; rs = int(sys.argv[5]) + seed = int(sys.argv[6]) if len(sys.argv) > 6 else 0; fam = sys.argv[7] if len(sys.argv) > 7 else 'onepass' + print(run(v, kd, ku, tg, rs, seed, fam, planted=(tg == 'planted'))[0], flush=True) diff --git a/research/p104-surplus-hub-form-note/checks/surplus_check.py b/research/p104-surplus-hub-form-note/checks/surplus_check.py new file mode 100644 index 0000000000..457962ee0e --- /dev/null +++ b/research/p104-surplus-hub-form-note/checks/surplus_check.py @@ -0,0 +1,235 @@ +"""surplus_check.py -- exact, standard library only (fractions, itertools, random,). +Prints 'SURPLUS CHECK PASS' iff every CORE check holds. +Sections + A. Ratio lemma N >= 1 + dim ker(R+I) (exact rationals, n=4, N=3..5, plus tightness and scratch toy) + B. Seam model rank conservation (exhaustive F2 subspace metric on F2^4 + pin bookkeeping + 884 identity) + C. S arithmetic identity, bound, equality on the reference record, other port sets, closure sweeps +Hypothesis labels (a) SPEC/cost model, (b) verifier convention, (c) family assumption are given in the note (THEOREM.md); +here each check names the hypothesis it exercises (H-numbers of an earlier draft; see the note for current numbering). +""" +import itertools, random, os, sys +from fractions import Fraction as Fr + +FAILS = [] +def ok(cond, msg): + print((' ok ' if cond else ' FAIL ') + msg) + if not cond: FAILS.append(msg) + +# ---------------------------------------------------------------- exact linear algebra +def eye(n): return [[Fr(int(i == j)) for j in range(n)] for i in range(n)] +def mm(A, B): + Bt = list(zip(*B)) + return [[sum(a * b for a, b in zip(r, c)) for c in Bt] for r in A] +def madd(A, B, s=1): return [[a + s * b for a, b in zip(r, q)] for r, q in zip(A, B)] +def msc(A, s): return [[s * a for a in r] for r in A] +def tr(A): return [list(r) for r in zip(*A)] +def outer(x, y): return [[a * b for b in y] for a in x] +def dot(x, y): return sum(a * b for a, b in zip(x, y)) +def rref(A): + M = [list(map(Fr, r)) for r in A]; rows, cols = len(M), len(M[0]); piv = []; r = 0 + for c in range(cols): + p = next((i for i in range(r, rows) if M[i][c] != 0), None) + if p is None: continue + M[r], M[p] = M[p], M[r] + pv = M[r][c]; M[r] = [v / pv for v in M[r]] + for i in range(rows): + if i != r and M[i][c] != 0: + f = M[i][c]; M[i] = [a - f * b for a, b in zip(M[i], M[r])] + piv.append(c); r += 1 + if r == rows: break + return M, piv +def rank(A): return len(rref(A)[1]) +def inv(A): + n = len(A); aug = [list(map(Fr, A[i])) + eye(n)[i] for i in range(n)] + M, piv = rref(aug) + assert piv[:n] == list(range(n)), 'singular' + return [r[n:] for r in M] +def nullity(A): return len(A[0]) - rank(A) +def det_nonzero(A): return rank(A) == len(A) +def matpow_prod(Ms): # product Ms[-1] ... Ms[0] (Ms[0] applied first) + P = eye(len(Ms[0])) + for M in Ms: P = mm(M, P) + return P + +# ================================================================ A. RATIO LEMMA +print('A. Ratio lemma N >= 1 + dim ker(R+I) [hyps H2 isotropic rank-1 Q-odd units, H4 exact at Q=+-1, H5 no leak]') +rnd = random.Random(20261108) +def rvec(n, lo=-3, hi=3): return [Fr(rnd.randint(lo, hi)) for _ in range(n)] +def iso_unit(n): + while True: + x, y = rvec(n), rvec(n) + if all(v == 0 for v in x): continue + y = [b - dot(y, x) / dot(x, x) * a for a, b in zip(x, y)] + if any(v != 0 for v in y): return x, y +def rnd_gl(n): + while True: + G = [[Fr(rnd.randint(-2, 2)) for _ in range(n)] for _ in range(n)] + if det_nonzero(G): return G +n = 4 +for N in (3, 4, 5): + worst = 0; formula_ok = True; lemma_ok = True; ranks_ok = True + for trial in range(30): + units = [iso_unit(n) for _ in range(N)]; Gs = [rnd_gl(n) for _ in range(N + 1)] + def P(Q): + M = Gs[0] + for k, (x, y) in enumerate(units): + U = madd(eye(n), outer(x, y), Q) + M = mm(Gs[k + 1], mm(U, M)) + return M + P1, Pm = P(1), P(-1) + Gtot = eye(n) + for G in Gs: Gtot = mm(G, Gtot) + # conjugated product A(Q) = Gtot^{-1} P(Q) = prod (I + Q x~ y~^T) with x~,y~ the conjugated vectors + Gi = inv(Gtot) + S = madd(mm(Gi, madd(P1, Pm)), eye(n), -2) + rk = rank(S); worst = max(worst, rk) + R = mm(Pm, inv(P1)); k = nullity(madd(R, eye(n))) + lemma_ok &= (N >= 1 + k); ranks_ok &= (rk <= N - 1) + # step 1 of the proof: conjugate every G to the left; unit k becomes I + Q xt_k yt_k^T + xt, yt = [], [] + for k_, (x, y) in enumerate(units): + # unit k_ is applied after pre_k = Gs[k_]..Gs[0]; pulling all G left gives xt = pre_k^-1 x, yt^T = y^T pre_k + pre_k = eye(n) + for G in Gs[:k_ + 1]: pre_k = mm(G, pre_k) + Hi = inv(pre_k) + xt.append([sum(Hi[i][j] * x[j] for j in range(n)) for i in range(n)]) + yt.append([sum(y[j] * pre_k[j][i] for j in range(n)) for i in range(n)]) + # A(Q) = Gtot^{-1}P(Q) = prod_k (I + Q xt_k yt_k^T) in time order, times nothing else + for Q in (1, -1): + A = eye(n) + for k_ in range(N): A = mm(madd(eye(n), outer(xt[k_], yt[k_]), Q), A) + formula_ok &= (A == mm(Gi, P(Q))) + # isotropy of conjugated units + formula_ok &= all(dot(yt[k_], xt[k_]) == 0 for k_ in range(N)) + # product formula A(c) = I + c X (I - cL)^-1 Y^T, L_{kj} = yt_k . xt_j (k>j) + L = [[dot(yt[a], xt[b]) if a > b else Fr(0) for b in range(N)] for a in range(N)] + X = [[xt[k_][i] for k_ in range(N)] for i in range(n)] # n x N + YT = [yt[k_] for k_ in range(N)] # N x n + for c in (1, -1): + T = inv(madd(eye(N), L, -c)) + Ac = madd(eye(n), msc(mm(X, mm(T, YT)), c)) + formula_ok &= (Ac == mm(Gi, P(c))) + ranks_ok &= (rank(L) <= N - 1) and all(v == 0 for v in L[0]) + ok(formula_ok, f'n={n} N={N}: A(c)=I+cX(I-cL)^-1Y^T, isotropy kept under conjugation (30 trials)') + ok(ranks_ok and worst <= N - 1, f'n={n} N={N}: rank(A(1)+A(-1)-2I) <= rank L <= N-1 (max seen {worst}, bound {N - 1})') + ok(lemma_ok, f'n={n} N={N}: N >= 1 + dim ker(R+I) in all 30 trials') + +# tightness 1: SL2 Weyl word, n=2, N=3, G=identity, R=-I; exhaustive: no N=2 word exists in a small family +def shear(u, t): + a, b = u; return [[t * a * (-b), t * a * a], [t * b * (-b), t * b * a]] # t u (u_perp)^T, isotropic nilpotent +def qunit(Nm, Q): return [[(1 if i == j else 0) + Q * Nm[i][j] for j in range(2)] for i in range(2)] +vecs = [(1, 0), (0, 1), (1, 1), (1, -1), (1, 2), (2, 1), (1, -2), (2, -1)] +ts = [1, -1, 2, -2, Fr(1, 2), Fr(-1, 2)] +pool = [shear(u, t) for u in vecs for t in ts] +def word_is_minus_I(combo): + A1 = [[Fr(1), Fr(0)], [Fr(0), Fr(1)]]; Am = [r[:] for r in A1] + for c in combo: + A1 = mm(qunit(pool[c], 1), A1); Am = mm(qunit(pool[c], -1), Am) + return all(Am[i][j] == -A1[i][j] for i in range(2) for j in range(2)) +found2 = sum(word_is_minus_I(c) for c in itertools.product(range(len(pool)), repeat=2)) +found3 = sum(word_is_minus_I(c) for c in itertools.product(range(len(pool)), repeat=3)) +ok(found2 == 0, 'n=2, r=2 (R=-I): no N=2 word in the 48-unit family (lemma: N>=3)') +ok(found3 > 0, f'n=2, r=2 (R=-I): N=3 words exist ({found3} in the family) -> lemma tight at n=2') + +# tightness 2: the n=4 chain root (TRACEDELTA a) in Q-form; unit(Q) = (I - x y^T)(I + Q x y^T) = I + (Q-1) x y^T +n4, N5 = 4, 5 +Gm = [[Fr((i > j) - (i < j)) for j in range(N5)] for i in range(N5)] # sign(i-j) +Xc = [[Fr(0)] * N5 for _ in range(n4)] +for k in range(n4): Xc[k][k] = Fr(1) +for k in range(n4): Xc[k][4] = Fr(-((-1) ** k)) +Yc = [[Gm[i][k] for i in range(N5)] for k in range(n4)] # 4 x 5, Y = (G[:, :4])^T +xs = [[Xc[i][j] for i in range(n4)] for j in range(N5)]; ys = [[Yc[i][j] for i in range(n4)] for j in range(N5)] +ok(all(dot(ys[i], xs[j]) == Gm[i][j] for i in range(N5) for j in range(N5)), 'chain root: Gram y_i.x_j = sign(i-j) (isotropic)') +prodm = matpow_prod([madd(eye(n4), outer(xs[k], ys[k]), -2) for k in range(N5)]) +ok(prodm == msc(eye(n4), -1), 'chain root: prod (I - 2 x_k y_k^T) = -I exactly with N = n+1 = 5 units') +def unitQ(k, Q): return madd(eye(n4), outer(xs[k], ys[k]), Q - 1) +P1 = matpow_prod([unitQ(k, 1) for k in range(N5)]); Pm = matpow_prod([unitQ(k, -1) for k in range(N5)]) +Rr = mm(Pm, inv(P1)) +ok(P1 == eye(n4) and Rr == msc(eye(n4), -1) and nullity(madd(Rr, eye(n4))) == 4, + 'chain root in Q-form: P(+1)=I, P(-1)=-I, R=-I, dim ker(R+I)=4, so N=5=1+r: EQUALITY in the ratio lemma') +ok(all(mm(madd(eye(n4), outer(xs[k], ys[k]), 1), madd(eye(n4), outer(xs[k], ys[k]), -1)) == eye(n4) for k in range(N5)), + 'chain root: isotropy => (I+xy^T)(I-xy^T)=I (Q-odd units invertible at both characters)') + +# scratch toy (H5): N = n = 1 with one scratch coordinate: V-block of R is -1 yet ker(R+I)=0 and the leak R_HV != 0 +x, y = [Fr(1), Fr(1)], [Fr(1), Fr(-1)] # coordinates (V, H); y.x = 0 +Rs = madd(eye(2), outer(x, y), -2) # R = I - 2 x y^T for the single Q-odd unit +ok(dot(y, x) == 0 and Rs[0][0] == -1 and Rs[1][0] != 0 and nullity(madd(Rs, eye(2))) == 0, + 'scratch toy: N=n=1, V-block of R = -1 (credit looks complete) but ker(R+I)=0 and R_HV = %s != 0 (junk leak): scratch leaves H5' % Rs[1][0]) + +# block roots: lemma per block gives N >= sum(1+r_b) = r + B +ok(sum(1 + r for r in (2, 2)) == 4 + 2 and 1 + 4 == 5 < 6, 'block split: two (n=2) blocks need N >= 6 vs one n=4 root N >= 5 (+1 per block)') + +# ================================================================ B. SEAM MODEL +print('B. Seam lemma [hyps H7 (i) contacts rank-preserving (b), (ii) price >= |dim| rank change (a), (iii) natives Q-free (b), (iv) pins (a)]') +# (ii): Fourier rank d(U,W) = dim U + dim W - 2 dim(U cap W) on subspaces of F2^m is a metric with d >= |dim U - dim W| +m = 4 +def span(vs): + S = {0} + for v in vs: S |= {s ^ v for s in S} + return frozenset(S) +subs = set() +for k in range(0, m + 1): + for vs in itertools.combinations(range(1, 2 ** m), k): subs.add(span(vs)) +subs = sorted(subs, key=lambda s: (len(s), sorted(s))) +dimof = lambda S: len(S).bit_length() - 1 +d = lambda U, W: dimof(U) + dimof(W) - 2 * dimof(U & W) +ok(len(subs) == 67, f'F2^4 has {len(subs)} subspaces (expect 67)') +ok(all(d(U, W) >= abs(dimof(U) - dimof(W)) for U in subs for W in subs), '(ii) d(U,W) >= |dim U - dim W| for all 4489 pairs') +ok(all((d(U, W) == abs(dimof(U) - dimof(W))) == (U <= W or W <= U) for U in subs for W in subs), '(ii) equality iff U, W nested') +ok(all(d(U, W) <= d(U, V) + d(V, W) for U in subs for V in subs for W in subs), 'd is a metric (triangle, 67^3 triples)') +# consequence: any priced path from dim a to dim b costs >= |b - a| (here: 8 per stage in the real model); equality iff monotone/nested +# pin bookkeeping (entry ranks 8s+1 and 8s as stated; checked as arithmetic only) +ent_X = lambda s: 8 * s + 1; ent_Y = lambda s: 8 * s +okp = True +for s in range(1, 18): + # register R: Y in call s then X' in call s+1 ; register X: X in call s then Y' in call s+1 + r_exit = ent_Y(s) + 8; r_next = ent_X(s + 1); x_exit = ent_X(s) + 8; x_next = ent_Y(s + 1) + okp &= (r_next - r_exit == +1) and (x_next - x_exit == -1) + okp &= (r_next + 8 - ent_Y(s) - 1 == 16) and (x_next + 8 - ent_X(s) + 1 == 16) # natives supply 16 per register per pair +ok(okp, 'pair accounting, stages 1..17: interstitials are +1 / -1 and the two natives supply exactly 16 per register') +ok((ent_Y(3), ent_Y(3) + 8 + 1 + 8, ent_X(3), ent_X(3) + 8 - 1 + 8) == (24, 41, 25, 40), 'pair (3,4): R 24 -> 41, X 25 -> 40 (arithmetic on stated entry ranks)') +# ledger identity: outer credit = idle rank + main rank + n +outer_credit = 145 + 2 * sum(range(9, 74, 8)) + 1 +idle = 2 * sum(range(8, 65, 8)); mains = 16 * 18; nfld = 20 +ok((outer_credit, idle, mains) == (884, 576, 288) and outer_credit == idle + mains + nfld, '884 = 576 + 288 + 20 (outer credit = idles + mains + n; arithmetic on stated numbers)') + +# ================================================================ C. S ARITHMETIC +print('C. S theorem arithmetic [hyps H6 ledger, H8 hosting h<=1, H9 c>=56, H10 thin price 1]') +v, L, c, n_ = 104, 18, 56, 20 +comp = {'outer': 884 * v, 'idles': -576 * v, 'thin': -3 * v, 'X mains': -832 * L, 'Y mains': -832 * L, 'owned': -c * L} +ok(comp['outer'] == 91936 and comp['idles'] == -59904 and comp['X mains'] == -14976 and comp['owned'] == -1008, + 'component arithmetic on STATED numbers (not read from a pricing file): 91936, -59904, -312, -14976, -14976, -1008') +ok(sum(comp.values()) == 760, 'sum of the stated components = 760 (arithmetic on stated numbers)') +ok(v * (L - 1) - L * c == 760 == 104 * 17 - 18 * 56, 'closed form S = v(L-1) - L c = 104*17 - 18*56 = 760') +thin = 3 +ok(n_ - thin == L - 1 and Fr(n_) - thin - Fr(L * c, v) == Fr(760, v), 'per port: S/v = n - thin - Lc/v = 20 - 3 - 9.692 = 7.3077 = 760/104') +ok(thin == (n_ + 1) - L and (n_ + 1) == 21, 'thin = N - hosted = (n+1) - L = 21 - 18 = 3 (N = n+1 is the ratio-lemma floor)') +ok(comp['thin'] * -1 * 100 // 760 == 41 and Fr(v, 760) > Fr(13, 100), 'thin = 312 = 41% of S; one extra thin unit = 104 = 13.7% of S') + +def S_bound(v, L, c, h=1): return v * (h * L - 1) - L * c +def S_of(r, thin_, v, L, c): return v * (r - thin_) - L * c # H6 identity per uniform port set +# sweep: for every credited-field count r and every legal thin >= max(0, 1 + r - hL), S <= v(L-1)-Lc ; equality iff r>=L-1 and thin = 1+r-L +bad = 0; eq = [] +for r in range(0, 81): + for th in range(max(0, 1 + r - L), 1 + r - L + 25 if 1 + r - L > 0 else 25): + s = S_of(r, th, v, L, c) + if s > S_bound(v, L, c): bad += 1 + if s == S_bound(v, L, c): eq.append((r, th)) +ok(bad == 0, 'sweep r=0..80, all thin >= max(0,1+r-L): S <= v(L-1) - Lc (no counterexample; target size r drops out)') +ok(all(th == max(0, 1 + r - L) for r, th in eq) and (20, 3) in eq and min(r for r, _ in eq) == L - 1, f'equality set: thin = 1+r-L (or 0 at r=L-1), starts at r=L-1={L-1}; (r,thin)=(20,3) is the reference record') +ok(all(S_of(r, max(0, 1 + r - L), v, L, c) == v * min(r, L - 1) - L * c for r in range(0, 60)), 'S/v = min(r, L-1) - Lc/v at the lemma floor') +# other port sets (Gram-class c values as stated; listed for comparison) +ok((S_bound(104, 18, 56), S_bound(112, 18, 64), S_bound(120, 18, 72)) == (760, 752, 744), + 'port sets: P104 760, P112 752, P120 744 (c = 56/64/72 as stated)') +# non-uniform ports: S <= sum_p (L_p - 1) - sum_j c_j (per-port lemma, per-call owned) +Lp = [9] * 52 + [18] * 52; cj = [56] * 18 +ok(sum(l - 1 for l in Lp) - sum(cj) == 52 * 8 + 52 * 17 - 1008, 'non-uniform ports: bound sum_p (L_p - 1) - sum_j c_j (uniformity not needed)') +# hosting hypothesis made explicit: what h=2 (M1, owned-UP rows) would change +ok(S_bound(104, 18, 56, 2) == 104 * 35 - 1008 == 2632, 'if h=2 (two hosted Q-odd per LOCAL = M1) the bound would be 2632: the hosting hypothesis H8 is the load-bearing one') +# lambda sensitivity of c: each unit of c is 18 S = 2.37% +ok(Fr(18, 760) == Fr(9, 380) and abs(float(Fr(18, 760)) - 0.0237) < 1e-4, '1 unit of c = L = 18 S = 2.37% of S') + +print() +if FAILS: + print('SURPLUS CHECK FAIL:', len(FAILS), 'failures'); sys.exit(1) +print('SURPLUS CHECK PASS') diff --git a/research/p104-surplus-hub-form-note/checks/typed_query.py b/research/p104-surplus-hub-form-note/checks/typed_query.py new file mode 100644 index 0000000000..7b5f334b8b --- /dev/null +++ b/research/p104-surplus-hub-form-note/checks/typed_query.py @@ -0,0 +1,151 @@ +"""Typed-query exact checks over the Gaussian rationals Q(i) (standard library only: fractions). +Run: python3.12 -I -B typed_query.py +H = H0/sqrt2 with H0 = [[1,1],[1,-1]]. Every identity below involves H only through H(x)H = (H0(x)H0)/2 or +H S H = (H0 S H0)/2, so no square root is needed and all arithmetic is exact.""" +import itertools +from fractions import Fraction as Fr + +class G: + """Gaussian rational a + b i, exact.""" + __slots__ = ('a', 'b') + def __init__(s, a=0, b=0): s.a = Fr(a); s.b = Fr(b) + def __add__(s, o): o = g(o); return G(s.a + o.a, s.b + o.b) + __radd__ = __add__ + def __sub__(s, o): o = g(o); return G(s.a - o.a, s.b - o.b) + def __rsub__(s, o): return g(o) - s + def __neg__(s): return G(-s.a, -s.b) + def __mul__(s, o): o = g(o); return G(s.a*o.a - s.b*o.b, s.a*o.b + s.b*o.a) + __rmul__ = __mul__ + def __truediv__(s, o): + o = g(o); d = o.a*o.a + o.b*o.b + return s * G(o.a/d, -o.b/d) + def __rtruediv__(s, o): return g(o) / s + def conj(s): return G(s.a, -s.b) + def __eq__(s, o): o = g(o); return s.a == o.a and s.b == o.b + def __hash__(s): return hash((s.a, s.b)) + def __repr__(s): + if s.b == 0: return str(s.a) + if s.a == 0: return f'{s.b}i' + return f'({s.a}+{s.b}i)' +def g(x): return x if isinstance(x, G) else G(x) +I = G(0, 1); ONE = G(1); ZERO = G(0) + +def M(rows): return [[g(x) for x in r] for r in rows] +def mm(A, B): + Bt = list(zip(*B)); return [[sum((a*b for a, b in zip(r, c)), ZERO) for c in Bt] for r in A] +def madd(A, B): return [[a + b for a, b in zip(r, s)] for r, s in zip(A, B)] +def msub(A, B): return [[a - b for a, b in zip(r, s)] for r, s in zip(A, B)] +def sc(c, A): return [[g(c)*a for a in r] for r in A] +def eye(n): return [[ONE if i == j else ZERO for j in range(n)] for i in range(n)] +def zeros(r, c): return [[ZERO]*c for _ in range(r)] +def kp(A, B): + return [[A[i][j]*B[k][l] for j in range(len(A[0])) for l in range(len(B[0]))] for i in range(len(A)) for k in range(len(B))] +def dag(A): return [[A[j][i].conj() for j in range(len(A))] for i in range(len(A[0]))] +def is0(A): return all(x == ZERO for r in A for x in r) +def diag(*d): n = len(d); return [[g(d[i]) if i == j else ZERO for j in range(n)] for i in range(n)] +def minv(A): + n = len(A); W = [A[i][:] + eye(n)[i] for i in range(n)] + for c in range(n): + p = next(r for r in range(c, n) if W[r][c] != ZERO); W[c], W[p] = W[p], W[c] + pv = W[c][c]; W[c] = [x/pv for x in W[c]] + for r in range(n): + if r != c and W[r][c] != ZERO: + f = W[r][c]; W[r] = [x - f*y for x, y in zip(W[r], W[c])] + return [r[n:] for r in W] + +H0 = M([[1, 1], [1, -1]]); S = diag(1, I); X = M([[0, 1], [1, 0]]); Z = diag(1, -1); I2 = eye(2) +a = (1 + I)/2; b = (1 - I)/2 +C = sc(Fr(1, 2), mm(mm(H0, S), H0)) # H S H +aIbX = madd(sc(a, I2), sc(b, X)) +print("1. C=HSH == aI+bX:", is0(msub(C, aIbX)), "| C^2==X:", is0(msub(mm(C, C), X)), "| b/a =", b/a) + +def mpow(P, k): return P if k else eye(len(P)) +PH = (ONE, I, -ONE, -I) +def pauli_n(Mx, n): + for xs in itertools.product((0, 1), repeat=n): + for zs in itertools.product((0, 1), repeat=n): + P = M([[1]]) + for q in range(n): P = kp(P, mm(mpow(X, xs[q]), mpow(Z, zs[q]))) + for ph in PH: + if is0(msub(Mx, sc(ph, P))): return xs + zs + return None +def symp(U, n): + cols = []; Ui = minv(U) + for kind in ('x', 'z'): + for q in range(n): + P = M([[1]]) + for r in range(n): P = kp(P, X if (kind == 'x' and r == q) else Z if (kind == 'z' and r == q) else I2) + cols.append(pauli_n(mm(mm(U, P), Ui), n)) + return [list(r) for r in zip(*cols)] # 2n x 2n, columns = images of x_1..x_n, z_1..z_n +def rankF2(Mx): + Mx = [[int(v) % 2 for v in row] for row in Mx]; r = 0; rows = len(Mx); cols = len(Mx[0]) if Mx else 0 + for c in range(cols): + p = next((i for i in range(r, rows) if Mx[i][c]), None) + if p is None: continue + Mx[r], Mx[p] = Mx[p], Mx[r] + for i in range(rows): + if i != r and Mx[i][c]: Mx[i] = [(u + v) % 2 for u, v in zip(Mx[i], Mx[r])] + r += 1 + return r +def Bblock(Sy, n): return [row[n:] for row in Sy[:n]] +S1 = symp(C, 1); print(" symplectic of C:", S1, " B-block rank_F2 =", rankF2(Bblock(S1, 1))) + +# free group F: monomial matrices with entries in {1,i,-1,-i}, 1 qubit +F1 = [] +for perm in itertools.permutations(range(2)): + for p in itertools.product(PH, repeat=2): + Mx = zeros(2, 2) + for r in range(2): Mx[r][perm[r]] = p[r] + F1.append(Mx) +print(" |F_1| =", len(F1)) +def prop(A, B): + for i in range(len(A)): + for j in range(len(A[0])): + if B[i][j] != ZERO: + lam = A[i][j]/B[i][j]; return is0(msub(A, sc(lam, B))) and lam != ZERO + return False +inF = any(prop(C, f) for f in F1) +cell = any(prop(C, mm(mm(f1, H0), f2)) for f1 in F1 for f2 in F1) +print("1a. C in F (free)?", inF, "| C in F*H*F (one H-cell, C-rank 1)?", cell) + +# field Bruhat (non-unitary): C = U(t1) W U(t2), U(t) = [[1,t],[0,1]], W antidiagonal [[0,w1],[w2,0]] +# U(t1) W U(t2) = [[w2 t1, w1 + t1 w2 t2],[w2, w2 t2]]: the four entries of C determine (t1,t2,w1,w2) uniquely. +Uu = lambda t: M([[1, t], [0, 1]]) +w2 = C[1][0]; t2 = C[1][1]/w2; t1 = C[0][0]/w2; w1 = C[0][1] - t1*w2*t2 +Wn = M([[0, w1], [w2, 0]]) +chk = is0(msub(mm(mm(Uu(t1), Wn), Uu(t2)), C)) +print("1b. field-Bruhat C = U(t1) W U(t2), W antidiagonal: t1 =", t1, "t2 =", t2, "w1 =", w1, "w2 =", w2) +print(" check:", chk, "| U(t) unitary?", is0(msub(mm(dag(Uu(t1)), Uu(t1)), I2)), + "| W monomial with non-unit entry:", Wn, + "(shears have CONSTANT Gaussian coefficient t=i: Q-independent, non-Clifford, outside F and outside the symplectic lemma)") + +# 2. K_P +H4 = sc(Fr(1, 2), kp(H0, H0)) # H (x) H +CZ = diag(1, 1, 1, -1); SW = M([[1, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 0], [0, 0, 0, 1]]) +X1 = kp(X, I2); X2 = kp(I2, X) +KP = sc(Fr(1, 2), msub(madd(madd(eye(4), X1), X2), mm(X1, X2))) +print("2. K_P == H(x)H diag((-1)^(x1x2)) H(x)H :", is0(msub(KP, mm(mm(H4, CZ), H4)))) +print(" (H(x)H, normalised H=[[1,1],[1,-1]]/sqrt2) == CZ K_P CZ SWAP :", is0(msub(H4, mm(mm(mm(CZ, KP), CZ), SW))), + " [(H(x)H) here uses the sqrt2-normalised H; the unnormalised version differs by a factor 1/2 only]") +S2K = symp(KP, 2); S2C = symp(kp(C, C), 2); S2CI = symp(kp(C, I2), 2) +print(" rank_F2 B: K_P =", rankF2(Bblock(S2K, 2)), "| C(x)C =", rankF2(Bblock(S2C, 2)), "| C(x)I =", rankF2(Bblock(S2CI, 2))) +nz = lambda A: [sum(1 for v in r if v != ZERO) for r in A] +print(" nonzeros per row: K_P", nz(KP), "| C(x)I", nz(kp(C, I2)), "-> K_P not in F*(C(x)I)*F (monomial maps preserve row support sizes)") +CC = kp(C, C) +def same_cell(A, B): + for pr in itertools.permutations(range(4)): + for pc in itertools.permutations(range(4)): + Bp = [[B[pr[i]][pc[j]] for j in range(4)] for i in range(4)] + if any((A[i][j] == ZERO) != (Bp[i][j] == ZERO) for i in range(4) for j in range(4)): continue + Rr = [[A[i][j]/Bp[i][j] if Bp[i][j] != ZERO else ZERO for j in range(4)] for i in range(4)] + base = Rr[0][0]; ok = True + for i in range(4): + for j in range(4): + if Rr[i][j] == ZERO: continue + pred = Rr[i][0]*Rr[0][j]/base + if Rr[i][j] != pred: ok = False; break + if (Rr[i][0]/base) not in PH: ok = False; break + if not ok: break + if ok and all((Rr[0][j]/base) in PH for j in range(4)): return True + return False +print(" K_P in F*(C(x)C)*F (same Bruhat cell, rank 2)?", same_cell(KP, CC), " -> K_P = a rank-2 plane job; NO rank drop vs C(x)C") diff --git a/research/p104-surplus-hub-form-note/data/quotes.json b/research/p104-surplus-hub-form-note/data/quotes.json new file mode 100644 index 0000000000..0b116f9439 --- /dev/null +++ b/research/p104-surplus-hub-form-note/data/quotes.json @@ -0,0 +1,99 @@ +{ + "pkg": [ + [ + "research/p104-helper470-twin-rung-removal/pricing.py", + 48, + "elif e[0] == 'QUERY_SHEAR':" + ], + [ + "research/p104-helper470-twin-rung-removal/pricing.py", + 49, + "paid[1] += 104" + ], + [ + "research/p104-helper470-twin-rung-removal/pricing.py", + 62, + "counts['LOCAL'] == 18 and counts['QUERY_SHEAR'] == counts['IDLE'] == 15" + ], + [ + "research/p104-helper470-twin-rung-removal/pricing.py", + 75, + "== 760, 'Complete rank surplus'" + ], + [ + "research/p104-productive-controller/PROOF.md", + 31, + "Y_r -> Y_r + X_r" + ], + [ + "research/p104-productive-controller/PROOF.md", + 57, + "All public paths are nested." + ], + [ + "research/p104-productive-controller/PROOF.md", + 119, + "retains Q as a formal invertible variable" + ], + [ + "research/p104-productive-controller/local.py", + 126, + "'Nested chronological transport'" + ], + [ + "research/p104-productive-controller/local.py", + 171, + "'Independent productive inputs'" + ], + [ + "research/p104-productive-controller/local.py", + 229, + "need(recipe['rank'] == abs(len(w['frames'][a])-len(w['frames'][b])), 'Native boundary rank')" + ], + [ + "research/p104-productive-controller/local.py", + 242, + "'Literal central port'" + ], + [ + "research/p104-productive-controller/local.py", + 243, + "'Literal output hyperplane'" + ], + [ + "notes/general-clifford-frames.tex", + 16, + "$d(L(S),L(T))$, where $d(L,L')=h-\\dim(L\\cap L')$." + ], + [ + "notes/general-clifford-frames.tex", + 27, + "d(L_U,L_V)=\\dim U+\\dim V-2\\dim(U\\cap V)" + ], + [ + "notes/general-clifford-frames.tex", + 62, + "At every common scalar gate use one identical exact representative on all" + ], + [ + "research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md", + 139, + "small rank use the ordinary sequential program: `B_e=1`, `P_e=e`." + ], + [ + "research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md", + 169, + "Induction removes all recursive calls: the only remaining paid children" + ], + [ + "upstream/build/sections/05-layers.tex", + 431, + "step is the entire algorithm." + ], + [ + "upstream/build/sections/05-layers.tex", + 640, + "Stop recursion when" + ] + ] +} \ No newline at end of file diff --git a/research/p104-surplus-hub-form-note/data/selected_record_profile.json b/research/p104-surplus-hub-form-note/data/selected_record_profile.json new file mode 100644 index 0000000000..0ccf20b0de --- /dev/null +++ b/research/p104-surplus-hub-form-note/data/selected_record_profile.json @@ -0,0 +1,45 @@ +{ + "full_forward_calls": 18, + "paid": { + "1": 41502, + "16": 416, + "2": 8226, + "24": 416, + "3": 8928, + "32": 416, + "4": 1800, + "40": 416, + "48": 416, + "5": 2934, + "56": 416, + "6": 198, + "64": 416, + "7": 108, + "72": 208, + "8": 18 + }, + "paid_calls": 66834, + "productive_fields": 13444, + "query_shears": 15, + "rank_mass_surplus": 760, + "targets": { + "1": 252, + "145": 208, + "17": 416, + "2": 144, + "25": 416, + "3": 72, + "33": 416, + "4": 1926, + "41": 416, + "49": 416, + "5": 252, + "57": 416, + "6": 36, + "65": 416, + "7": 162, + "73": 208, + "8": 342, + "9": 6930 + } +} \ No newline at end of file diff --git a/research/p104-surplus-hub-form-note/verify.sh b/research/p104-surplus-hub-form-note/verify.sh new file mode 100755 index 0000000000..c2e52bd776 --- /dev/null +++ b/research/p104-surplus-hub-form-note/verify.sh @@ -0,0 +1,4 @@ +#!/bin/sh +# Runs the exact checks; run from anywhere. Needs python3.12 and numpy (pinned in VERIFY.json). +set -e +exec python3.12 -I -B "$(dirname "$0")/check.py"