From 15e8433c431aaaf7fa3756407d44f4700fc8377a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 00:46:11 +0100 Subject: [PATCH] feat(research): classify shared maps for three frame subspaces --- research/three-frame-shared-map/PROOF.md | 166 ++++++++++++ research/three-frame-shared-map/README.md | 110 ++++++++ research/three-frame-shared-map/RESULT.json | 115 +++++++++ research/three-frame-shared-map/SOURCES.json | 24 ++ research/three-frame-shared-map/TASK.json | 89 +++++++ research/three-frame-shared-map/VERIFY.json | 34 +++ research/three-frame-shared-map/verify.py | 250 +++++++++++++++++++ 7 files changed, 788 insertions(+) create mode 100644 research/three-frame-shared-map/PROOF.md create mode 100644 research/three-frame-shared-map/README.md create mode 100644 research/three-frame-shared-map/RESULT.json create mode 100644 research/three-frame-shared-map/SOURCES.json create mode 100644 research/three-frame-shared-map/TASK.json create mode 100644 research/three-frame-shared-map/VERIFY.json create mode 100644 research/three-frame-shared-map/verify.py diff --git a/research/three-frame-shared-map/PROOF.md b/research/three-frame-shared-map/PROOF.md new file mode 100644 index 0000000000..86aef55407 --- /dev/null +++ b/research/three-frame-shared-map/PROOF.md @@ -0,0 +1,166 @@ +# Shared invertible maps for three frame subspaces + +This is a scoped algebraic proof over every finite field F_q. The normal +form is classical three-subspace linear algebra. The contribution here is +an explicit compatibility and multiplicity contract for shared native maps. +No claim of literature priority is made for the normal form or its elementary +orbit-counting consequences. + +Let U=(U1,U2,U3) and W=(W1,W2,W3) be ordered triples in F_q^n. A realizing +map is G in GL_n(F_q) with G Ui=Wi for each i. The ordering matters. Put + +``` +di = dim Ui +pij = dim(Ui intersection Uj) +c = dim(U1 intersection U2 intersection U3) +s = dim(U1 + U2 + U3) +t = d1+d2+d3 - p12-p13-p23 + c - s. +``` + +For each subset S of {1,2,3}, define an integer m_S by + +``` +m_empty = n-s +m_123 = c +m_ij = pij-c +m_i = di-pij-pik+c-t, where {i,j,k}={1,2,3}. +``` + +All these integers and t are nonnegative, and sum_S m_S + 2t=n. + +**Compatibility theorem.** There is a realizing map exactly when the two +triples have identical values of n, the three di, the three pij, c and s. +Equivalently they have the same eight m_S and t. + +## A simultaneous normal form + +Let A_S denote a one-dimensional configuration in which Ui is the whole +line exactly when i belongs to S, and zero otherwise. Let D denote a +configuration on a plane with + +``` +U1 = , U2 = , U3 = . +``` + +Every ordered triple is a direct sum of m_S copies of A_S and t copies of D. +Here is a direct proof which works over arbitrary fields. + +First split off T=U1 intersection U2 intersection U3. Any linear section of +V/T takes each image Ui/T back into Ui, because T is contained in every Ui. +It therefore gives a simultaneous decomposition with dim(T) copies of A_123. +Work in the complementary configuration, whose triple intersection is zero. + +Write Pij=Ui intersection Uj. The sum S=P12+P13+P23 is direct. Indeed, a +relation p12+p13+p23=0 puts p23 in all three Ui, hence makes it zero, and +then the other terms vanish too. In V/S the images of the three Ui have +pairwise zero intersections. For example, if x in U1 and y in U2 have the +same quotient image, write x-y=p12+p13+p23. Then +x-p12-p13=y+p23 lies in P12, so x belongs to P12+P13 and its quotient image +is zero. The other cases follow by relabeling. + +For a pairwise-disjoint triple, put K=U3 intersection (U1+U2). The sum +U1+U2 is direct, so every z in K has a unique expression x+y. Both +projections from K to U1 and U2 are injective, since K meets either Ui +trivially. A basis z_k=x_k+y_k of K therefore gives t independent D planes. +Choose complements to the x_k in U1, the y_k in U2, and K in U3. These +complements are independent of each other and of those planes. A relation +would put its U3 part into K, then uniqueness in U1+U2 would make all parts +zero. They give the A_1, A_2 and A_3 summands. A complement to the total +sum gives A_empty. + +This decomposition also lifts through the previous quotient V/S. Choose +lifts x_k in U1, y_k in U2 and z_k in U3 for each quotient D relation. +If x_k+y_k-z_k=p12+p13+p23, replace x_k by x_k-p12-p13 and y_k by +y_k-p23. Their sum is now z_k, while all three vectors remain in their +required subspaces. Lift the remaining independent quotient basis vectors +arbitrarily inside their Ui. Their collective span is disjoint from S, +because their quotient vectors are a basis of V/S. Each Ui splits into its +lifted part and Ui intersection S, which is Pij+Pik. Thus S contributes +precisely the pair atoms, and the quotient decomposition lifts simultaneously. + +Counting intersections, individual dimensions and the total sum in this +normal form gives the formulas above. They also prove uniqueness of the +multiplicities. A realizing G preserves those dimensions, proving necessity. +Matching bases of equal normal-form summands constructs a realizing G, +proving sufficiency. + +## Exact number of realizing maps + +Define g_q(r)=product_(j=0)^(r-1)(q^r-q^j), with g_q(0)=1. Put + +``` +E = sum_(S subseteq T) m_S m_T + t^2 + + t (2m_empty + m_1+m_2+m_3 + m_12+m_13+m_23 + 2m_123) +R = E - sum_S m_S^2 - t^2. +``` + +If compatibility fails the number is zero. If it holds, the exact number is + +``` +q^R g_q(t) product_S g_q(m_S). +``` + +To prove the formula, an endomorphism of a configuration means a linear map +which sends every Ui into itself, without requiring invertibility. For the +one-dimensional atoms, Hom(A_S,A_T) has dimension one exactly when S is a +subset of T, and zero otherwise. Hom(A_S,D) has dimension two when S is +empty, one for a singleton, and zero otherwise. Hom(D,A_T) has dimension +two when T is full, one for a pair, and zero otherwise. An endomorphism of +D must preserve three distinct lines, so it is scalar. These statements +follow directly by choosing the images of e and f, and give the displayed E. + +Order the blocks as A_empty, the three singleton types, D, the three pair +types, A_123. Every allowable off-diagonal map runs forward in that order. +The whole endomorphism matrix is therefore block triangular. The diagonal +blocks are arbitrary m_S by m_S matrices, and the D-isotypic diagonal block +is B tensor I_2 for an arbitrary t by t matrix B. Consequently an +endomorphism is invertible exactly when each of these nine diagonal matrices +is invertible. The remaining R scalar parameters are unconstrained, giving +q^R choices. This proves the stabilizer formula. If G0 realizes U to W, +all realizers are exactly G0 times the stabilizer of U, so the same formula +counts them. No search through GL_n is needed to evaluate this number. + +## Number of compatibility types + +The normal-form multiplicities are arbitrary nonnegative integers satisfying +sum m_S+2t=n. Conversely each such tuple constructs a triple. There are +therefore + +``` +N(n) = sum_(t=0)^floor(n/2) binomial(n-2t+7,7) +``` + +ordered compatibility types, independently of q. At native ambient dimension +nine this gives 15,792 types. This is an exact enumeration of normal-form +tuples, not a literal enumeration of all nine-dimensional subspaces or +matrices. The finite checker enumerates all literal triples only in its +explicit small-field domains. + +## Why both extra invariants matter + +Three distinct coplanar lines and three independent lines in F_2^3 have +identical individual dimensions and all intersection dimensions. Their +sum dimensions differ, and their realizing-map stabilizers have orders four +and one respectively. Pairwise compatibility alone cannot impose all three +correspondences. + +Three coordinate planes in F_2^3 and three distinct planes through a fixed +line have the same individual dimensions, pairwise dimensions and total sum. +Their triple intersections have dimensions zero and one. Thus the triple +intersection cannot be dropped even when the total sum is retained. + +## Scope of the native-map application + +Cao Yifan's PR4610 package asks for simultaneous subspace-map consistency +when freeing its twelve prelude contracts together with late contacts. The +criterion answers the algebraic equality contract for any three ordered +subspaces. For two subspaces, setting U3=W3=0 reduces it to equality of +the two dimensions and the intersection dimension. + +An actual prelude can prescribe the action on individual vectors, include +more than three subspaces, or impose dual, phase or symplectic conditions. +Those are additional constraints. This theorem does not assert that the +15,792 classes exhaust such contracts, and it does not construct a changed +native word or decide the current construction's profitability. Arbitrary-input +semantics, absolute phase, paid contacts, restoration, hosting, precision, +tape costs and supplier admission remain separate obligations. diff --git a/research/three-frame-shared-map/README.md b/research/three-frame-shared-map/README.md new file mode 100644 index 0000000000..b0279f4835 --- /dev/null +++ b/research/three-frame-shared-map/README.md @@ -0,0 +1,110 @@ +# Exact shared-map compatibility for three frame subspaces + +For two ordered triples of subspaces in F_q^n, a common invertible map exists +exactly when their three individual dimensions, three pairwise intersection +dimensions, triple-intersection dimension and total-sum dimension agree. +[PROOF.md](PROOF.md) gives the exact number of realizing maps and a constructive +all-dimension proof. At ambient dimension nine there are exactly **15,792** +ordered compatibility types, independently of the finite field. + +This contribution was produced by Nick Petalas. Its claim type is a **scoped +proof with finite exact corroboration**. The classical three-subspace normal +form is background, with no literature-priority claim. The new repository +contribution is an explicit shared-native-map compatibility and multiplicity +contract, addressing the prelude-contact question in Cao Yifan's +[PR4610 package](../kappa-round3-warp-20261022/README.md). This is not a replay +or audit of that contributor's result. + +If m_S are the eight Boolean-atom multiplicities and t is the triangle +multiplicity defined in the proof, the number of realizers is zero for +incompatible triples and otherwise + +``` +q^R |GL_t(F_q)| product_S |GL_(m_S)(F_q)|, +``` + +where the proof gives R explicitly. Counting types gives +`sum_(t=0)^floor(n/2) binomial(n-2t+7,7)`. + +The literal checker constructs vector sets, all subspaces and every invertible +matrix in its declared domains. It computes complete orbits independently of +the invariant classifier, then compares compatibility and every orbit's map +multiplicities. The domains are F_2 in dimensions zero through three and +F_3 and F_5 in dimension two. They contain 4,958 ordered triples in total. +The binary dimension-three domain alone has 4,096 triples and 128 orbits. +All 15,792 dimension-nine normal-form tuples are separately enumerated and +reconstructed from their dimensions, with an ordered digest. No nine-dimensional +GL enumeration is claimed. Seven invalid-input controls +and two incomplete-invariant examples accompany the complete orbit checks. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/three-frame-shared-map/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/three-frame-shared-map +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/three-frame-shared-map --check-source-history +``` + +Expected direct output begins `PASS_THREE_FRAME_SHARED_MAP` and reports +`triples=4958`, `orbits=248`, `dimension_nine_orbits=15792`. The registered +manifest runs warning-strict normal and optimized checks. The receipt in +[RESULT.json](RESULT.json) is generated by the verifier and binds the six +local proof/metadata/code files to SHA256 hashes. To generate another receipt, +pass `--write /a/new/path.json`; an occupied path is rejected. No normal replay +writes into the checkout. The direct verifier also works without Git when +the package and its declared source input are exported together. + +## Evidence and limits + +[VERIFY.json](VERIFY.json) declares the exact replay commands. +[SOURCES.json](SOURCES.json) pins the predecessor README, original card and +selected-record provenance at main `624de9dc66858af0945e5f8a0942488d62280d43`. +The predecessor README is authenticated, not executed. The selected baseline +source-binding control passed with kappa `60403/20000000`; it is not a supplier +replay. [TASK.json](TASK.json) records the scope change from the rank-shape card +to this algebraic side result and the live coordination claim. + +The universal result rests on the written proof. Finite experiments are +corroboration. Independent human and formal proof-kernel review are unclaimed. +The dimension-nine count follows the proved normal-form enumeration, not a +nine-dimensional exhaustive matrix run. General vector-action constraints, +four or more subspaces, absolute phases, symplectic restrictions, actual +prelude integration, physical prices, changed paid profiles and a new kappa +are outside scope. The selected frontier is unchanged. + +The verifier uses finite sets and integers in Python. Managed-runtime +allocation is a Power of Ten deviation. Literal domains have at most 25 +vectors, 16 subspaces, 4,096 triples and 480 matrices; arithmetic dimensions +are capped at 64. All loops have finite bounds from these domains, no recursion +or dynamic evaluation is used, and runtime `require` checks remain active +under `-O`. Internal functions are below 60 lines. No performance comparison +or complete historical suite is claimed. + +## Open next questions + +1. Bind the criterion to one actual prelude/late shared-G contract in PR4610. + First identify whether that occurrence prescribes vector values or only + subspace images. Additional vector and phase constraints are the blocker. + This decides whether the algebraic freedom can remove paid work. +2. For four ordered subspaces, add the necessary relative-operator invariant + on the non-Boolean component. Start with two complementary planes and two + graph subspaces. Three-subspace dimension data no longer decide this domain; + a complete application-specific contract is needed before a new search. + +## Credit and background + +Credit Cao Yifan for PR4610's changed native-map/helper construction and its +shared-G prelude-contact question; Cinna Davis for the PR4470 supplier and +cumulative sources; Dugongue for transported warp frames; zxv for native and +compiler work; and Jacob Alan Sussman for mixed-target recursion. No predecessor +code or mathematical result was reverified for this package. + +The finite-dimensional three-subspace decomposition is classical. See +Masatoshi Enomoto and Yasuo Watatani, *Relative position of four subspaces in a +Hilbert space*, Section 7, for the nine indecomposable three-subspace systems +and the Gelfand-Ponomarev background: +[author manuscript](https://catalog.lib.kyushu-u.ac.jp/opac_download_md/3339/2004-1.pdf). +The proof here derives the required arbitrary-field statement and finite-field +map count directly. New material is Apache-2.0; predecessor credits are unchanged. diff --git a/research/three-frame-shared-map/RESULT.json b/research/three-frame-shared-map/RESULT.json new file mode 100644 index 0000000000..6d352afbe4 --- /dev/null +++ b/research/three-frame-shared-map/RESULT.json @@ -0,0 +1,115 @@ +{ + "claim_type": "scoped proof", + "controls": { + "incomplete_invariants_rejected": 2, + "invalid_inputs_rejected": 7 + }, + "dimension_nine_normal_forms": { + "count": 15792, + "tuple_sha256": "eaef301ff170fc700f405f0d5891d497d114a1517fafa9936820eacdfb0ce02b" + }, + "dimension_nine_orbits": 15792, + "literal_cases": [ + { + "GL": 1, + "classification_sha256": "3e246222729ed3a26d98bd726c1c82f390771036bfd5d2b3d61056cf95b32008", + "matrix_triple_images": 1, + "n": 0, + "orbits": 1, + "q": 2, + "stabilizer_histogram": { + "1": 1 + }, + "subspaces": 1, + "triples": 1 + }, + { + "GL": 1, + "classification_sha256": "1f0cf47b9422612e2d8e2ab5e880aa5c9cc0b99c9386a5ac878d49949946491c", + "matrix_triple_images": 8, + "n": 1, + "orbits": 8, + "q": 2, + "stabilizer_histogram": { + "1": 8 + }, + "subspaces": 2, + "triples": 8 + }, + { + "GL": 6, + "classification_sha256": "0b5e6d5962574752a1a61c04615c129236a5871ff5fb8c9f4f1bdc7aef0825ba", + "matrix_triple_images": 222, + "n": 2, + "orbits": 37, + "q": 2, + "stabilizer_histogram": { + "1": 10, + "2": 19, + "6": 8 + }, + "subspaces": 5, + "triples": 125 + }, + { + "GL": 168, + "classification_sha256": "0581acb22a56f6bba6de7109999d6dfbb07ef0e4f8dacda6871f08c1f0ada381", + "matrix_triple_images": 21504, + "n": 3, + "orbits": 128, + "q": 2, + "stabilizer_histogram": { + "1": 2, + "168": 8, + "2": 18, + "24": 38, + "4": 26, + "6": 18, + "8": 18 + }, + "subspaces": 16, + "triples": 4096 + }, + { + "GL": 48, + "classification_sha256": "865a173500b17e8322a8d7c55407bcccadfaae11e5f485bb46a1aec8cfaaa8b9", + "matrix_triple_images": 1776, + "n": 2, + "orbits": 37, + "q": 3, + "stabilizer_histogram": { + "12": 19, + "2": 1, + "4": 9, + "48": 8 + }, + "subspaces": 6, + "triples": 216 + }, + { + "GL": 480, + "classification_sha256": "3f5219fcd7fba346a4523e7577cdacf0bb5604869604f6308eda9d4a3b6d6444", + "matrix_triple_images": 17760, + "n": 2, + "orbits": 37, + "q": 5, + "stabilizer_histogram": { + "16": 9, + "4": 1, + "480": 8, + "80": 19 + }, + "subspaces": 8, + "triples": 512 + } + ], + "schema": "three-frame-shared-map/v1", + "source_sha256": { + "PROOF.md": "cbe916ebae3637963c4aaeeeb25948bdb704221073b201eac562aeeba828db9a", + "README.md": "cfff0b64130a6e55246c3479cd42708bcd3d8c9a5d6e8e53517d7c1b39108837", + "SOURCES.json": "d0763b354c8a8908c4d18d6d39b01a9cdcb9fd4e079eb35d0b8a4fb9bd28f0d1", + "TASK.json": "83e8b7f7f808e8ff8438815dfa72369007496cbbc300fd947ef5c7fd66e4d692", + "VERIFY.json": "8e11c8b04c16fc38184329cf3582fda804780f8a5fa26b8a8fb1d68f9066ca1c", + "verify.py": "8fc4321e80e166c7daba9430a636c4546c6214707414dcf090de7587df35639f" + } +} diff --git a/research/three-frame-shared-map/SOURCES.json b/research/three-frame-shared-map/SOURCES.json new file mode 100644 index 0000000000..4d1fac6254 --- /dev/null +++ b/research/three-frame-shared-map/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/kappa-round3-warp-20261022/README.md", + "usage": "input", + "git_blob": "e4c18ea0926e0502e6dce637a15a104cccf05624", + "sha256": "6cfcd49a0601f5b1f184a2567fc35dcb0a5c28eb06fce5e510d54895e8d17fde" + } + ] +} diff --git a/research/three-frame-shared-map/TASK.json b/research/three-frame-shared-map/TASK.json new file mode 100644 index 0000000000..6b60f43924 --- /dev/null +++ b/research/three-frame-shared-map/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact compatibility and realizing-map counts for three ordered subspaces over a finite field.", + "scope_change_reason": "The live PR4610 open question asks for shared native-map consistency at prelude contacts. This isolates a new algebraic interface obligation rather than searching the card's fixed decoder or repeating predecessor checks.", + "bottleneck_link": "A common native G must realize all frame correspondences; matching dimensions separately can admit impossible combinations. This side result removes the algebraic equality gap for up to three subspace correspondences, without claiming a paid-profile gain.", + "budget_minutes": 60, + "stop_rule": "Stop at the first complete compatibility and multiplicity proof plus its bounded literal corroboration. No native-word optimization or predecessor replay.", + "outcome": "completed", + "evidence": "PROOF.md; generated RESULT.json; exhaustive literal GL orbits for F2 dimensions 0..3 and F3/F5 dimension 2.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one actual PR4610 prelude contract use the three-subspace criterion?", + "why_it_matters": "It could expose genuinely consistent shared native-map freedom.", + "first_step": "Identify one actual G occurrence and translate every contact to subspace-image or vector-action constraints.", + "blocked_by": "Actual contacts can impose vector and phase conditions beyond this theorem." + }, + { + "question": "Which relative-operator invariant completes a four-subspace native contract?", + "why_it_matters": "Three-subspace dimension signatures do not classify arbitrary larger contracts.", + "first_step": "Study two complementary subspaces and two graph subspaces with a specified field and dimensions.", + "blocked_by": "A concrete source-compatible four-contact contract is not supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134607", + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit" + }, + "upstream_checkpoint": { + "commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "checked_at_utc": "2026-10-22T23:37:40Z" + } +} diff --git a/research/three-frame-shared-map/VERIFY.json b/research/three-frame-shared-map/VERIFY.json new file mode 100644 index 0000000000..7430234353 --- /dev/null +++ b/research/three-frame-shared-map/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-round3-warp-20261022/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete literal small-field orbit classification, exact realizing-map counts, generated proof/source hashes and rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same certificate and checks with Python assertions disabled." + } + ] +} diff --git a/research/three-frame-shared-map/verify.py b/research/three-frame-shared-map/verify.py new file mode 100644 index 0000000000..d5162db67e --- /dev/null +++ b/research/three-frame-shared-map/verify.py @@ -0,0 +1,250 @@ +"""Exact three-frame shared-map counts. No predecessor imports.""" + +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import combinations, product +import json +from math import comb +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +SOURCE_NAMES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def gl_order(q, n): + require(type(q) is int and 2 <= q <= 256, "field size outside arithmetic bound") + require(type(n) is int and 0 <= n <= 64, "dimension outside arithmetic bound") + value = 1 + for i in range(n): + value *= q ** n - q ** i + return value + + +def multiplicities(n, dims, pairs, common, total): + """Return Boolean atoms in mask order, then the two-dimensional triangle.""" + require(len(dims) == len(pairs) == 3, "expected three dimensions and intersections") + values = (n, *dims, *pairs, common, total) + require(all(type(x) is int and 0 <= x <= 64 for x in values), "invalid dimension") + d1, d2, d3 = dims + p12, p13, p23 = pairs + triangle = sum(dims) - sum(pairs) + common - total + atoms = (n - total, + d1 - p12 - p13 + common - triangle, + d2 - p12 - p23 + common - triangle, + p12 - common, + d3 - p13 - p23 + common - triangle, + p13 - common, p23 - common, common) + require(min(*atoms, triangle) >= 0, "infeasible dimension data") + require(sum(atoms) + 2 * triangle == n, "normal-form dimension mismatch") + return atoms, triangle + + +def stabilizer(q, atoms, triangle): + require(len(atoms) == 8, "expected eight Boolean atoms") + require(all(type(x) is int and 0 <= x <= 64 for x in (*atoms, triangle)), + "invalid multiplicity") + n = sum(atoms) + 2 * triangle + require(n <= 64, "normal form too large") + end_dimension = sum(atoms[s] * atoms[t] + for s in range(8) for t in range(8) if s & t == s) + end_dimension += triangle * (2 * atoms[0] + atoms[1] + atoms[2] + atoms[4] + + atoms[3] + atoms[5] + atoms[6] + 2 * atoms[7]) + end_dimension += triangle ** 2 + free_entries = end_dimension - sum(x * x for x in atoms) - triangle ** 2 + require(free_entries >= 0, "negative off-diagonal dimension") + value = q ** free_entries * gl_order(q, triangle) + for m in atoms: + value *= gl_order(q, m) + require(gl_order(q, n) % value == 0, "stabilizer does not divide GL") + return value + + +def add(x, y, q): + return tuple((a + b) % q for a, b in zip(x, y, strict=True)) + + +def span(vectors, q, n): + require(q in (2, 3, 5) and 0 <= n <= 3 and q ** n <= 25, + "literal experiment outside fixed domain") + require(len(vectors) <= 3 * q ** n, "too many span generators") + result = frozenset({(0,) * n}) + for v in vectors: + multiples = [tuple(c * x % q for x in v) for c in range(q)] + result = frozenset(add(x, y, q) for x in result for y in multiples) + return result + + +def spaces(q, n): + vectors = tuple(product(range(q), repeat=n)) + found = {frozenset({(0,) * n})} + for _ in range(n): + previous = tuple(found) + for space in previous: + for v in vectors: + found.add(span((*space, v), q, n)) + return tuple(sorted(found, key=lambda x: (len(x), sorted(x)))), vectors + + +def dimension(space, q, n): + candidates = [i for i in range(n + 1) if q ** i == len(space)] + require(len(candidates) == 1, "set is not a subspace size") + return candidates[0] + + +def signature(triple, q, n): + dims = tuple(dimension(x, q, n) for x in triple) + pairs = tuple(dimension(triple[i] & triple[j], q, n) + for i, j in combinations(range(3), 2)) + common = dimension(triple[0] & triple[1] & triple[2], q, n) + total = dimension(span(tuple(set().union(*triple)), q, n), q, n) + return multiplicities(n, dims, pairs, common, total) + + +def matrix_action(columns, v, q, n): + return tuple(sum(columns[j][i] * v[j] for j in range(n)) % q + for i in range(n)) + + +def permutations(q, n, subspaces, vectors): + indices = {s: i for i, s in enumerate(subspaces)} + result = [] + for columns in product(vectors[1:], repeat=n): + if len(span(columns, q, n)) == q ** n: + permutation = tuple(indices[frozenset(matrix_action(columns, v, q, n) + for v in s)] for s in subspaces) + result.append(permutation) + require(len(result) == gl_order(q, n), "literal GL enumeration incomplete") + return result + + +def orbit_check(q, n): + subspaces, vectors = spaces(q, n) + actions = permutations(q, n, subspaces, vectors) + signatures = {t: signature(tuple(subspaces[i] for i in t), q, n) + for t in product(range(len(subspaces)), repeat=3)} + unseen = set(signatures) + seen_signatures = set() + histogram = Counter() + digest = sha256() + applications = 0 + # Each iteration removes at least one triple; the for loop is explicitly bounded. + for representative in sorted(signatures): + if representative not in unseen: + continue + images = Counter(tuple(p[i] for i in representative) for p in actions) + applications += len(actions) + key = signatures[representative] + require(key not in seen_signatures, "same invariant in two GL orbits") + seen_signatures.add(key) + predicted = stabilizer(q, *key) + require(images[representative] == predicted, "wrong literal stabilizer") + require(len(images) * predicted == len(actions), "wrong orbit size") + for image, count in sorted(images.items()): + require(signatures[image] == key, "invariant changed under GL") + require(count == predicted, "wrong realizing-map multiplicity") + digest.update(repr((representative, image, count)).encode("ascii")) + unseen.difference_update(images) + histogram[predicted] += 1 + require(not unseen, "uncovered triples") + expected_orbits = sum(comb(n - 2 * t + 7, 7) for t in range(n // 2 + 1)) + require(len(seen_signatures) == expected_orbits, "normal-form count mismatch") + return {"q": q, "n": n, "subspaces": len(subspaces), "triples": len(signatures), + "GL": len(actions), "orbits": expected_orbits, + "matrix_triple_images": applications, + "stabilizer_histogram": {str(k): v for k, v in sorted(histogram.items())}, + "classification_sha256": digest.hexdigest()} + + +def controls(): + cases = [(lambda: multiplicities(2, (1, 1, 1), (0, 0, 0), 0, 4)), + (lambda: multiplicities(2, (1, 1), (0, 0, 0), 0, 2)), + (lambda: multiplicities(2, (True, 1, 1), (0, 0, 0), 0, 2)), + (lambda: stabilizer(2, (0,) * 8, -1)), + (lambda: gl_order(1, 2)), (lambda: gl_order(2, 65)), + (lambda: span((), 7, 2))] + for f in cases: + try: + f() + except ValueError: + continue + raise ValueError("invalid input accepted") + a = multiplicities(3, (1, 1, 1), (0, 0, 0), 0, 2) + b = multiplicities(3, (1, 1, 1), (0, 0, 0), 0, 3) + require(a != b and stabilizer(2, *a) == 4 and stabilizer(2, *b) == 1, + "sum-dimension discrimination failed") + c = multiplicities(3, (2, 2, 2), (1, 1, 1), 0, 3) + d = multiplicities(3, (2, 2, 2), (1, 1, 1), 1, 3) + require(c != d, "triple-intersection discrimination failed") + return {"invalid_inputs_rejected": len(cases), "incomplete_invariants_rejected": 2} + + +def source_hashes(): + root = PACKAGE.parents[1] + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + require(sha256((root / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "source drift: " + row["path"]) + return {name: sha256((PACKAGE / name).read_bytes()).hexdigest() for name in SOURCE_NAMES} + + +def nine_dimensional_types(): + """Enumerate normal-form tuples, never nine-dimensional subspace matrices.""" + count = 0 + digest = sha256() + for triangle in range(5): + total = 9 - 2 * triangle + for bars in combinations(range(total + 7), 7): + ends = (-1, *bars, total + 7) + atoms = tuple(ends[i + 1] - ends[i] - 1 for i in range(8)) + dims = tuple(sum(atoms[s] for s in range(8) if s & (1 << i)) + triangle + for i in range(3)) + pairs = tuple(atoms[(1 << i) | (1 << j)] + atoms[7] + for i, j in combinations(range(3), 2)) + require(multiplicities(9, dims, pairs, atoms[7], 9 - atoms[0]) + == (atoms, triangle), "normal-form tuple reconstruction failed") + digest.update(repr((atoms, triangle)).encode("ascii")) + count += 1 + require(count == sum(comb(9 - 2 * t + 7, 7) for t in range(5)) == 15792, + "dimension-nine normal-form enumeration changed") + return {"count": count, "tuple_sha256": digest.hexdigest()} + + +def certificate(): + cases = [orbit_check(q, n) for q, n in ((2, 0), (2, 1), (2, 2), + (2, 3), (3, 2), (5, 2))] + nine = nine_dimensional_types() + return {"schema": "three-frame-shared-map/v1", "claim_type": "scoped proof", + "source_sha256": source_hashes(), "literal_cases": cases, + "dimension_nine_orbits": nine["count"], + "dimension_nine_normal_forms": nine, "controls": controls()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="create a new receipt, never overwrite") + args = parser.parse_args() + result = certificate() + if args.write is None: + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "receipt differs from regenerated certificate") + else: + with args.write.open("x", encoding="utf-8") as handle: + handle.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + print("PASS_THREE_FRAME_SHARED_MAP", json.dumps( + {"triples": sum(c["triples"] for c in result["literal_cases"]), + "orbits": sum(c["orbits"] for c in result["literal_cases"]), + "dimension_nine_orbits": result["dimension_nine_orbits"]}, sort_keys=True)) + + +if __name__ == "__main__": + main()