From 936a8a19896a56afbf428da6f7c29c175f348935 Mon Sep 17 00:00:00 2001 From: DreamingOfClouds Date: Sun, 8 Nov 2026 17:54:27 -0600 Subject: [PATCH] Root-word duality, Gram-class floor for 16 to 24 deleted lines, flag-chain flattening and exact frame facts (no kappa) Co-Authored-By: Claude Opus 5.5 --- .../p104-duality-ceiling-flag-note/LICENSE | 201 ++++++++++++++++++ .../p104-duality-ceiling-flag-note/NOTICE | 4 + .../p104-duality-ceiling-flag-note/README.md | 34 +++ .../SOURCES.json | 36 ++++ .../p104-duality-ceiling-flag-note/TASK.json | 144 +++++++++++++ .../p104-duality-ceiling-flag-note/THEOREM.md | 115 ++++++++++ .../VERIFY.json | 24 +++ .../p104-duality-ceiling-flag-note/check.py | 43 ++++ .../checks/a2.py | 80 +++++++ .../checks/caps.py | 75 +++++++ .../checks/duality.py | 196 +++++++++++++++++ .../checks/e8lib.py | 107 ++++++++++ .../checks/flatten.py | 77 +++++++ .../checks/lagr.py | 108 ++++++++++ .../checks/omega_floor.py | 142 +++++++++++++ .../checks/schur_leak.py | 100 +++++++++ .../data/p104_pairs.json | 1 + .../data/quotes.json | 49 +++++ .../p104-duality-ceiling-flag-note/verify.sh | 4 + 19 files changed, 1540 insertions(+) create mode 100644 research/p104-duality-ceiling-flag-note/LICENSE create mode 100644 research/p104-duality-ceiling-flag-note/NOTICE create mode 100644 research/p104-duality-ceiling-flag-note/README.md create mode 100644 research/p104-duality-ceiling-flag-note/SOURCES.json create mode 100644 research/p104-duality-ceiling-flag-note/TASK.json create mode 100644 research/p104-duality-ceiling-flag-note/THEOREM.md create mode 100644 research/p104-duality-ceiling-flag-note/VERIFY.json create mode 100644 research/p104-duality-ceiling-flag-note/check.py create mode 100644 research/p104-duality-ceiling-flag-note/checks/a2.py create mode 100644 research/p104-duality-ceiling-flag-note/checks/caps.py create mode 100644 research/p104-duality-ceiling-flag-note/checks/duality.py create mode 100644 research/p104-duality-ceiling-flag-note/checks/e8lib.py create mode 100644 research/p104-duality-ceiling-flag-note/checks/flatten.py create mode 100644 research/p104-duality-ceiling-flag-note/checks/lagr.py create mode 100644 research/p104-duality-ceiling-flag-note/checks/omega_floor.py create mode 100644 research/p104-duality-ceiling-flag-note/checks/schur_leak.py create mode 100644 research/p104-duality-ceiling-flag-note/data/p104_pairs.json create mode 100644 research/p104-duality-ceiling-flag-note/data/quotes.json create mode 100755 research/p104-duality-ceiling-flag-note/verify.sh diff --git a/research/p104-duality-ceiling-flag-note/LICENSE b/research/p104-duality-ceiling-flag-note/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/p104-duality-ceiling-flag-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-duality-ceiling-flag-note/NOTICE b/research/p104-duality-ceiling-flag-note/NOTICE new file mode 100644 index 0000000000..73b7b5388b --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/NOTICE @@ -0,0 +1,4 @@ +Root-word duality, Gram-class floor, flag-chain flattening and exact frame facts for the P104 setting: 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. Standard library only. diff --git a/research/p104-duality-ceiling-flag-note/README.md b/research/p104-duality-ceiling-flag-note/README.md new file mode 100644 index 0000000000..d5fe91d991 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/README.md @@ -0,0 +1,34 @@ +# Root-word duality, Gram-class floor for 16 to 24 deleted lines, flag-chain flattening and exact frame facts for the P104 setting (no kappa) + +**No new kappa.** No word is built and nothing is priced. This package states seven results about the E8 line model behind the P104 caller, each with its hypotheses and a check. 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 with its missing premise. A verifier or package restriction is never called a law: the labels are SPEC (outer framework or paper, quoted with file and line and checked), package convention, verifier behaviour, derived, family assumption. + +## Results + +1. **Theorem G, duality [P+C].** N isotropic transvections in dimension n with product -I correspond, on gauge classes, to N reflections in dimension rho = N - n with product -I (characteristic not 2). Both directions are checked exactly on reduced words of w_0 for D4, B3, F4, I2(4), I2(6) and on random rho = 2 words. The real-window law for three hosted pairs, which rests on citations not checkable here, is not included. +2. **Theorem O, Gram-class floor [P+C].** For any set D of 16 to 24 deleted lines and any Gram-class design (any number of terms, any invertible M), the owned cost is at least 56; so v - c <= 64 - |D| <= 48, with equality at |D| = 16 attained by an explicit design (c = 56, every term price 7). The proof is Cauchy-Binet plus a Sylvester rank bound plus a domination lemma plus a computed census (cost of making a codimension-2 drop is at least 25 on all eight ray types). It does not cover |D| <= 15 or |D| >= 25, carriers outside col(E), or other line systems. +3. **Theorem F, flattening [P+C].** A chain of nested frames equals, on the mask N, one rank-one term, at price at most the chain's frame-dimension change. Corollary F2 (CONDITIONAL on the word being a disjoint union of such chains whose flattened terms form a Gram-class design) transfers the floor 56. +4. **A2 toy [P + C].** The naive transfer "any N-diagonal rank-one decomposition costs at least the Gram value" is false: Gram value 4, identity decoder 3 on A2. +5. **Theorems I and R [P+C for h <= 4].** Subspace frames are exactly the Lagrangians on a geodesic from L_0 to L_F, and rho(L) = L_{pi_1 L} is a retraction that does not increase adjacency distance. Network reading CONDITIONAL on two stated Clifford premises. +6. **Exact tile caps [C].** On the 104-line port set of the package data, over all subspaces: maximum area 32, 32 and 36 for (dim A, dim B) = (2,3), (3,4), (4,5). +7. **Schur law and leak identity [P+C].** An exact complement formula for the public inverse of a map with owned lifetimes, and the per-register identity L_X L_Y = r f. + +## Scope and what is not claimed + +No bound on kappa; nothing about the denominator; Theorem O is about the scalar Gram model with F2 mask-rank price, not about any particular word's owned layer; Corollary F2 and the network reading of Theorem R are conditional as stated; the tile caps are counting facts and no claim is made that geodesic tiles reduce to linear tiles. No word from any pull request is replayed or checked here. + +## Exact checks + +`python3.12 -I -B research/p104-duality-ceiling-flag-note/check.py` from the repository root (or `verify.sh` from anywhere). About 30 s. Standard library only, no dependencies. The quote checks read four repository files named in `data/quotes.json` (9 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_DUALITY_CEILING_FLAG_NOTE`. + +## Open next questions + +1. Can the floor of Theorem O be proved for 25 or more deleted lines, and for 15 or fewer, in the Gram class? +2. Is a given word's owned layer a disjoint union of flag chains with Gram-class flattened terms, so that Corollary F2 applies? +3. Do the floors survive owned networks that are not flag chains (forks with later reads or writes, relays, owned ascent)? +4. Does the retraction of Theorem R extend to helpers with non-family endpoints, and do geodesic tiles reduce to linear tiles? + +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-duality-ceiling-flag-note/SOURCES.json b/research/p104-duality-ceiling-flag-note/SOURCES.json new file mode 100644 index 0000000000..649347d943 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "notes/general-clifford-frames.tex", + "usage": "input", + "git_blob": "0367eeb005298601f28a673861d6f71bf1d0ebbb", + "sha256": "c9bb9655b594583c6b4bab8cb485233f1d1e588f83858cf1e4c3530cee8fed54" + }, + { + "path": "upstream/build/sections/03-motifs.tex", + "usage": "input", + "git_blob": "cdb0ba527aa8df5d57c151183fd3893c1a7e21ab", + "sha256": "ed76761194988a01af77ead0ea6469cb5dcd29690ab985a0b5a4006b0f2b69bb" + }, + { + "path": "upstream/build/sections/04-swap.tex", + "usage": "input", + "git_blob": "951e792b1768e6509561380b8bbfb1d1ccb64c08", + "sha256": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906" + }, + { + "path": "upstream/build/sections/05-layers.tex", + "usage": "input", + "git_blob": "5ce8b3c83c455f221bb84858a97230b0285644aa", + "sha256": "20cfc8d12099d4e4ed9e3e7eeb6162edd9b6e0e076f24693364cd24377252594" + } + ] +} \ No newline at end of file diff --git a/research/p104-duality-ceiling-flag-note/TASK.json b/research/p104-duality-ceiling-flag-note/TASK.json new file mode 100644 index 0000000000..c23a4d1099 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/TASK.json @@ -0,0 +1,144 @@ +{ + "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 E8 line model behind the P104 caller, with a stated hypothesis ledger: a duality between isotropic transvection words and reflection words with product -I (Theorem G); a Gram-class floor c >= 56 for 16 to 24 deleted lines with the exact equality design (Theorem O); flattening of nested-frame chains onto the mask with a conditional transfer of the floor (Theorem F, Corollary F2); an A2 toy showing the naive transfer fails; the subspace frames as the geodesic interval of Lagrangian frames and a 1-Lipschitz retraction onto them (Theorems I and R, exhaustive for h <= 4); exact tile caps over all subspaces for one 104-line port set; and the Schur law and leak identity for owned lifetimes. 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 results about the owned layer, the frame family and the root-word algebra, each with its hypotheses, and keeps every open door at a named hypothesis.", + "bottleneck_link": "docs/research/research-family-status.md; the statements constrain the owned-layer floor, the frame family and the helper-form algebra of any word in the stated model. They say nothing about the denominator or about kappa.", + "stop_rule": "No kappa claim and no new word. Open and stated: the Gram-class floor for 25 or more and 15 or fewer deleted lines; carriers outside col(E); owned networks that are not flag chains (forks with later reads or writes, relays, owned ascent); the network reading of the retraction (two Clifford premises); geodesic tiles versus linear tiles; word-level membership in the flag-chain class.", + "evidence": "README.md and THEOREM.md (statements, proofs, hypothesis ledger), check.py with checks/ (exact rational and integer certificates, standard library only) and data/ (quoted-line table, one 16-line pair system).", + "author": "DreamingOfClouds", + "ai_assistance": "Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code.", + "outcome": "completed", + "open_questions": [ + { + "question": "Can the Gram-class floor of Theorem O be proved for 25 or more deleted lines, and for 15 or fewer?", + "why_it_matters": "Theorem O covers 16 to 24 deleted lines, which contains the P104 port set; other port sets need the same floor to compare gains.", + "first_step": "For 25 or more, count how many independent tops can have codimension at least 2 at once (joint star counts); for 15 or fewer, use the per-term level law with the end-line saving.", + "blocked_by": "Joint counts of high-codimension stars are not part of this package, and the argument for 15 or fewer needs biorthogonality that general invertible M does not give." + }, + { + "question": "Is a given word's owned layer a disjoint union of flag chains whose flattened terms form a Gram-class design?", + "why_it_matters": "Corollary F2 transfers the floor 56 only under that membership.", + "first_step": "Extract the owned chains of one shipped word, check nesting of frames, flatten, and compare the flattened terms with a Gram-class design up to a sign gauge.", + "blocked_by": "No word is replayed in this package." + }, + { + "question": "Do the floors survive owned networks that are not flag chains?", + "why_it_matters": "Forks with later reads or writes and relays can compute a rank-two object with shared trunk mass, so the rank-one cost model may overprice them.", + "first_step": "State the weakest network class for which Theorem F's read-before-write argument still gives a flattening, then test a fork instance exactly.", + "blocked_by": "Theorem F uses that levels are non-decreasing in time; ascent breaks it (control in section 3 of THEOREM.md)." + }, + { + "question": "Does the retraction of Theorem R extend to helpers with non-family endpoints, and do geodesic tiles reduce to linear tiles?", + "why_it_matters": "The network reading of Theorem R and the tile caps only matter if no cheaper non-subspace frame or tile exists.", + "first_step": "Check helper step patterns with two or more family contact stops at h = 4 for a family replacement with the same steps, and prove the reduction of an additive-step tile to a linear tile.", + "blocked_by": "Exhaustive checks stop at h = 4, and the tile reduction needs the equality case of a rectangle bound on Hadamard matrices, not proved here." + } + ], + "research_context": { + "sources": [ + "notes/general-clifford-frames.tex (frame labels, Fourier rank d(L,L'))", + "upstream/build/sections/03-motifs.tex (frames, labels)", + "upstream/build/sections/04-swap.tex (rank_Q interchange contract)", + "upstream/build/sections/05-layers.tex (directional kernels)" + ], + "credit": "DreamingOfClouds." + }, + "selected_frontier_changed": false +} \ No newline at end of file diff --git a/research/p104-duality-ceiling-flag-note/THEOREM.md b/research/p104-duality-ceiling-flag-note/THEOREM.md new file mode 100644 index 0000000000..90d1e224b6 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/THEOREM.md @@ -0,0 +1,115 @@ +# Proof note: a root-word duality, a Gram-class floor for 16 to 24 deleted lines, flag-chain flattening, and exact frame and tile facts (no kappa) + +Every claim carries one of: **[C]** exact computation reproduced by `check.py` (a PASS line per claim); **[P]** hand proof, re-derived line by line for this package; **[P+C]** both; **CONDITIONAL** (stated with its missing premise, not proved 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 (quoted with file and line, checked by `check.py`); **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. + +## 0. Quoted premises (checked against the repository by `check.py`, group Q) + +| id | text | file:line | label | +|---|---|---|---| +| S1 | "its Fourier rank is d(L(S),L(T)), where d(L,L')=h-dim(L cap L')" | `notes/general-clifford-frames.tex:16` | SPEC (Clifford-frame family) | +| S2 | d(L_U,L_V)=dim U+dim V-2dim(U cap V) for subspace frames | `notes/general-clifford-frames.tex:27` | SPEC (Clifford-frame family) | +| S3 | "For U subset V, the exact transition T_V T_U^-1 has rank dim V - dim U" | `notes/general-clifford-frames.tex:67-68` | SPEC (Clifford-frame family) | +| S4 | "use one identical exact representative" at a common scalar gate | `notes/general-clifford-frames.tex:62` | package convention (not SPEC) | +| S5 | "assign an invertible R-linear operator ... called its frame" | `upstream/build/sections/03-motifs.tex:154` | SPEC | +| S6 | "A label is a nondegenerate subspace of a fixed bilinear space" | `upstream/build/sections/03-motifs.tex:203` | SPEC for the labelled construction; a choice of that construction | +| S7 | A_e = M_head(e) - M_tail(e), price rank_Q A_e | `upstream/build/sections/04-swap.tex:115`, `:197` | SPEC for the rational-matrix interchange contract only | +| S8 | "The number of directional kernels is precisely rho_edge" | `upstream/build/sections/05-layers.tex:82` | SPEC | + +Consequence for pricing (derived from S1 and S7): the price used below, the F2 rank of the mask pairing, is the Clifford-frame family's Fourier-rank price. It is not the rank_Q price of S7, which belongs to the interchange contract. Nothing in this note uses rank_Q. + +## 1. Theorem G: duality between isotropic transvection words and reflection words [P+C] + +**Setting.** Work over a field of characteristic not 2 (checks: Q). A transvection is T = I - 2 x y^T with y^T x = 0 (isotropic); a reflection is r = I - 2 q p^T with p^T q = 1. For N transvections T_k = I_n - 2 x_k y_k^T put X = [x_1 ... x_N] (n x N), Y with rows y_k (N x n), G = Y X, so G_kl = y_k . x_l and diag G = 0. Let L be the strictly lower triangle of G, K = I + 2L (unit lower triangular, invertible) and Z = K - G = I + L - U, where U is the strictly upper triangle of G. Z has diagonal 1 and Z_ij = G_ij for i > j, Z_ij = -G_ij for i < j. + +**Lemma G0 (product formula) [P+C].** For any vectors, T_N ... T_1 = I - 2 X K^-1 Y, where K = I + 2 L(G) and only the strictly lower triangle of G = YX enters (the diagonal never does). +*Proof.* Induction on N. N = 1: K = 1. Step: write W_m = T_m ... T_1 = I - 2 X_m K_m^-1 Y_m and g = (y_{m+1}.x_1, ..., y_{m+1}.x_m). Then y_{m+1}^T W_m = y_{m+1}^T - 2 g K_m^-1 Y_m, so W_{m+1} = T_{m+1} W_m = I - 2 [X_m x_{m+1}] [[K_m^-1, 0], [-2 g K_m^-1, 1]] [Y_m; y_{m+1}^T], and the middle matrix is the inverse of K_{m+1} = [[K_m, 0], [2g, 1]]. QED + +**Theorem G.** Let N = n + rho. (a) If T_N ... T_1 = -I_n with every T_k isotropic, then rank Z = rho, and any rank factorisation Z = P Q^T (P, Q of size N x rho, rows p_i, q_j) gives p_i . q_i = 1 and reflections r_i = I_rho - 2 q_i p_i^T with r_N ... r_1 = -I_rho. (b) Conversely, reflections r_i = I_rho - 2 q_i p_i^T (p_i . q_i = 1) with r_N ... r_1 = -I_rho, put Z = P Q^T, define G by diag 0, G_ij = Z_ij (i > j), G_ij = -Z_ij (i < j). Then rank G = N - rho = n, and any rank factorisation G = Y X gives isotropic transvections with T_N ... T_1 = -I_n. (c) The two assignments are inverse bijections between GL_n-gauge classes of transvection words and GL_rho-gauge classes of reflection words: a class on either side is determined by its matrix G, respectively Z, and G and Z determine each other. + +*Proof.* (a) By Lemma G0, the product is -I iff X K^-1 Y = I_n. Then E := K^-1 G = (K^-1 Y) X satisfies E^2 = K^-1 Y (X K^-1 Y) X = E, and K^-1 Y, X have rank n, so rank E = n. Hence K^-1 Z = I - E is idempotent of rank N - n = rho, and rank Z = rho. Z_ii = 1 gives p_i . q_i = 1. The reflection word has Gram matrix (p_i . q_j) = Z, whose strictly lower triangle equals that of G, so Lemma G0 (diagonal never enters) gives r_N ... r_1 = I - 2 Q^T K^-1 P with the same K. Now A := K^-1 P (rank rho, left-invertible) and B := Q^T (right-invertible) satisfy A B A B = A B (idempotence of K^-1 Z = A B), hence B A = I_rho, i.e. Q^T K^-1 P = I_rho and r_N ... r_1 = -I_rho. +(b) By Lemma G0 the reflection product is -I iff Q^T K^-1 P = I_rho. This forces rank P = rank Q = rho, so rank Z = rho, and K^-1 Z = (K^-1 P) Q^T is idempotent. Then E := I - K^-1 Z = K^-1 G is idempotent of rank N - rho = n, and rank G = n. For G = Y X (rank factorisation), E^2 = E reads (K^-1 Y)(X K^-1 Y) X = (K^-1 Y) X; cancelling the left-invertible K^-1 Y and the right-invertible X gives X K^-1 Y = I_n, so T_N ... T_1 = -I_n by Lemma G0; y_k . x_k = G_kk = 0. +(c) Gauge changes x -> g x, y^T -> y^T g^-1 fix G, and a rank-n factorisation of G is unique up to GL_n; likewise for Z. The maps G <-> Z are mutually inverse linear bijections between {diag 0} and {diag 1}. QED + +**Checks [C]** (`checks/duality.py`, exact rationals): both directions and the product -I on the reduced words of w_0 for D4 (N = 12, rho = 4, n = 8), B3 (9, 3, 6), F4 (24, 4, 20), I2(4) and I2(6) (rho = 2), and on random rho = 2 words with N = 6, 8, 10, 12 (closed by solving for the last two reflections); a perturbed word fails on both sides. + +**Corrections kept from the independent read.** (i) The idempotent of rank n is E = K^-1 G; it is I - E = K^-1 Z that has rank rho = N - n. (ii) The correspondence is on gauge classes, not on tuples. (iii) K is always invertible; characteristic not 2 enters only through the factor 2 in K. + +**Not claimed.** The dictionary built on Theorem G (moduli count 2(rho-1)(n-1), the real-window law for three hosted pairs, and the Fricke and Margulis citations behind it) is not part of this note: those citations are not checkable inside the package, so the real-window statement is dropped. + +## 2. Theorem O: a Gram-class floor for 16 to 24 deleted lines [P+C] + +**Model (family assumption, definitions).** Lines: the 120 root lines l_p of E8, scaled so that norm is 8 in the checker's coordinates (inner product ip(l_p,l_q) in {0, +-1, +-2} after dividing by 4). Mask: N[p,q] = 1 iff ip(l_p,l_q) is even (orthogonal or equal); rank_F2 N = 9 [C]. Labels: a map p -> label(p) in F2^9 and a nondegenerate symmetric form with N[p,q] = [C: the form <(a,v),(b,w)> = ab + v C w, C the Cartan matrix mod 2]. For a set P = lines minus D (|D| = d) a **Gram-class design** is a family of terms (u_k, w_k), u_k, w_k in C^8 (any number n >= 8 of terms), with M = sum_k u_k w_k^T invertible. Term k has top support S_k = {p in P : l_p . u_k != 0}, bottom support T_k, price rho_k = rank_F2 N[S_k, T_k], and the cost is c = sum_k rho_k. (A decoder O = E M E^T with N o O = I is of this form with M = I up to scale; allowing every invertible M only strengthens the statement.) The F2 rank price is the Clifford-frame family's price (S1, section 0). + +**Theorem O.** For every D with 16 <= |D| <= 24 and every Gram-class design on P = lines minus D, c >= 56. Hence v - c <= (120 - |D|) - 56 = 64 - |D| <= 48, with v = |P|. At |D| = 16 the bound 56 is attained by an explicit design (data/p104_pairs.json), so v - c = 48 there. + +*Proof.* Write a_k = 9 - dim span label(S_k) and b_k likewise for T_k. +1. *Cauchy-Binet [P].* M = U W^T with U, W the 8 x n matrices of the u_k, w_k; det M = sum over 8-subsets K of det U_K det W_K. Since det M != 0, some K has {u_k} and {w_k} both bases of C^8. All prices are nonnegative, so c >= sum_{k in K} rho_k. +2. *Sylvester [P].* N = L G L^T over F2 with L the 120 x 9 label matrix and G the invertible form (labels span F2^9 because rank N = 9). So rho_k = rank(L_S G L_T^T) >= dim span label(S_k) + dim span label(T_k) - 9 = 9 - a_k - b_k. +3. *Domination [P].* Let u != 0 and orth(u) = {p : l_p . u = 0}. Let X be the intersection of the root hyperplanes containing u (a flat of the arrangement, defined over Q, so the complex case is its complexification). The arrangement restricted to X is essential (the intersection of all root hyperplanes is 0), so X contains a ray r, and orth(u) is contained in orth(r), hence T(r) (the lines not orthogonal to r) is contained in T(u). Therefore span label(T(u) minus D) contains span label(T(r) minus D), i.e. a(u; D) <= a(r; D). +4. *Census [C].* W(E8) acts on the lines by isometries, hence preserves N, hence preserves dim span label(S) (it equals rank_F2 N[S, all lines]). Every ray of the arrangement is conjugate to one of the 8 fundamental-weight rays (a vector in the closed chamber lies on a 1-dimensional flat only at an extreme ray). For each of these 8 rays the cost cost_a(r) = |T(r)| - max over codimension-a subspaces W of F2^9 of #{p in T(r) : label(p) in W} is the least number of deleted lines that makes a >= a. [C] The values (|T|, cost_1, cost_2) are (57,1,25), (78,14,42), (83,27,51), (92,28,56), (97,33,61), (98,35,62), (104,40,68), (106,43,70); in particular cost_2 >= 25 for all 8 rays. +5. *Assembly [P].* If |D| <= 24 then a(u; D) <= 1 for every vector u: otherwise step 3 gives a ray r with a(r; D) >= 2, and D would contain at least cost_2(r) >= 25 lines of T(r) (step 4). The same holds for the bottoms. By step 2, rho_k >= 9 - a_k - b_k >= 7, and by step 1, c >= 8 * 7 = 56. With v = 120 - |D|, v - c <= 64 - |D|, which is <= 48 when |D| >= 16. QED + +**Checks [C]** (`checks/omega_floor.py`): rank_F2 N = 9; labels reproduce N on all 14,400 pairs; sum of l l^T = 120 I (tight frame; the per-unit trace constant is 120/8 = 15, not used above); the census table; the design data (16 distinct lines, y_k . z_l = 0 for k != l, y_k . z_k = +-1, dual basis of the y_k proportional to the z_k); c = 56 with every rho_k = 7 on the 104 lines, c = 72 with every rho_k = 9 for the same eight terms on all 120 lines, c = 72 for generic dual bases, c = 64 for an orthoframe on its complement; 231 random designs with 16 <= |D| <= 24 (including D containing the 16 pair lines) satisfy the Cauchy-Binet subset, a <= 1, the Sylvester bound and c >= 56. + +**Scope (what is not claimed).** (i) |D| <= 15: the argument above gives c >= 56 only, which is weaker than 72 - |D|; the bound v - c <= 48 for the P111 and P112 port sets is not claimed. (ii) |D| >= 25: a >= 2 becomes possible (cost_2 = 25) and the bound would need joint counts of the high-codimension stars; those counts are not part of this note. (iii) Carriers outside col(E) (tops or bottoms not of the form E u), other line systems (E7, E6, D_n have different values), plane ports, and any price other than the F2 mask rank. (iv) The theorem is about the Gram model; it says nothing about an actual word whose owned layer is not shown to be a Gram design (see Theorem F and its conditional corollary). (v) Port sets other than subsets of the 120 E8 lines. + +## 3. Theorem F: flag chains flatten onto the mask at no higher price [P+C] + +**Model (family assumption).** Ports have labels in F2^9 with the form of section 2, N[s,p] = . A *flag chain* is a program whose frames descend, F_0 contains F_1 contains ... contains F_m (subspaces of F2^9), with events in this time order: a *read* at level i adds a vector r_i to an accumulator, supported on ports p with label(p) in F_i; a *write* at level j adds the current accumulator, scaled by a vector w_j supported on ports s with label(s) orthogonal to F_j, into s. The price of the chain is the sum of move ranks, which telescopes to dim F_0 - dim F_m (S3 for nested frames). The read and write support rules are the family's pinning rules (ports read inside the frame, written on its orthogonal complement); they are not a SPEC clause. + +**Theorem F.** Let w = sum of all write vectors and r = sum of all read vectors, and let X[s,p] be the coefficient with which p's read reaches s's write. Then N o X = N o (w r^T), and the chain's price dim F_0 - dim F_m is at least rho(supp w, supp r) = rank_F2 N[supp w, supp r]. +*Proof.* Suppose N[s,p] = 1 and p is read at level i, s written at level j, with the read after the write in time. Levels are non-decreasing in time, so i >= j, label(p) in F_i, F_i contained in F_j, and label(s) is orthogonal to F_j, so N[s,p] = = 0, a contradiction. So on N pairs every read precedes every write, X[s,p] = (sum of writes at s)(sum of reads at p) = w(s) r(p). Price: all reads lie in F_0 and all writes in F_m^perp; the pairing of F_m^perp with F_0 under a nondegenerate form has rank dim F_0 - dim(F_0 cap F_m) = dim F_0 - dim F_m. QED + +**Checks [C]** (`checks/flatten.py`, ports = all 120 lines): on 60 random nested chains (depth 1 to 4, reads and writes interleaved) N o X = N o (w r^T) at every N entry (13,376 nonzero entries tested) and the price bound holds; control: with non-nested frames the identity fails on 37 of 60 random programs. + +**Corollary F2 [P, CONDITIONAL on its hypothesis].** Suppose a word is a disjoint union of flag chains whose flattened terms (w_k, r_k), after a diagonal sign gauge on ports (which does not change supports), form a Gram-class design on P = lines minus D with 16 <= |D| <= 24. Then its total price is at least sum_k rho(supp w_k, supp r_k) >= 56 (Theorem O). Every floor proved for rank-one decompositions in the Gram class therefore transfers to such flag networks of any staging depth. Membership of a particular word in this class is not shown here, and non-flag networks (forks with reads or writes after the fork, relays, owned ascent) are outside the corollary. + +## 4. The naive transfer fails at A2 [C + P] + +Statement tested: "if sum_k a_k b_k^T is N-diagonal with nonzero diagonal, then sum_k rho_k is at least the Gram value." On A2 (the three lines e1-e2, e2-e3, e1-e3 in the plane x+y+z = 0; inner products +-1, so N = I_3) a Gram-class design (a_k = E u_k, b_k = E w_k, sum u_k w_k^T = the projector onto the plane) costs at least 4, while the identity decoder O = I_3 (three terms e_p e_p^T, each of price 1) has N o O = I and costs 3. So the statement is false as written, and holds only after padding or restricting the carriers. +*Proof of c_Gram(A2) >= 4 [P with exact checks].* A plane vector is orthogonal to at most one line, so supports have size 2 or 3 and every term has price rho = |S cap T| >= 1; price 1 iff u is orthogonal to a line i and w to a line j != i. Rank 2 needs at least two terms, so total price <= 3 leaves the price multisets (1,1), (1,1,1), (1,2). The first two never sum to the projector (exact linear algebra over all 6 term types, repeats allowed). For (1,2): a price-1 term lambda u w^T leaves a remainder Pi - lambda u w^T of determinant 1 - lambda (w.u) on the plane, which must vanish; the remainder is then u_B w_B^T with u_B proportional to line j and w_B to line i, supports 3 x 3, price 3, never 2. The forced remainder also attains cost 4. [C] `checks/a2.py`. +A4 (c_Gram >= 12 against the identity decoder 10) is not part of this note. + +## 5. Lagrangian frames: the geodesic interval and a 1-Lipschitz retraction [P + C for h <= 4] + +Notation: vectors of F2^h x F2^h are written (x, z); the symplectic form is x.z' + z.x'; L_0 = {(0,z)}, L_F = {(u,u)}; for a subspace U, L_U = {(u, u+v) : u in U, v in U^perp}; d(L,L') = h - dim(L cap L') (S1, S2). + +**Theorem I [P+C].** A Lagrangian L lies on a geodesic from L_0 to L_F, i.e. d(L_0,L) + d(L,L_F) = h, iff L = L_U for a subspace U. Hence the subspace frames are exactly the interval. +*Proof.* If dim(L cap L_0) + dim(L cap L_F) = h, then, because L_0 cap L_F = 0, L = (L cap L_0) + (L cap L_F), say L = {(0,z): z in Z} + {(w,w): w in W}. Isotropy of (0,z) and (w,w) gives z . w = 0, so Z is contained in W^perp, and dimension h gives Z = W^perp, L = L_W. Conversely dim(L_W cap L_0) = h - dim W and dim(L_W cap L_F) = dim W. QED + +**Theorem R [P+C].** rho(L) := L_{pi_1(L)}, with pi_1(L) = {x : (x,z) in L for some z}, is a retraction of all Lagrangians onto {L_U} that does not increase the adjacency distance: for L, L' with dim(L cap L') = h - 1, d(rho L, rho L') <= 1. +*Proof.* Since L is Lagrangian, L cap L_0 = {(0,z) : z in pi_1(L)^perp}, so pi_1(L) is determined by Z = L cap L_0. Let M = L cap L', Z = L cap L_0, Z' = L' cap L_0. If a in Z minus L' and b in Z' minus L existed, then a, b are orthogonal (L_0 isotropic), both orthogonal to M (a in L, b in L'), so M + is isotropic; its dimension exceeds h unless a + b lies in M, which forces b = (a+b) + a in L, a contradiction. So Z is contained in L' (hence in Z') or Z' is contained in L (hence in Z): the two are nested, and as Z' cap L = Z cap L' their dimensions differ by at most 1. With U = pi_1(L), V = pi_1(L') nested of dimensions differing by at most 1, S2 gives d(L_U, L_V) = |dim U - dim V| <= 1. rho fixes every L_U since pi_1(L_U) = U. QED + +**Checks [C]** (`checks/lagr.py`, exhaustive for h = 1, 2, 3, 4): |LG(h)| = 3, 15, 135, 2295; Theorem I; the distance formula S2 on all pairs of subspaces; d equals the graph distance (all sources for h <= 3, two sources for h = 4); pi_1(L) = (L cap L_0)^perp; rho fixes every L_U; zero violations of d(rho L, rho L') <= 1 over all 68,850 ordered adjacent pairs at h = 4. The proofs above are for every h; the checks cover h <= 4. + +**Consequence for networks [CONDITIONAL].** Replace every gate frame by rho of it: terminals in the family are fixed and no edge rank (S1) rises. This reading needs two premises not proved here: every Lagrangian is the label L(T) = T^-1 L_0 of an exact Clifford operator T (S1), and the network's functional identity depends only on its terminal frames (the common-frame identity of S5). The claim "d is the graph distance for every h" is standard for dual polar graphs and is checked for h <= 4. + +**Exact tile caps [C]** (`checks/caps.py`). For the 104 lines left after deleting the 16 lines of data/p104_pairs.json, labels in F2^9, a subspace A of dimension a and B = A + of dimension a + 1, let area(A,B) = #{ports with label in A} x #{ports orthogonal to B}. Over all subspaces (exhaustive; 43,435, 788,035 and 3,309,747 subspaces, equal to the Gaussian binomials) the maximum area is 32 = 2 x 16 for (a, a+1) = (2,3), 32 = 4 x 8 for (3,4), and 36 = 6 x 6 for (4,5). These are counting facts about this port set. That every tile of a geodesic main is dominated by such a linear tile is not claimed here. + +## 6. Owned lifetimes: the Schur law, and the leak identity [P+C] + +**Schur law (linear algebra).** Let T_f be an invertible matrix on cells P + O (rows are output cells, columns input cells), where each owned lifetime i is born at an input cell in O_b and dies at an output cell in O_d, |O_b| = |O_d|. Define the public map by compression, T_pub = T_f[P,P] (owned inputs zero, owned outputs discarded; **package convention**, the stated definition of T_pub). Then T_pub is invertible iff Tinv_f[O_b,O_d] is, and then +Tinv_pub = Tinv_f[P,P] - Tinv_f[P,O_d] Tinv_f[O_b,O_d]^-1 Tinv_f[O_b,P]. +*Proof.* Jacobi's complementary-minor identity gives det T_f[P,P] = det T_f . det Tinv_f[O_b,O_d] up to sign, and the inverse of a block of T_f is the Schur complement of the complementary block of Tinv_f. QED. [C] `checks/schur_leak.py`: exact on 58 random instances and on 22 singular ones. Word-level replays of this law are not part of the package. + +**Leak identity (elementary).** At a cut T = B A and for each register i define the four rank-one terms f_i[y,x'] = B[y,i] A[i,x'], r_i[x,y'] = Ainv[x,i] Binv[i,y'], L_X,i[x,x'] = Ainv[x,i] A[i,x'], L_Y,i[y,y'] = B[y,i] Binv[i,y']. Then sum_i f_i = T[Y,X], sum_i r_i = Tinv[X,Y], sum_i L_X,i = I, sum_i L_Y,i = I, and entrywise +L_X,i[x,x'] L_Y,i[y,y'] = r_i[x,y'] f_i[y,x'] +(a product of the same four numbers). All four terms are invariant under a diagonal rescaling of the registers. Consequence, stated with its scope: if register i carries both a nonzero forward term f_i[y,x'] and a nonzero reverse term r_i[x,y'] on the quadruple (x,x',y,y'), then both of its leak entries L_X,i[x,x'] and L_Y,i[y,y'] are nonzero. It says nothing about cancellation across several registers. [C] `checks/schur_leak.py`: exact on 40 random cuts. + +## 7. Hypothesis ledger + +| item | statement | label | +|---|---|---| +| H-field | characteristic not 2, rational checks | derived (the factor 2 in K) | +| H-F2 | rank_F2 of the mask pairing is the price | SPEC for Clifford frames (S1, S3); package convention for the 120-line mask N | +| H-N | N = even inner product mask on the 120 E8 lines | family assumption (the unit) | +| H-Gram | tops and bottoms in col(E), M invertible | family assumption; Theorem O does not cover carriers outside it | +| H-pin | reads inside the frame, writes on its orthogonal complement | family assumption (pinning rule), not SPEC | +| H-chain | a chain is a disjoint nested flag; edges disjoint between chains | family assumption | +| H-rep | one identical exact representative per gate | package convention (S4), not SPEC | +| H-lab | labels are nondegenerate subspaces | SPEC for the labelled construction; a choice of it (S6) | +| H-Cliff | every Lagrangian is a frame label; common-frame identity | SPEC premises (S1, S5), used only in the conditional reading of Theorem R | +| H-compress | T_pub = T_f[P,P] with owned inputs zero, outputs discarded | package convention | +| H-nested | descent only; ascent breaks Theorem F (control in section 3) | derived (Theorem F proof) | diff --git a/research/p104-duality-ceiling-flag-note/VERIFY.json b/research/p104-duality-ceiling-flag-note/VERIFY.json new file mode 100644 index 0000000000..06bbd1127e --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "notes/general-clifford-frames.tex", + "upstream/build/sections/03-motifs.tex", + "upstream/build/sections/04-swap.tex", + "upstream/build/sections/05-layers.tex" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/check.py" + ], + "timeout_seconds": 300, + "checks": "9 quoted repository lines (Clifford-frame rank and distance formulas, frame and label premises, rank_Q interchange contract, directional kernels); Theorem G both directions on reduced w0 words (D4, B3, F4, I2(4), I2(6)) and random rho = 2 words with a perturbation control; E8 line model (rank_F2 N = 9, labels, tight frame), census of codimension-1 and codimension-2 costs on the eight ray types, exact P104-type design (c = 56), generic and orthoframe controls, and random Gram-class designs against Cauchy-Binet, Sylvester and the a <= 1 bound; flag-chain flattening on random nested chains with a non-nested control; A2 exact toy; Lagrangian Grassmannians h <= 4 (interval, distance formula, retraction); exact tile caps over all subspaces; Schur law and leak identity on exact random instances." + } + ] +} \ No newline at end of file diff --git a/research/p104-duality-ceiling-flag-note/check.py b/research/p104-duality-ceiling-flag-note/check.py new file mode 100644 index 0000000000..f4117623b2 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/check.py @@ -0,0 +1,43 @@ +#!/usr/bin/env python3 +"""Single driver: one PASS line per claim of THEOREM.md; ends with PASS_P104_DUALITY_CEILING_FLAG_NOTE (exit 1 on any FAIL). +Run from anywhere: python3.12 -I -B research/p104-duality-ceiling-flag-note/check.py (writes nothing). +Standard library only. The quote checks read the repository files named in data/quotes.json (root is two levels above this +package); a missing file or a changed line is a FAIL, never a skip. Each check script prints 'ok' or 'FAIL' lines and a +PASS_* marker; the driver requires the marker, the exact number of ok lines, and no FAIL.""" +import os, sys, json, subprocess +HERE = os.path.dirname(os.path.abspath(__file__)) +CH = os.path.join(HERE, 'checks') +ROOT = os.path.dirname(os.path.dirname(HERE)) +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) + +quotes = json.load(open(os.path.join(HERE, 'data', 'quotes.json'))) +for rel, ln, sub in quotes['pkg']: + path = os.path.join(ROOT, rel) + if not os.path.isfile(path): + FAIL('Q', f'{rel}:{ln} (file absent)'); continue + lines = open(path, encoding='utf-8', errors='replace').read().split('\n') + ck('Q', ln <= len(lines) and sub in lines[ln - 1], f'{rel}:{ln} contains {sub[:60]!r}') + +# (script, tag, marker, expected number of ok lines) +SCRIPTS = [ + ('duality.py', 'G-duality', 'PASS_DUALITY', 22), + ('omega_floor.py', 'omega-floor', 'PASS_OMEGA_FLOOR', 19), + ('flatten.py', 'flag-flatten', 'PASS_FLATTEN', 4), + ('a2.py', 'A2-toy', 'PASS_A2', 5), + ('lagr.py', 'lagrangian', 'PASS_LAGR', 36), + ('caps.py', 'tile-caps', 'PASS_CAPS', 3), + ('schur_leak.py', 'schur-leak', 'PASS_SCHUR_LEAK', 5), +] +for script, tag, marker, nok in SCRIPTS: + p = subprocess.run([sys.executable, '-I', '-B', os.path.join(CH, script)], cwd=CH, capture_output=True, text=True, timeout=500) + out = p.stdout + p.stderr + oks = [l[5:].strip() for l in out.splitlines() if l.startswith('ok ')] + bad = [l for l in out.splitlines() if l.startswith('FAIL')] + for m in oks: PASS(tag, m) + for b in bad: FAIL(tag, b) + ck(tag, marker in out and p.returncode == 0 and not bad and len(oks) == nok, f'{script}: marker {marker}, {len(oks)} ok lines (expected {nok}), exit {p.returncode}') +print('PASS_P104_DUALITY_CEILING_FLAG_NOTE' if not fails else f'FAILED: {sorted(set(fails))}') +sys.exit(1 if fails else 0) diff --git a/research/p104-duality-ceiling-flag-note/checks/a2.py b/research/p104-duality-ceiling-flag-note/checks/a2.py new file mode 100644 index 0000000000..8bf0c318ef --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/checks/a2.py @@ -0,0 +1,80 @@ +"""A2 toy: the Gram floor does not transfer to arbitrary rank-one decompositions (exact, rational, stdlib only).""" +import itertools +from fractions import Fraction as Fr +fails = [] +def ck(cond, msg): + print(('ok ' if cond else 'FAIL ') + msg, flush=True) + if not cond: fails.append(msg) +L = [(1, -1, 0), (0, 1, -1), (1, 0, -1)] # the three lines of A2 in the plane x+y+z = 0 +def dot(a, b): return sum(x * y for x, y in zip(a, b)) +ip = [[dot(a, b) for b in L] for a in L] # norm 2, odd (+-1) off the diagonal +ck(all(ip[i][i] == 2 and abs(ip[i][j]) == 1 for i in range(3) for j in range(3) if i != j), 'A2: three lines, all pairwise inner products +-1 (odd), so N = I_3') +# unit vector of the plane orthogonal to line i +def cross(a, b): return (a[1]*b[2]-a[2]*b[1], a[2]*b[0]-a[0]*b[2], a[0]*b[1]-a[1]*b[0]) +nrm = (1, 1, 1) +perp = [cross(nrm, L[i]) for i in range(3)] # in the plane, orthogonal to line i +ck(all(dot(perp[i], nrm) == 0 and dot(perp[i], L[i]) == 0 and all(dot(perp[i], L[j]) != 0 for j in range(3) if j != i) for i in range(3)), + 'the plane vector orthogonal to line i is orthogonal to no other line') +# decoder = sum of terms lambda u w^T equal to the projector Pi = I - J/3 of the plane +Pi = [[Fr(int(i == j)) - Fr(1, 3) for j in range(3)] for i in range(3)] +def outer(u, w): return [[Fr(u[i] * w[j]) for j in range(3)] for i in range(3)] +def flat(M): return [x for r in M for x in r] +def solvable(mats, target): + # is target in the Q-span of mats (exact elimination)? + rows = [flat(m) for m in mats] + T = flat(target) + rows_aug = [r[:] for r in rows] + # column space test: rank(rows) == rank(rows + [T]) + def rk(R): + R = [r[:] for r in R]; rr = 0 + for c in range(len(R[0])): + p = next((i for i in range(rr, len(R)) if R[i][c] != 0), None) + if p is None: continue + R[rr], R[p] = R[p], R[rr] + for i in range(len(R)): + if i != rr and R[i][c] != 0: + f = R[i][c] / R[rr][c]; R[i] = [a - f * b for a, b in zip(R[i], R[rr])] + rr += 1 + return rr + return rk(rows) == rk(rows + [T]) +types = [(i, j) for i in range(3) for j in range(3) if i != j] # rho = 1 terms: u orth to line i, w orth to line j +def mat(t): return outer(perp[t[0]], perp[t[1]]) +c2 = any(solvable([mat(t) for t in combo], Pi) for combo in itertools.combinations_with_replacement(types, 2)) +c3 = any(solvable([mat(t) for t in combo], Pi) for combo in itertools.combinations_with_replacement(types, 3)) +ck(not c2 and not c3, 'two or three terms of price 1 (all 6 types, repeats allowed) never sum to the plane identity') +# one term of price 1 plus one other term: the remainder must be rank one, which forces both of its vectors onto lines (price 3) +def rank_rows(M): + M = [r[:] for r in M]; rr = 0 + for c in range(3): + p = next((i for i in range(rr, 3) if M[i][c] != 0), None) + if p is None: continue + M[rr], M[p] = M[p], M[rr] + for i in range(3): + if i != rr and M[i][c] != 0: + f = M[i][c] / M[rr][c]; M[i] = [a - f * b for a, b in zip(M[i], M[rr])] + rr += 1 + return rr +ok = True; seen_forced = set() +for (i, j) in types: + u, w = perp[i], perp[j] + d = dot(u, w) + ok &= d != 0 + lam = Fr(1, d) + R = [[Pi[a][b] - lam * u[a] * w[b] for b in range(3)] for a in range(3)] + ok &= rank_rows(R) == 1 + # a rank-one matrix a b^T with the column space vector proportional to line j and row space vector to line i + col = next(c for c in range(3) if any(R[r][c] != 0 for r in range(3))) + colvec = tuple(R[r][col] for r in range(3)) + row = next(r for r in range(3) if any(R[r][c] != 0 for c in range(3))) + rowvec = tuple(R[row][c] for c in range(3)) + # supports: lines not orthogonal to the vector + S = [k for k in range(3) if dot(L[k], colvec) != 0]; T = [k for k in range(3) if dot(L[k], rowvec) != 0] + seen_forced.add((len(S), len(T), len(set(S) & set(T)))) + ok &= cross(colvec, L[j]) == (0, 0, 0) and cross(rowvec, L[i]) == (0, 0, 0) +ck(ok and seen_forced == {(3, 3, 3)}, 'a price-1 term plus a second term: the second term is forced onto lines j and i, support 3 x 3, price 3 (never 2)') +print('hand: with every term priced >= 1, total cost <= 3 leaves only the term-price multisets (1,1), (1,1,1), (1,2); the first two are excluded by the exact test above and (1,2) by the forced remainder, so c_Gram(A2) >= 4; the forced remainder (price 3) attains 4') +# identity decoder: terms e_p e_p^T, one per line, each of price 1; N o I = I holds since N = I_3 +IDc = sum(len({p} & {p}) for p in range(3)) +ck(IDc == 3 and all(ip[p][q] % 2 == 1 for p in range(3) for q in range(3) if p != q), 'the identity decoder O = I_3 (terms e_p e_p^T, price |{p} & {p}| = 1 each) has N o O = I because N = I_3, and costs 3, below the Gram value 4') +print('PASS_A2' if not fails else 'FAILED_A2') +import sys; sys.exit(1 if fails else 0) diff --git a/research/p104-duality-ceiling-flag-note/checks/caps.py b/research/p104-duality-ceiling-flag-note/checks/caps.py new file mode 100644 index 0000000000..3289717cf2 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/checks/caps.py @@ -0,0 +1,75 @@ +"""Exact tile caps over ALL subspaces of F2^9 for the port set (120 lines minus the 16 pair lines). Stdlib only. +For A of dimension a and B = A + (dimension a+1): area(A,B) = #{ports with label in A} * #{ports orthogonal to B}. +Prints the maximum over all pairs; recursion over reduced row-echelon bases (exhaustive, no sampling).""" +import os, sys, json, time +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import e8lib as E +HERE = os.path.dirname(os.path.abspath(__file__)) +pairs = json.load(open(os.path.join(os.path.dirname(HERE), 'data', 'p104_pairs.json'))) +D = set(pairs['ys']) | set(pairs['zs']) +PORTS = [E.LABEL[i] for i in range(E.n) if i not in D] +assert len(PORTS) == 104 +isp = [0] * 512 +for x in PORTS: isp[x] += 1 +assert max(isp) == 1 +# linear map G with form(x, y) = parity(G(x) & y) +G = [sum(E.form(1 << i, 1 << j) << j for j in range(9)) for i in range(9)] +def Gx(x): + r = 0 + for i in range(9): + if (x >> i) & 1: r ^= G[i] + return r +def par(x): return bin(x).count('1') & 1 +orth = [0] * 512 # bitmask over port indices: ports orthogonal to v +GP = [Gx(x) for x in PORTS] +for v in range(512): + m = 0 + for k, g in enumerate(GP): + if par(g & v) == 0: m |= 1 << k + orth[v] = m +ALL = (1 << 104) - 1 +pc = int.bit_count +results = {} +def run(a): + best = [0, 0, 0]; cnt = [0] + def leaf(basis): + cnt[0] += 1 + el = [0] + o = ALL + for b in basis: + el += [x ^ b for x in el]; o &= orth[b] + po = sum(isp[x] for x in el) + if not po: return + c0 = pc(o) + if po * c0 <= best[0]: return + inA = set(el) + for w in range(1, 512): + if w in inA: continue + c = pc(o & orth[w]) + if po * c > best[0]: best[0] = po * c; best[1] = po; best[2] = c + basis = [0] * a + def rec(i, start): + if i == a: + leaf(basis); return + for p in range(start, a - i - 2, -1): + for fr in range(1 << p): + v = (1 << p) | fr + if any((basis[k] >> p) & 1 for k in range(i)): + break + basis[i] = v + rec(i + 1, p - 1) + rec(0, 8) + return best, cnt[0] +if __name__ == '__main__': + fails = [] + want = {2: 32, 3: 32, 4: 36} + for a in (2, 3, 4): + t = time.time() + best, cnt = run(a) + gauss = 1 + for i in range(a): gauss = gauss * (2 ** (9 - i) - 1) // (2 ** (i + 1) - 1) + ok = cnt == gauss and best[0] == want[a] + print(('ok ' if ok else 'FAIL ') + f'dim A = {a}: {cnt} subspaces (Gaussian binomial {gauss}), maximum area {best[0]} = {best[1]} x {best[2]} [{time.time()-t:.0f}s]', flush=True) + if not ok: fails.append(a) + print('PASS_CAPS' if not fails else 'FAILED_CAPS') + sys.exit(1 if fails else 0) diff --git a/research/p104-duality-ceiling-flag-note/checks/duality.py b/research/p104-duality-ceiling-flag-note/checks/duality.py new file mode 100644 index 0000000000..cd4ff1a5f2 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/checks/duality.py @@ -0,0 +1,196 @@ +"""Theorem G: isotropic transvections in dimension n with product -I <-> reflections in dimension rho = N - n with product -I. +Exact rational arithmetic, standard library only.""" +import itertools, random, sys +from fractions import Fraction as Q +fails = [] +def ck(cond, msg): + print(('ok ' if cond else 'FAIL ') + msg, flush=True) + if not cond: fails.append(msg) +def eye(n): return [[Q(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 rref(M): + M = [r[:] for r in M]; piv = []; r = 0 + for c in range(len(M[0])): + p = next((i for i in range(r, len(M)) 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] = [x / pv for x in M[r]] + for i in range(len(M)): + 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 + return M[:r], piv +def rank(M): return len(rref(M)[0]) +def factor(G): + """rank factorisation G = C R with C (N x r) and R (r x N)""" + R, piv = rref(G) + C = [[row[c] for c in piv] for row in G] + assert mm(C, R) == G + return C, R +def refl(q, p): # I - 2 q p^T (column q, row p), p.q = 1 + n = len(q); return [[Q(int(i == j)) - 2 * q[i] * p[j] for j in range(n)] for i in range(n)] +def transv(x, y): # I - 2 x y^T + n = len(x); return [[Q(int(i == j)) - 2 * x[i] * y[j] for j in range(n)] for i in range(n)] +def prod_left(mats, n): + """T_N ... T_1 for mats = [T_1, ..., T_N]""" + P = eye(n) + for T in mats: P = mm(T, P) + return P +def negI(n): return [[Q(-int(i == j)) for j in range(n)] for i in range(n)] +def dotv(a, b): return sum(x * y for x, y in zip(a, b)) + +def reflections_to_transvections(qs, ps): + N = len(qs); rho = len(qs[0]) + Z = [[dotv(ps[i], qs[j]) for j in range(N)] for i in range(N)] + G = [[(Z[i][j] if i > j else (-Z[i][j] if i < j else Q(0))) for j in range(N)] for i in range(N)] + Y, X = factor(G) # G = Y X, rows y_k of Y, columns x_l of X + n = len(X) + xs = [[X[a][k] for a in range(n)] for k in range(N)]; ys = [Y[k] for k in range(N)] + iso = all(dotv(ys[k], xs[k]) == 0 for k in range(N)) + word = prod_left([transv(xs[k], ys[k]) for k in range(N)], n) + return n, iso, word == negI(n), (xs, ys), G + +def transvections_to_reflections(xs, ys): + N = len(xs); n = len(xs[0]) + G = [[dotv(ys[k], xs[l]) for l in range(N)] for k in range(N)] + Z = [[(Q(1) if i == j else (G[i][j] if i > j else -G[i][j])) for j in range(N)] for i in range(N)] + P, Qt = factor(Z) # Z = P Qt, rows p_i of P, columns q_j of Qt + rho = len(Qt) + ps = [P[i] for i in range(N)]; qs = [[Qt[a][j] for a in range(rho)] for j in range(N)] + unit = all(dotv(ps[i], qs[i]) == 1 for i in range(N)) + word = prod_left([refl(qs[i], ps[i]) for i in range(N)], rho) + return rho, unit, word == negI(rho) + +def check_reflection_word(name, qs, ps, expect_n=None): + N = len(qs); rho = len(qs[0]) + prodR = prod_left([refl(qs[i], ps[i]) for i in range(N)], rho) + pre = prodR == negI(rho) and all(dotv(ps[i], qs[i]) == 1 for i in range(N)) + n, iso, ok, (xs, ys), G = reflections_to_transvections(qs, ps) + ck(pre and iso and ok and n == N - rho, f'{name}: N={N}, rho={rho}: reflections with product -I give isotropic transvections in dimension n={n}=N-rho with product -I') + rho2, unit, ok2 = transvections_to_reflections(xs, ys) + ck(unit and ok2 and rho2 == rho, f'{name}: and back: the transvection word returns reflections in dimension {rho2} with product -I') + +# ---- Coxeter words (w0 = -I): reduced word by greedy length increase, reflections are the inversion roots +def coxeter(name, simple, positive_funcional): + d = len(simple) + def s(a): + aa = dotv(a, a); return [[Q(int(i == j)) - 2 * a[i] * a[j] / aa for j in range(d)] for i in range(d)] + S = [s(a) for a in simple] + w = eye(d); betas = [] + while True: + for i, a in enumerate(simple): + wa = [sum(w[r][c] * a[c] for c in range(d)) for r in range(d)] + if positive_funcional(wa) > 0: + betas.append(wa); w = mm(w, S[i]); break + else: + break + assert w == negI(d), 'w0 is not -I' + qs = betas; ps = [[x / dotv(b, b) for x in b] for b in betas] + # product of s_beta_N ... s_beta_1 = w0 = -I with betas in this order + check_reflection_word(name, qs, ps) + return len(betas) +def F(vals): + return lambda v: sum(Q(a) * x for a, x in zip(vals, v)) +# D4, B3, F4 in coordinates (rational) +D4 = [[1, -1, 0, 0], [0, 1, -1, 0], [0, 0, 1, -1], [0, 0, 1, 1]] +coxeter('Coxeter D4 w0', [[Q(x) for x in r] for r in D4], F([1000, 100, 10, 1])) +B3 = [[1, -1, 0], [0, 1, -1], [0, 0, 1]] +coxeter('Coxeter B3 w0', [[Q(x) for x in r] for r in B3], F([100, 10, 1])) +F4 = [[0, 1, -1, 0], [0, 0, 1, -1], [0, 0, 0, 1], [Q(1, 2), Q(-1, 2), Q(-1, 2), Q(-1, 2)]] +nF4 = coxeter('Coxeter F4 w0', [[Q(x) for x in r] for r in F4], F([1000, 100, 10, 1])) +ck(nF4 == 24, 'F4 reduced word of w0 has 24 reflections') +# dihedral words for k = 4 (B2), 6 (G2): Cartan realisation in the simple-root basis +def dihedral_cartan(name, c12, c21, N): + # s1: e1 -> -e1, e2 -> e2 - c21*e1 (row convention on coordinates); build reflections as matrices acting on coordinate vectors + A = [[Q(-1), Q(-c12)], [Q(0), Q(1)]] # s1 acts on coords: a1 -> -a1, a2 -> a2 + (-c12... ) use Cartan pairing + Bm = [[Q(1), Q(0)], [Q(-c21), Q(-1)]] + return A, Bm +def refl_from_matrix(M): + d = len(M); R = [[M[i][j] - Q(int(i == j)) for j in range(d)] for i in range(d)] # M - I = -2 q p^T (rank one) + r = next(i for i in range(d) if any(R[i][j] != 0 for j in range(d))) + j0 = next(j for j in range(d) if R[r][j] != 0) + q = [R[i][j0] for i in range(d)] # a column of M - I + # M - I = q * u^T with u a row; -2 p = u => p = -u/2 ; check p.q = 1 + u = [R[r][j] / q[r] for j in range(d)] + p = [-x / 2 for x in u] + assert refl(q, p) == M, 'not a reflection' + assert dotv(p, q) == 1 + return q, p +for name, c12, c21, k in (('dihedral I2(4)=B2', 1, 2, 4), ('dihedral I2(6)=G2', 1, 3, 6)): + A, Bm = dihedral_cartan(name, c12, c21, k) + # the inversion reflections of the reduced word s1 s2 s1 ... (conjugates of the simple reflections) + S = [A, Bm]; w = eye(2) + for t in range(k): + i = t % 2 + # beta_t = w * alpha_i where alpha_i is the i-th coordinate vector + alpha = [Q(int(r == i)) for r in range(2)] + beta = [sum(w[r][c] * alpha[c] for c in range(2)) for r in range(2)] + w = mm(w, S[i]) + ck(w == negI(2), f'{name}: reduced word s1 s2 ... of length {k} equals -I') + # reflection s_beta = w_{t-1} s_i w_{t-1}^{-1} + refl_list = [] + w = eye(2) + for t in range(k): + i = t % 2 + # conjugate: M_beta = w S_i w^{-1} + winv = [[w[1][1], -w[0][1]], [-w[1][0], w[0][0]]] + det = w[0][0] * w[1][1] - w[0][1] * w[1][0] + winv = [[x / det for x in r] for r in winv] + refl_list.append(mm(mm(w, S[i]), winv)); w = mm(w, S[i]) + pairs = [refl_from_matrix(M) for M in refl_list] + check_reflection_word(name, [q for q, p in pairs], [p for q, p in pairs]) +# ---- random words in rho = 2: choose N - 2 random reflections, then close with two reflections r_N r_{N-1} = M +rng = random.Random(2) +def random_word(N): + while True: + pairs = [] + for _ in range(N - 2): + q = [Q(rng.randint(-4, 4)) for _ in range(2)] + p0 = [Q(rng.randint(-4, 4)) for _ in range(2)] + d = dotv(p0, q) + if d == 0: break + p = [x / d for x in p0]; pairs.append((q, p)) + else: + P = eye(2) + for q, p in pairs: P = mm(refl(q, p), P) + M = [[-x for x in r] for r in P] # need r_N r_{N-1} = -P^{-1} + det = M[0][0] * M[1][1] - M[0][1] * M[1][0] + if det == 0: continue + Mi = [[M[1][1] / det, -M[0][1] / det], [-M[1][0] / det, M[0][0] / det]] # (-P)^-1 + # want r_N r_{N-1} * P = -I, i.e. r_N r_{N-1} = -P^{-1} = Mi + # r_N = Mi r_{N-1}: reflection needs trace(Mi r) = 0 for det(Mi) = 1 (the product of N-2 reflections has det (+1)^(N-2) with N even) + q5 = [Q(rng.randint(-4, 4)) for _ in range(2)] + tr = Mi[0][0] + Mi[1][1] + Mq = [Mi[0][0] * q5[0] + Mi[0][1] * q5[1], Mi[1][0] * q5[0] + Mi[1][1] * q5[1]] + # solve p.q5 = 1 and p.Mq = tr/2 + a, b = q5; c_, d_ = Mq + D_ = a * d_ - b * c_ + if D_ == 0: continue + p5 = [(Q(1) * d_ - b * (tr / 2)) / D_, (a * (tr / 2) - c_ * Q(1)) / D_] + r5 = refl(q5, p5) + r6 = mm(Mi, r5) + # r6 must be a reflection I - 2 q6 p6^T + try: + q6, p6 = refl_from_matrix(r6) + except (AssertionError, StopIteration): + continue + pairs += [(q5, p5), (q6, p6)] + P = eye(2) + for q, p in pairs: P = mm(refl(q, p), P) + if P != negI(2): continue + return [q for q, p in pairs], [p for q, p in pairs] +for N in (6, 8, 10, 12): + qs, ps = random_word(N) + check_reflection_word(f'random rho=2 word', qs, ps) +# control: perturbing one reflection destroys the product -I and the transvection side +qs, ps = random_word(8) +qs2 = [q[:] for q in qs]; qs2[3] = [qs2[3][0] + 1, qs2[3][1]] +ps2 = [p[:] for p in ps]; d = dotv(ps2[3], qs2[3]) +if d != 0: + ps2[3] = [x / d for x in ps2[3]] + prodR = prod_left([refl(qs2[i], ps2[i]) for i in range(8)], 2) + n2, iso2, ok2, _, _ = reflections_to_transvections(qs2, ps2) + ck(prodR != negI(2) and not ok2, 'control: perturbing one reflection destroys the product -I on both sides') +print('PASS_DUALITY' if not fails else 'FAILED_DUALITY') +sys.exit(1 if fails else 0) diff --git a/research/p104-duality-ceiling-flag-note/checks/e8lib.py b/research/p104-duality-ceiling-flag-note/checks/e8lib.py new file mode 100644 index 0000000000..1901a6a92e --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/checks/e8lib.py @@ -0,0 +1,107 @@ +"""E8 from scratch (doubled coordinates), F2 labels, simple roots and fundamental weights. Standard library only.""" +import itertools +from fractions import Fraction as Fr + +def build(): + roots = [] + for i, j in itertools.combinations(range(8), 2): + for si in (2, -2): + for sj in (2, -2): + v = [0] * 8; v[i] = si; v[j] = sj; roots.append(tuple(v)) + for s in itertools.product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: + roots.append(tuple(s)) + assert len(roots) == 240 + seen = set(); lines = [] + for r in roots: + if tuple(-x for x in r) in seen: + continue + seen.add(r); lines.append(r) + assert len(lines) == 120 + return roots, lines + +ROOTS, LINES = build() +n = 120 +def dot(a, b): return sum(x * y for x, y in zip(a, b)) +def ip(a, b): return dot(a, b) // 4 # root inner product, norm 2 +IP = [[ip(LINES[i], LINES[j]) for j in range(n)] for i in range(n)] +# N[i][j] = 1 iff the root inner product is even (orthogonal or equal); one bitmask row per line +NR = [sum(1 << j for j in range(n) if IP[i][j] % 2 == 0) for i in range(n)] + +def rank2(rows): + b = [] + for v in rows: + for x in b: + v = min(v, v ^ x) + if v: + b.append(v) + return len(b) + +def rho(S, T): + """rank over F2 of N[S,T]""" + if not S or not T: + return 0 + tm = sum(1 << t for t in T) + return rank2([NR[s] & tm for s in S]) + +# simple roots: positive roots (generic functional) that are not a sum of two positive roots +GEN = (1000, 100, 10, 1, 10007, 1009, 101, 11) # generic integer functional +def func(r): return sum(a * b for a, b in zip(GEN, r)) +POS = [r if func(r) > 0 else tuple(-x for x in r) for r in LINES] +POSSET = set(POS) +SIMPLE = [r for r in POS if not any(tuple(a - b for a, b in zip(r, q)) in POSSET for q in POS)] +assert len(SIMPLE) == 8 + +def solve_dual(vs): + """rows of Fraction inverse so that columns give vectors w_l with dot(vs[k], w_l)=delta (vs: 8 vectors)""" + M = [[Fr(x) for x in row] + [Fr(int(i == j)) for j in range(8)] for i, row in enumerate(vs)] + for c in range(8): + p = next(i for i in range(c, 8) if M[i][c] != 0); M[c], M[p] = M[p], M[c] + pv = M[c][c]; M[c] = [x / pv for x in M[c]] + for i in range(8): + if i != c and M[i][c] != 0: + f = M[i][c]; M[i] = [a - f * b for a, b in zip(M[i], M[c])] + inv = [row[8:] for row in M] # inverse of the matrix with rows vs + return [[inv[i][l] for i in range(8)] for l in range(8)] + +def scale_int(v): + import math + den = 1 + for x in v: + den = den * x.denominator // math.gcd(den, x.denominator) + return tuple(int(x * den) for x in v) + +# fundamental weights w_i with ip(w_i, alpha_j) = delta (simple roots have doubled norm 8: dot/4) +_cols = solve_dual([tuple(Fr(x) for x in s) for s in SIMPLE]) # dot(s_k, col_l) = delta_kl +WEIGHTS = [scale_int(c) for c in _cols] # proportional to the fundamental weights (ray directions) +for i, w in enumerate(WEIGHTS): + assert all((dot(SIMPLE[k], w) == 0) == (k != i) for k in range(8)) + +# F2 labels: label(l) = (1, c_1 mod 2, ..., c_8 mod 2), c_i = coefficient of l on the simple roots +def coeffs(l): + # coefficient vector solving sum c_i alpha_i = l, via the dual vectors + out = [] + for i in range(8): + num = dot(l, _cols[i]); out.append(num) + return out +LABEL = [] +for l in LINES: + c = coeffs(l) + assert all(x.denominator == 1 for x in c) + bits = 1 + for i, x in enumerate(c): + bits |= (int(x) & 1) << (i + 1) + LABEL.append(bits) + +# the form on F2^9 whose Gram matrix on labels is N: <(a,v),(b,w)> = ab + v^T C w, C the Cartan matrix mod 2 +CART = [[ip(SIMPLE[i], SIMPLE[j]) % 2 for j in range(8)] for i in range(8)] +def form(x, y): + a, b = x & 1, y & 1 + v, w = x >> 1, y >> 1 + s = a & b + for i in range(8): + if (v >> i) & 1: + for j in range(8): + if (w >> j) & 1: + s ^= CART[i][j] + return s diff --git a/research/p104-duality-ceiling-flag-note/checks/flatten.py b/research/p104-duality-ceiling-flag-note/checks/flatten.py new file mode 100644 index 0000000000..d146e10926 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/checks/flatten.py @@ -0,0 +1,77 @@ +"""Theorem F (flag chains flatten onto N at no higher price). Stdlib only.""" +import os, sys, random +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import e8lib as E +n = E.n +fails = [] +def ck(cond, msg): + print(('ok ' if cond else 'FAIL ') + msg, flush=True) + if not cond: fails.append(msg) +def span_set(gens): + S = {0} + for g in gens: + if g not in S: S |= {s ^ g for s in S} + return S +def dim(S): return len(S).bit_length() - 1 +def orth_to(S): # ports whose label is orthogonal (form) to every element of S + return [p for p in range(n) if all(E.form(E.LABEL[p], x) == 0 for x in S)] +def inside(S): return [p for p in range(n) if E.LABEL[p] in S] +def flag(m, rng): + F = [span_set([rng.randrange(1, 512) for _ in range(rng.randint(4, 8))])] + for i in range(m): + base = sorted(F[-1]) + F.append(span_set([rng.choice(base) for _ in range(rng.randint(0, max(0, dim(F[-1]) - 1)))])) + return F +def rand_vec(supp, rng): + v = [0] * n + for p in supp: + if rng.random() < 0.7: v[p] = rng.randint(-3, 3) + return v +def run_chain(F, rng, nested=True): + ev = [] # time-ordered events (kind, vector) + for lvl, Fi in enumerate(F): + reads = inside(Fi); writes = orth_to(Fi) + items = [] + for _ in range(rng.randint(0, 2)): items.append(('R', rand_vec(reads, rng))) + for _ in range(rng.randint(0, 2)): items.append(('W', rand_vec(writes, rng))) + rng.shuffle(items); ev += items + X = [[0] * n for _ in range(n)] + seen_reads = [0] * n + for kind, v in ev: + if kind == 'R': + for p in range(n): seen_reads[p] += v[p] + else: + for s in range(n): + if v[s]: + for p in range(n): + if seen_reads[p]: X[s][p] += v[s] * seen_reads[p] + w = [sum(v[s] for k, v in ev if k == 'W') for s in range(n)] + r = [sum(v[p] for k, v in ev if k == 'R') for p in range(n)] + return X, w, r +rng = random.Random(12) +okF = okP = True; total = 0; nonzero = 0; mismatch_ctrl = 0; ctrl = 0 +for t in range(60): + m = rng.randint(1, 4) + F = flag(m, rng) + X, w, r = run_chain(F, rng) + S = [s for s in range(n) if w[s]]; T = [p for p in range(n) if r[p]] + for s in range(n): + for p in range(n): + if (E.NR[s] >> p) & 1: + if X[s][p] != w[s] * r[p]: okF = False + if w[s] * r[p]: nonzero += 1 + mass = dim(F[0]) - dim(F[-1]) + if E.rho(S, T) > mass: okP = False + total += 1 +ck(okF, f'N o X = N o (w r^T) on all {total} random flag chains (nested frames, interleaved reads and writes, depth 1 to 4)') +ck(nonzero > 0, f'the test is not vacuous: {nonzero} N entries with w(s) r(p) != 0') +ck(okP, 'price: rho(supp w, supp r) <= dim F_0 - dim F_m on every chain (reads in F_0, writes orthogonal to F_m)') +# control: frames that are not nested (an ascent) break the flattening +for t in range(60): + F = [span_set([rng.randrange(1, 512) for _ in range(rng.randint(3, 7))]) for _ in range(3)] + X, w, r = run_chain(F, rng) + ctrl += 1 + if any(((E.NR[s] >> p) & 1) and X[s][p] != w[s] * r[p] for s in range(n) for p in range(n)): mismatch_ctrl += 1 +ck(mismatch_ctrl > 0, f'control: with non-nested frames the flattening fails on {mismatch_ctrl} of {ctrl} random programs (hypothesis is used)') +print('PASS_FLATTEN' if not fails else 'FAILED_FLATTEN') +sys.exit(1 if fails else 0) diff --git a/research/p104-duality-ceiling-flag-note/checks/lagr.py b/research/p104-duality-ceiling-flag-note/checks/lagr.py new file mode 100644 index 0000000000..3908e524c3 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/checks/lagr.py @@ -0,0 +1,108 @@ +"""Theorems I and R: the subspace frames are the geodesic interval, and rho(L) = L_{pi_1(L)} is a 1-Lipschitz retraction. Exhaustive for h <= 4. Stdlib only.""" +import itertools, sys +fails = [] +def ck(cond, msg): + print(('ok ' if cond else 'FAIL ') + msg, flush=True) + if not cond: fails.append(msg) +def par(x): return bin(x).count('1') & 1 +def sp(h, u, v): + m = (1 << h) - 1 + return par((u >> h) & (v & m)) ^ par((u & m) & (v >> h)) +def span(gens): + S = {0} + for g in gens: + if g not in S: S |= {s ^ g for s in S} + return frozenset(S) +def dimof(S): return len(S).bit_length() - 1 +def subspaces(h): + seen = {frozenset({0})}; fr = list(seen) + while fr: + nxt = [] + for U in fr: + for v in range(1, 1 << h): + if v not in U: + W = frozenset(U | {u ^ v for u in U}) + if W not in seen: seen.add(W); nxt.append(W) + fr = nxt + return list(seen) +def perp(h, U): return frozenset(v for v in range(1 << h) if all(par(v & u) == 0 for u in U)) +def LU(h, U): # {(u, u+v) : u in U, v in U^perp}, vector = (x << h) | z + return frozenset((u << h) | (u ^ v) for u in U for v in perp(h, U)) +def lagrangians(h): + L0 = frozenset(range(1 << h)) # {(0, z)} is x = 0: with (x<> h for x in L) +for h in (1, 2, 3, 4): + Ls = lagrangians(h) + expect = 1 + for i in range(1, h + 1): expect *= (2 ** i + 1) + ck(len(Ls) == expect and all(len(L) == 2 ** h and all(sp(h, a, b) == 0 for a in list(L)[:8] for b in L) for L in Ls[:200]), f'h={h}: {len(Ls)} Lagrangians = prod (2^i + 1), isotropic of size 2^h') + Us = subspaces(h) + FU = {U: LU(h, U) for U in Us} + ck(len(set(FU.values())) == len(Us) and all(L in set(Ls) for L in FU.values()), f'h={h}: U -> L_U is injective into the Lagrangians ({len(Us)} subspaces)') + L0 = LU(h, frozenset({0})); LF = LU(h, frozenset(range(1 << h))) + interval = {L for L in Ls if dist(h, L0, L) + dist(h, L, LF) == h} + ck(interval == set(FU.values()), f'h={h} Theorem I: the Lagrangians on a geodesic from L_0 to L_F are exactly the L_U') + ok = all(dist(h, FU[U], FU[V]) == dimof(U) + dimof(V) - 2 * dimof(U & V) for U, V in itertools.combinations(Us, 2)) + ck(ok, f'h={h}: d(L_U, L_V) = dim U + dim V - 2 dim(U cap V)') + # adjacency by hyperplanes + byhyp = {} + for idx, L in enumerate(Ls): + els = sorted(L) + basis = [] + for v in els: + if v not in span(basis): basis.append(v) + # direct: a hyperplane is the span of L minus a coset; enumerate via functionals on coordinates of the basis + coords = {} + for c in range(1 << h): + vec = 0 + for i in range(h): + if (c >> i) & 1: vec ^= basis[i] + coords[vec] = c + for f in range(1, 1 << h): + H = frozenset(v for v, c in coords.items() if par(c & f) == 0) + byhyp.setdefault(H, []).append(idx) + adj = [set() for _ in Ls] + for H, lst in byhyp.items(): + for a in lst: + for b in lst: + if a != b: adj[a].add(b) + ck(all(dist(h, Ls[a], Ls[b]) == 1 for a in range(len(Ls)) for b in adj[a]) and all(len(adj[a]) == 2 * (2 ** h - 1) for a in range(len(Ls))), f'h={h}: adjacency (meeting in a hyperplane) has valency 2(2^h - 1)') + # d is the graph distance (all sources for h <= 3, two sources for h = 4) + srcs = range(len(Ls)) if h <= 3 else [0, len(Ls) // 2] + okd = True + for s in srcs: + D = {s: 0}; fr = [s] + while fr: + nxt = [] + for a in fr: + for b in adj[a]: + if b not in D: D[b] = D[a] + 1; nxt.append(b) + fr = nxt + okd &= all(D[b] == dist(h, Ls[s], Ls[b]) for b in range(len(Ls))) + ck(okd, f'h={h}: d(L, L\') = h - dim(L cap L\') equals the graph distance ({"all" if h <= 3 else "two"} sources)') + # Theorem R + rho = {}; allproj = True + for L in Ls: + U = proj1(h, L) + Z = frozenset(z for (x, z) in ((v >> h, v & ((1 << h) - 1)) for v in L) if x == 0) + okproj = all(par(u & z) == 0 for u in U for z in Z) and len(U) * len(Z) == 2 ** h + rho[L] = LU(h, U) + allproj &= okproj + idx = {L: i for i, L in enumerate(Ls)} + ck(all(rho[L] == L for L in FU.values()) and allproj, f'h={h} Theorem R: rho fixes every L_U, and pi_1(L) is the orthogonal complement of L cap L_0 (sizes multiply to 2^h)') + bad = sum(1 for a in range(len(Ls)) for b in adj[a] if dist(h, rho[Ls[a]], rho[Ls[b]]) > 1) + ck(bad == 0, f'h={h} Theorem R: d(rho L, rho L\') <= 1 for all {sum(len(x) for x in adj)} ordered adjacent pairs (violations {bad})') + nonfam = sum(1 for L in Ls if L not in set(FU.values())) + ck(h < 2 or nonfam > 0, f'h={h}: {nonfam} Lagrangians are not subspace frames (the retraction moves them)') +print('PASS_LAGR' if not fails else 'FAILED_LAGR') +sys.exit(1 if fails else 0) diff --git a/research/p104-duality-ceiling-flag-note/checks/omega_floor.py b/research/p104-duality-ceiling-flag-note/checks/omega_floor.py new file mode 100644 index 0000000000..38ede9cffc --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/checks/omega_floor.py @@ -0,0 +1,142 @@ +"""Gram-class floor checks (stdlib only). Prints OMEGA_FLOOR lines; final marker PASS_OMEGA_FLOOR.""" +import os, sys, json, random, itertools +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import e8lib as E +from fractions import Fraction as Fr +HERE = os.path.dirname(os.path.abspath(__file__)) +n = E.n +fails = [] +def ck(cond, msg): + print(('ok ' if cond else 'FAIL ') + msg, flush=True) + if not cond: fails.append(msg) + +# (1) basic structure: rank_F2 N = 9, labels realise N, tight frame +ck(E.rank2(E.NR) == 9, 'rank_F2 N = 9 on the 120 lines (N = even root inner product)') +ck(all(E.form(E.LABEL[i], E.LABEL[j]) == ((E.NR[i] >> j) & 1) for i in range(n) for j in range(n)), + 'labels in F2^9 with the form <(a,v),(b,w)> = ab + v C w reproduce N on all 120 x 120 pairs') +S = [[sum(l[i] * l[j] for l in E.LINES) for j in range(8)] for i in range(8)] +ck(all(S[i][j] == (120 if i == j else 0) for i in range(8) for j in range(8)), 'sum over the 120 lines of l l^T = 120 I (tight frame, norm 8 coordinates): trace constant 120/8 = 15 per unit term') + +# (2) census: cost_a(r) = |T(r)| - max over codim-a subspaces W of F2^9 of #{labels of T(r) inside W}, a = 1, 2, all 8 ray types +def popc(x): return bin(x).count('1') +def par(x): return popc(x) & 1 +costs = [] +for w in E.WEIGHTS: + T = [i for i in range(n) if E.dot(E.LINES[i], w) != 0] + masks = {} + for f in range(1, 512): + masks[f] = sum(1 << k for k, i in enumerate(T) if par(f & E.LABEL[i]) == 0) + full = (1 << len(T)) - 1 + c1 = len(T) - max(popc(m) for m in masks.values()) + best2 = 0 + for f in range(1, 512): + mf = masks[f] + for g in range(f + 1, 512): + if g == f: continue + c = popc(mf & masks[g]) + if c > best2: best2 = c + c2 = len(T) - best2 + costs.append((len(T), c1, c2)) +print('ray types (|T|, cost_1, cost_2):', costs) +ck(len(set(E.WEIGHTS)) == 8, 'eight fundamental-weight rays') +ck(min(c[2] for c in costs) == 25, 'min over the eight ray types of cost_2 is 25 (so a >= 2 needs at least 25 deleted lines)') +ck(min(c[1] for c in costs) == 1 and sorted(c[1] for c in costs)[1] >= 14, 'cost_1: exactly one ray type has cost 1 (the root ray), every other type costs at least 14') +root_ray = [c for c in costs if c[0] == 57] +ck(len(root_ray) == 1 and root_ray[0][1:] == (1, 25), 'root ray (|T| = 57): cost_1 = 1, cost_2 = 25') + +# (3) exact designs: biorthogonal root-pair design (P104-type), generic basis (P120), orthoframe (P112) +def supp(u, D): return [p for p in range(n) if p not in D and E.dot(E.LINES[p], u) != 0] +def price(U, W, D): + rs = [E.rho(supp(u, D), supp(w, D)) for u, w in zip(U, W)] + return sum(rs), rs +pairs = json.load(open(os.path.join(os.path.dirname(HERE), 'data', 'p104_pairs.json'))) +ys, zs = pairs['ys'], pairs['zs'] +IP = E.IP +ck(all((IP[ys[k]][zs[l]] == 0) == (k != l) for k in range(8) for l in range(8)) and all(abs(IP[ys[k]][zs[k]]) == 1 for k in range(8)) and len(set(ys + zs)) == 16, + 'data/p104_pairs.json: 16 distinct lines, y_k.z_l = 0 for k != l, y_k.z_k = +-1 (eight A2-adjacent pairs)') +U = [E.LINES[y] for y in ys] +Wd = E.solve_dual(U) +Wd = [E.scale_int(c) for c in Wd] +ck(all(all(Wd[k][i] * E.LINES[zs[k]][j] == Wd[k][j] * E.LINES[zs[k]][i] for i in range(8) for j in range(8)) for k in range(8)), 'dual basis of the y_k is proportional to the z_k') +D16 = set(ys) | set(zs) +c, rs = price(U, Wd, D16) +ck(c == 56 and rs == [7] * 8, 'P104-type design (16 lines deleted, eight terms): c = 56, every rho_k = 7') +c120, rs120 = price(U, Wd, set()) +ck(c120 == 72 and rs120 == [9] * 8, 'same eight terms on all 120 lines: c = 72, every rho_k = 9') +random.seed(3) +def rand_basis(): + while True: + B = [tuple(random.randint(-3, 3) for _ in range(8)) for _ in range(8)] + try: + Wb = [E.scale_int(cc) for cc in E.solve_dual(B)] + return B, Wb + except StopIteration: + continue +B, Wb = rand_basis() +ck(price(B, Wb, set())[0] == 72, 'generic dual bases on 120 lines: c = 72') +fr = [] +cand = list(range(n)); random.shuffle(cand) +for p in cand: + if all(IP[p][q] == 0 for q in fr): fr.append(p) +ck(len(fr) == 8, 'eight mutually orthogonal roots exist'); +cf, rf = price([E.LINES[p] for p in fr], [E.LINES[p] for p in fr], set(fr)) +ck(cf == 64, 'orthoframe on the 112 lines (frame deleted): c = 64') + +# (4) Theorem O on random Gram-class designs: Cauchy-Binet subset, Sylvester bound, a_k <= 1 when |D| <= 24 +def rank_real_rows(vs): + M = [[Fr(x) for x in v] for v in vs]; r = 0 + for cidx in range(len(M[0]) if M else 0): + p = next((i for i in range(r, len(M)) if M[i][cidx] != 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][cidx] != 0: + f = M[i][cidx] / M[r][cidx]; M[i] = [a - f * b for a, b in zip(M[i], M[r])] + r += 1 + return r +def codim(S_): # a = 9 - dim span of labels + return 9 - E.rank2([E.LABEL[i] for i in S_]) +def rand_vec(kind): + if kind == 0: return E.LINES[random.randrange(n)] + if kind == 1: return tuple(random.randint(-2, 2) for _ in range(8)) + if kind == 2: # sum of two lines + a, b = E.LINES[random.randrange(n)], E.LINES[random.randrange(n)] + return tuple(x + y for x, y in zip(a, b)) + return E.WEIGHTS[random.randrange(8)] +random.seed(9) +ntests = 0; minc = 10**9; ok_a = ok_cb = ok_syl = True +for trial in range(300): + p = random.randint(16, 24) + if trial % 3 == 0: # adversarial: start from the 16 pair lines + D = set(D16) + else: + D = set() + while len(D) < p: D.add(random.randrange(n)) + m = random.randint(8, 11) + for _ in range(50): + Us = [rand_vec(random.choice((0, 0, 1, 2, 3))) for _ in range(m)] + Ws = [rand_vec(random.choice((0, 0, 1, 2, 3))) for _ in range(m)] + if all(any(v) for v in Us + Ws): break + # M = sum u_k w_k^T; use only if invertible + Mx = [[sum(Us[k][i] * Ws[k][j] for k in range(m)) for j in range(8)] for i in range(8)] + if rank_real_rows(Mx) != 8: continue + ntests += 1 + Ss = [supp(u, D) for u in Us]; Ts = [supp(w, D) for w in Ws] + rk = [E.rho(a, b) for a, b in zip(Ss, Ts)] + ak = [codim(a) for a in Ss]; bk = [codim(b) for b in Ts] + ok_a &= all(x <= 1 for x in ak + bk) + ok_syl &= all(rk[k] >= 9 - ak[k] - bk[k] for k in range(m)) + # Cauchy-Binet: a subset K of 8 terms with both U_K and W_K invertible exists + found = False + for K in itertools.combinations(range(m), 8): + if rank_real_rows([Us[k] for k in K]) == 8 and rank_real_rows([Ws[k] for k in K]) == 8: + found = True; break + ok_cb &= found + minc = min(minc, sum(rk)) +ck(ntests >= 100, f'{ntests} random Gram-class designs with 16 <= |D| <= 24 and invertible M') +ck(ok_cb, 'Cauchy-Binet: every one of them contains 8 terms with both top and bottom vectors a basis') +ck(ok_a, 'every top and bottom has a <= 1 (codim of the label span of its support), as the census forces for |D| <= 24') +ck(ok_syl, 'Sylvester: rho_k >= 9 - a_k - b_k on every term of every design') +ck(minc >= 56, f'cost of every random design >= 56 (minimum seen {minc})') +print('PASS_OMEGA_FLOOR' if not fails else 'FAILED_OMEGA_FLOOR') +sys.exit(1 if fails else 0) diff --git a/research/p104-duality-ceiling-flag-note/checks/schur_leak.py b/research/p104-duality-ceiling-flag-note/checks/schur_leak.py new file mode 100644 index 0000000000..cc2f847108 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/checks/schur_leak.py @@ -0,0 +1,100 @@ +"""Schur law for owned lifetimes and the per-register leak identity: exact rational arithmetic, stdlib only.""" +import random, sys +from fractions import Fraction as Q +fails = [] +def ck(cond, msg): + print(('ok ' if cond else 'FAIL ') + msg, flush=True) + if not cond: fails.append(msg) +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 eye(n): return [[Q(int(i == j)) for j in range(n)] for i in range(n)] +def inv(A): + n = len(A); M = [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 M[r][c] != 0), None) + if p is None: return None + M[c], M[p] = M[p], M[c] + pv = M[c][c]; M[c] = [x / pv for x 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 sub(M, R, C): return [[M[i][j] for j in C] for i in R] +def sm(A, B): return [[a - b for a, b in zip(r, s)] for r, s in zip(A, B)] +rng = random.Random(4) +def rand_inv(n): + while True: + M = [[Q(rng.randint(-3, 3)) for _ in range(n)] for _ in range(n)] + if inv(M) is not None: return M +# Schur law: T_f invertible on cells P + O. Rows (outputs) = P_r + O_d, columns (inputs) = P_c + O_b. +nP, nO = 5, 3 +okS = okI = True; cases = 0; singular_seen = 0 +for trial in range(60): + n = nP + nO + Tf = rand_inv(n) + P = list(range(nP)); O = list(range(nP, n)) + Tpub = sub(Tf, P, P) + Ti = inv(Tf) # rows indexed by inputs, columns by outputs + Dd = sub(Ti, O, O) # Tinv_f[O_b, O_d] + Dinv = inv(Dd) + Tp_inv = inv(Tpub) + # invertible iff the owned block of the inverse is invertible + okI &= ((Tp_inv is not None) == (Dinv is not None)) + if Tp_inv is not None and Dinv is not None: + rhs = sm(sub(Ti, P, P), mm(mm(sub(Ti, P, O), Dinv), sub(Ti, O, P))) + okS &= (Tp_inv == rhs); cases += 1 + else: + singular_seen += 1 +# force singular cases: make the owned block of the inverse singular +for trial in range(20): + n = nP + nO + Tf = rand_inv(n) + Ti = inv(Tf) + # modify T_f so that Tinv[O,O] has a zero column: set the last owned column of Ti on O rows to 0 via Tf = inv(Ti') + for r in range(nP, n): Ti[r][n - 1] = Q(0) + Tf2 = inv(Ti) + if Tf2 is None: continue + Tpub = sub(Tf2, list(range(nP)), list(range(nP))) + okI &= (inv(Tpub) is None) and (inv(sub(Ti, list(range(nP, n)), list(range(nP, n)))) is None) + singular_seen += 1 +ck(okS and cases >= 30, f'Schur law Tinv_pub = Tinv[P,P] - Tinv[P,O_d] Tinv[O_b,O_d]^-1 Tinv[O_b,P] exact on {cases} random invertible T_f (5 public cells, 3 owned lifetimes)') +ck(okI and singular_seen >= 10, f'T_pub = T_f[P,P] is invertible exactly when Tinv_f[O_b,O_d] is, including {singular_seen} singular cases') +# Leak identity: T = B A at a cut; per register i four rank-one terms +okL = okSum = True +for trial in range(40): + n = 7; nX = 3 + A = rand_inv(n); B = rand_inv(n) + Ai = inv(A); Bi = inv(B) + T = mm(B, A); Ti = inv(T) + Xp = list(range(nX)); Yp = list(range(nX, 2 * nX)) + f = [[sum(B[y][i] * A[i][x] for i in range(n)) for x in Xp] for y in Yp] + r = [[sum(Ai[x][i] * Bi[i][y] for i in range(n)) for y in Yp] for x in Xp] + okSum &= (f == [[T[y][x] for x in Xp] for y in Yp]) and (r == [[Ti[x][y] for y in Yp] for x in Xp]) + LXs = [[sum(Ai[x][i] * A[i][xp] for i in range(n)) for xp in Xp] for x in Xp] + LYs = [[sum(B[y][i] * Bi[i][yp] for i in range(n)) for yp in Yp] for y in Yp] + okSum &= (LXs == [[Q(int(a == b)) for b in range(nX)] for a in range(nX)]) and (LYs == [[Q(int(a == b)) for b in range(nX)] for a in range(nX)]) + for i in range(n): + for x in Xp: + for xp in Xp: + for y in range(nX): + for yp in range(nX): + fi = B[Yp[y]][i] * A[i][xp]; ri = Ai[x][i] * Bi[i][Yp[yp]] + lx = Ai[x][i] * A[i][xp]; ly = B[Yp[y]][i] * Bi[i][Yp[yp]] + okL &= (lx * ly == ri * fi) + # invariance under a diagonal rescaling of register i (A -> D A, B -> B D^-1) +ck(okSum, 'sums over registers: sum f_i = T[Y,X], sum r_i = Tinv[X,Y], sum L_X,i = I, sum L_Y,i = I (40 random cuts, exact)') +ck(okL, 'leak identity L_X,i[x,x\'] L_Y,i[y,y\'] = r_i[x,y\'] f_i[y,x\'] for every register i, every index quadruple (40 random cuts, 7 registers)') +# gauge invariance of each of the four terms under diagonal rescaling of one register +A = rand_inv(6); B = rand_inv(6); Ai = inv(A); Bi = inv(B) +lam = [Q(1), Q(2), Q(-3), Q(5), Q(1, 7), Q(4)] +A2 = [[lam[i] * A[i][j] for j in range(6)] for i in range(6)]; B2 = [[B[i][j] / lam[j] for j in range(6)] for i in range(6)] +A2i = inv(A2); B2i = inv(B2) +same = True +for i in range(6): + for x in range(3): + for xp in range(3): + for y in range(3): + same &= (B[3 + y][i] * A[i][xp] == B2[3 + y][i] * A2[i][xp]) and (Ai[x][i] * A[i][xp] == A2i[x][i] * A2[i][xp]) and (B[3 + y][i] * Bi[i][3 + y] == B2[3 + y][i] * B2i[i][3 + y]) +ck(same, 'f_i, L_X,i and L_Y,i are invariant under a diagonal rescaling of the registers (A -> D A, B -> B D^-1)') +print('PASS_SCHUR_LEAK' if not fails else 'FAILED_SCHUR_LEAK') +sys.exit(1 if fails else 0) diff --git a/research/p104-duality-ceiling-flag-note/data/p104_pairs.json b/research/p104-duality-ceiling-flag-note/data/p104_pairs.json new file mode 100644 index 0000000000..103cf7a0a7 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/data/p104_pairs.json @@ -0,0 +1 @@ +{"ys": [43, 44, 35, 112, 34, 105, 13, 30], "zs": [40, 18, 76, 23, 90, 22, 0, 45]} \ No newline at end of file diff --git a/research/p104-duality-ceiling-flag-note/data/quotes.json b/research/p104-duality-ceiling-flag-note/data/quotes.json new file mode 100644 index 0000000000..5918b27cc8 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/data/quotes.json @@ -0,0 +1,49 @@ +{ + "pkg": [ + [ + "notes/general-clifford-frames.tex", + 16, + "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", + 68, + "$\\dim V-\\dim U$" + ], + [ + "notes/general-clifford-frames.tex", + 62, + "use one identical exact representative" + ], + [ + "upstream/build/sections/03-motifs.tex", + 154, + "assign an invertible $R$-linear operator" + ], + [ + "upstream/build/sections/03-motifs.tex", + 203, + "A label is a nondegenerate subspace of a fixed bilinear space" + ], + [ + "upstream/build/sections/04-swap.tex", + 115, + "A_e=M_{\\mathrm{head}(e)}-M_{\\mathrm{tail}(e)}" + ], + [ + "upstream/build/sections/04-swap.tex", + 197, + "the sum of the edge ranks" + ], + [ + "upstream/build/sections/05-layers.tex", + 82, + "The number of directional kernels is precisely" + ] + ] +} \ No newline at end of file diff --git a/research/p104-duality-ceiling-flag-note/verify.sh b/research/p104-duality-ceiling-flag-note/verify.sh new file mode 100755 index 0000000000..d139c9c385 --- /dev/null +++ b/research/p104-duality-ceiling-flag-note/verify.sh @@ -0,0 +1,4 @@ +#!/bin/sh +# Runs the exact checks; run from anywhere. Needs python3.12 only (standard library). +set -e +exec python3.12 -I -B "$(dirname "$0")/check.py"