From a736cc61b1436ddb5b8689398e28f51021177839 Mon Sep 17 00:00:00 2001 From: apoursh <8867770+apoursh@users.noreply.github.com> Date: Wed, 28 Oct 2026 01:23:24 -0400 Subject: [PATCH] Classify all usable positive rank-one frames and exact word lengths --- research/bit-positive-frame-use/PROOF.md | 226 ++++++++++ research/bit-positive-frame-use/README.md | 149 +++++++ research/bit-positive-frame-use/SOURCES.json | 36 ++ research/bit-positive-frame-use/TASK.json | 74 +++ research/bit-positive-frame-use/VERIFY.json | 38 ++ .../bit-positive-frame-use/independent.py | 420 ++++++++++++++++++ research/bit-positive-frame-use/verify.py | 139 ++++++ 7 files changed, 1082 insertions(+) create mode 100644 research/bit-positive-frame-use/PROOF.md create mode 100644 research/bit-positive-frame-use/README.md create mode 100644 research/bit-positive-frame-use/SOURCES.json create mode 100644 research/bit-positive-frame-use/TASK.json create mode 100644 research/bit-positive-frame-use/VERIFY.json create mode 100644 research/bit-positive-frame-use/independent.py create mode 100644 research/bit-positive-frame-use/verify.py diff --git a/research/bit-positive-frame-use/PROOF.md b/research/bit-positive-frame-use/PROOF.md new file mode 100644 index 0000000000..0580cc135f --- /dev/null +++ b/research/bit-positive-frame-use/PROOF.md @@ -0,0 +1,226 @@ +# Which positive rank-one additions can occur at all? + +Proof by **apoursh**, with substantial OpenAI Codex assistance. Apache-2.0. + +This proof is self-contained in the established formal register model. It imports no theorem, executable, certificate or pending Git object from PR6079. The determinant method is credited to Nick Petalas's PR2910; the target, model, support and first-order methods retain the PR2085/2112/6032 attribution. + +## Statement + +Put + +$$ + A=\begin{pmatrix}1&0\\0&0\end{pmatrix},\quad + B=\begin{pmatrix}0&0\\0&1\end{pmatrix},\quad + P=\frac12\begin{pmatrix}1&1\\1&1\end{pmatrix},\quad + Q=\frac12\begin{pmatrix}1&-1\\-1&1\end{pmatrix}. +$$ + +Thus $A+B=P+Q=I_2$, and each of these four addresses has trace one. Fix a **nonzero positive semidefinite symmetric rational matrix $R$ of rank one**. Let $\Lambda=\mathbb ZA+\mathbb ZB+\mathbb ZP+\mathbb ZR$, an additive subgroup of $\operatorname{Sym}_2(\mathbb Q)$. Work in the commutative formal group algebra $K=\mathbb F_2[\Lambda]$, where $[F][G]=[F+G]$. Distinct rational addresses index distinct basis monomials; the exponents are not reduced modulo two or identified through a finite representation. + +For every finite $w\ge4$, allow paid calls + +$$ + D_N(F)=I_w+([F]-1)N, + \qquad F\in\{A,B,P,Q,R\},\quad + N\in M_w(\mathbb F_2),\quad N^2=N,\quad\operatorname{rank}N=1. +$$ + +Arbitrary address-independent matrices in $\operatorname{GL}_w(\mathbb F_2)$ may be interspersed at zero cost. Require exact equality of the whole register matrix with + +$$ + T_w=\operatorname{diag}([A+P],[A+Q],[B+P],[B+Q],1,\ldots,1). +$$ + +All roles start arbitrary. The extra $w-4$ roles are dirty workspace and must be restored exactly; they need not stay unchanged during the word. Inverse labels, address-dependent free matrices, clean-only initialization, and discarded roles are not included. + +Call $R$ **usable** if some such finite exact word contains at least one call labelled $R$. There is no length bound in this definition. + +**Theorem.** For every finite $w\ge4$: + +1. $R$ is usable if and only if $R=F/m$ for an address $F\in\{A,B,P,Q\}$ and a positive integer $m$. +2. For $R=F/m$, the complete set of attainable total call counts among exact words required to use $R$ is exactly $\{m+7,2m+6\}$. In particular, the minimum is $m+7$. The two counts coincide when $m=1$. +3. Every exact word using $R=F/m$ has one of the three necessary multiplicity profiles below, in order $(F,F^\perp,G,H,R)$, where $F^\perp$ is its mate in the old orthogonal pair and $G,H$ are the other pair: + +$$ + (1,2,2,2,m),\qquad + (0,2,2,2,2m),\qquad + (0,1,3,3,m). \tag{P} +$$ + +The first two profiles are attained by explicit subdivision words. The third is only a necessary candidate; its realizability for $m\ge2$ is **not asserted**. Accordingly, (P) is a complete necessary list, not a claimed classification of attainable count profiles. + +When $m=1$, $R$ duplicates an old address. One may distinguish the name of the extra label for the required-use statement; the operation and its cost are unchanged. Ignoring $R$ always gives the ordinary eight-call construction. For $m>1$, requiring use of the extra frame strictly raises the optimum. + +## 1. Determinants and removal of free mixing + +A rank-one binary idempotent has the form $N=xy^T$, with $y^Tx=1$. The matrix determinant lemma over the commutative ring $K$ gives + +$$ + \det D_N(F)=1+([F]-1)y^Tx=[F]. +$$ + +Every invertible binary matrix has determinant one. Thus, if $a,b,p,q,r$ count calls at $A,B,P,Q,R$, exact endpoint equality implies + +$$ + aA+bB+pP+qQ+rR=4I_2. \tag{1} +$$ + +This is exact rational-matrix equality, because it follows from equality of formal basis monomials. It is the determinant invariant already used in PR2910, not a new general identity. + +For the remaining arguments, move free binary matrices through paid factors by conjugation. Rank-one idempotence and the address label are preserved. The word becomes a product of paid factors followed by one free binary matrix $G$. Under augmentation $[F]\mapsto1$, every paid factor and the target become identity, so $G=I_w$. Consequently the support and first-order arguments may assume only paid factors, without restricting the permitted free mixing. + +In particular these arguments retain the full $w$-dimensional projectors. They do not incorrectly replace a projector by its compression to the first four roles. + +## 2. At every word length, a usable positive direction must be old + +Suppose $r\ge1$. Set + +$$ + n=a+b+p+q,\qquad d=a-b,\qquad e=p-q. +$$ + +Since $\operatorname{tr}R>0$, the trace of (1) gives $n<8$, independently of the total number $n+r$ of calls. Subtracting the old frames entry by entry yields + +$$ + 2rR= + \begin{pmatrix}8-n-d&-e\\-e&8-n+d\end{pmatrix}. +$$ + +The rank-one condition and nonnegative old counts imply + +$$ + d^2+e^2=(8-n)^2,\qquad |d|+|e|\le n. \tag{2} +$$ + +Because $8-n>0$, + +$$ + 8-n=\sqrt{d^2+e^2}\le |d|+|e|\le n, +$$ + +so $4\le n\le7$. The only possible circle radii are therefore $8-n\in\{1,2,3,4\}$. These four integer circles have only axial integer points. Substitution shows + +$$ + rR=(8-n)F\quad\text{for some }F\in\{A,B,P,Q\}. \tag{3} +$$ + +Therefore every usable positive frame has the form $R=cF$, $c>0$. This already excludes every positive direction outside the four old directions at every finite word length and workspace width. + +The small-circle assertion can be checked by listing squares up to sixteen. It is the entire uniform reduction, not a bounded search in rational slopes or word lengths. + +## 3. Exact symmetries reduce to $R=cA$ + +The rational similarity maps induced by + +$$ + J=\begin{pmatrix}0&1\\1&0\end{pmatrix},\qquad + H=\begin{pmatrix}1&1\\1&-1\end{pmatrix},\quad H^{-1}=H/2, +$$ + +preserve the four old frames. Conjugation by $J$ swaps $A,B$ and fixes $P,Q$; conjugation by $H$ swaps $A,P$ and swaps $B,Q$. They act transitively on the four addresses. In target order $(A+P,A+Q,B+P,B+Q)$, the induced permutations are respectively $(1\ 3)(2\ 4)$ and $(2\ 3)$, using one-based positions. + +Applying either address isomorphism to every formal monomial and then the corresponding active-role permutation takes exact admissible words to exact admissible words, preserving counts and restored dirty roles. This is a proof isomorphism between cases, not a free address-transformation operation being added to the model. We may therefore prove the remaining assertions for $R=cA$, with $c>0$. + +## 4. A denominator-independent character leaves three count patterns + +Equation (1), now with $R=cA$, gives + +$$ + p=q=s,\qquad b=4-s,\qquad a+rc=b. \tag{4} +$$ + +Since $r,c>0$, $0\le a0$. Therefore + +$$ + u_B=u_Q=0,\qquad u_P=1,\qquad u_A+cu_R=1. \tag{6} +$$ + +If $a=0$ globally, then $u_A=0$; (6) gives $c=1/u_R$, where $u_R$ is a positive integer. If $a>0$, (5) forces $(a,b,p,q)=(1,2,2,2)$, and (4) gives $rc=1$, again $c=1/r$. In every case + +$$ + c=1/m\quad\text{for a positive integer }m. +$$ + +Substituting into (4) and (5) gives exactly the necessary profiles (P): respectively $r=m,2m,m$. Their lengths are $m+7,2m+6,m+7$. Thus every exact word using $R$ has total length in $\{m+7,2m+6\}$, and since $m\ge1$, every such word has at least $m+7$ calls. + +For $m=1$, the third profile is impossible. In the canonical case $R=A$, the old-lattice character with values $\chi(A)=\chi(B)=1$ and $\chi(P)=\chi(Q)=0$ sends every target to one. That profile has only one $R$ call and one $B$ call detected by this character, so its first-order coefficient has rank at most two, whereas $D_w$ has rank four. The other directions follow by the exact symmetries. The remaining count-profile question starts at $m=2$. + +## 6. Sharp construction, valid at every width + +The ordinary eight-call construction uses coordinate-projector label pairs $(A,P),(A,Q),(B,P),(B,Q)$ on the four active roles. All other roles remain identity. For any idempotent $E$, + +$$ + D_E(U)D_E(V)=D_E(U+V), +$$ + +because the complementary summands $E$ and $I-E$ multiply orthogonally. Hence for $R=F/m$, + +$$ + D_E(R)^m=D_E(mR)=D_E(F). +$$ + +Replace one of the two $F$-labelled coordinate calls in the direct construction by $m$ consecutive $R$ calls. The new exact word has $7+m$ calls and uses the extra label. Replacing both such calls realizes profile $(0,2,2,2,2m)$ at length $6+2m$. These words work for every finite $w\ge4$, with all workspace unchanged. Both lengths in the necessary spectrum are therefore attained. This proves usability, the exact spectrum $\{m+7,2m+6\}$, and the required-use minimum. For $m=1$, the distinction between calls named $F$ and calls named $R$ is retained when counting profiles; both constructions use eight operations and the spectrum is the singleton $\{8\}$. + +The result does not say that every admissible word is literally a subdivided direct word. It classifies the additional addresses that may occur, proves their exact possible total call counts and optimal required-use cost, and supplies a necessary count-profile list. No realization is asserted for the third profile in (P) when $m\ge2$; $m=1$ was excluded above. + +## Scope, boundaries and contribution beyond PR6079 + +PR6079 excludes words of at most seven calls for one arbitrary signed rational rank-one addition. That minimum-eight result does not decide which positive additions can appear in longer exact words. The present proof answers that all-length question: the only usable positive additions are reciprocal-integer subdivisions of the four original directions, and the exact possible total call counts are $\{m+7,2m+6\}$, with optimum $m+7$. The proof here reconstructs all needed invariants directly from the canonical predecessor model and needs no PR6079 code or result as an input. + +The positivity and single-added-frame hypotheses are substantive. The zero frame gives an identity call and is excluded from the classification. A negative frame such as $-A$ can appear by appending an $A,-A$ cancellation pair to the direct word, so the positive classification must not be asserted for signed frames. Two or more positive added frames change the determinant rank-one reduction; no conclusion is made for that model. Clean ancillas, disposal, address-dependent free mixing, finite evaluated representations, changed endpoints, and native/consumer pricing remain outside scope. + +This is a scoped formal-model theorem, not a new native supplier, kappa improvement, all-size multiplication theorem, formal-kernel verification or independent human review. Finite checks should corroborate the forty determinant-compatible old-count profiles, exact source/target symmetries, the denominator-independent character, the three symbolic multiplicity families and the attaining subdivision words. A bounded integer-m grid cannot itself prove the all-length or all-workspace statements; those follow from the argument above. + +Credit Cinna Davis's PR2085/2112 for the model and endpoint; Nick Petalas's PR2910 for the earlier fixed-frame determinant obstruction and arbitrary dirty-workspace treatment, and PR6032 for its support/first-order approach and open alphabet question; Philippe Van Velzen's earlier fixed-frame exact-eight finding as retained in PR2910; and the retained BIT predecessor lineage. The standard determinant, support expansion and character/rank arguments are inherited techniques. The new conclusion is the all-length positive-frame classification, exact total-length spectrum and sharp required-use tariff. diff --git a/research/bit-positive-frame-use/README.md b/research/bit-positive-frame-use/README.md new file mode 100644 index 0000000000..07795968f3 --- /dev/null +++ b/research/bit-positive-frame-use/README.md @@ -0,0 +1,149 @@ +# Classify every usable positive rank-one frame + +**Scoped proof, with sharp constructions.** For the four-target formal +register endpoint of PR2085, one additional positive rational rank-one +frame is usable in an exact word **if and only if** it is `R=F/m`, where +`F` is one of the four original frames and `m` is a positive integer. +Among words that use it, the exact possible total lengths are + +``` +{m+7, 2m+6}. +``` + +The minimum is therefore `m+7`. The result holds with arbitrary finite +restored dirty workspace and address-independent binary mixing. It has no +word-length cutoff. The ordinary eight-call construction remains available +when use of the added frame is optional. This is not a native supplier or +an improvement to the selected multiplication bound. + +[PROOF.md](PROOF.md) gives the complete model, universal proof and both +attaining constructions. It retains the formal group algebra of rational +symmetric address matrices and paid factors `I+([F]-1)N`, with binary +rank-one idempotent `N`. Exact equality is imposed on all roles. Positive +means nonzero positive semidefinite; zero and negative frames are excluded +from the classification, as are two added frames and changed endpoints. + +The old frames are `A=diag(1,0)`, `B=diag(0,1)`, +`P=(1/2)[[1,1],[1,1]]`, and `Q=(1/2)[[1,-1],[-1,1]]`. +The target is `diag([A+P],[A+Q],[B+P],[B+Q],1,...)`. +For example, `R=A/3` can be used in words of exactly 10 or 12 calls; +`R=2A/3` and every positive off-axis rank-one frame cannot be used at all. + +## What the proof adds + +PR2910 already forbids the fixed dyadic extra frame at every length. +PR6032 handles the normalized rational-slope minimum, and PR6079 excludes +all words shorter than eight for any one signed scaled frame. None of +those results classifies which positive frames may occur in longer words. +This package supplies that classification and its exact length spectrum. + +The determinant identity bounds the number of **old** calls below eight +whenever the positive extra frame is used, even if the total word is long. +The resulting integer circles force an old direction. A character that +annihilates the entire rational added line leaves three possible count +patterns; exponent support forces reciprocal-integer scaling. Subdividing +one or both matching calls in the direct word attains both lengths. + +The three multiplicity patterns in PROOF.md are a complete **necessary** +list. The first two are constructed; the third is not asserted to be +realizable. This distinction does not affect the exact length spectrum. +When `m=1`, the added label duplicates an old address and both lengths +collapse to eight. + +## Reproduce + +Python 3.12, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/bit-positive-frame-use +python3.12 -I -W error -B research/bit-positive-frame-use/verify.py +python3.12 -I -O -W error -B research/bit-positive-frame-use/verify.py +``` + +The registered runner executes normal and optimized modes. The direct +verifier needs only this package and its three declared predecessor READMEs, +and neither Git nor network access. It checks their hashes, then compiles +the literal local checker bytes instead of importing cached bytecode. + +The independent checker derives the determinant families from all 330 old +multiplicity quadruples of total at most seven, obtaining 40 families and +12 survivors of the rank condition. These are not the same 40 count tuples +as PR6079's short-word census. The checker supplies 48 exact support-weight certificates that reduce the +unbounded extra-call count to one divisibility condition. Corroboration +covers 3,840 parameter support checks, 40 reciprocal-scale fixtures, 212 rejected +nonreciprocal-scale fixtures, and 20 rejected rotated frames. It multiplies 128 +one-/two-subdivision words and 128 freely conjugated versions, for all four +directions, m in {1,2,3,4,5,7,8,12} and widths 4/6, including temporary +dirty-role writes. All 577 dropped/extra-call, incorrect-fraction, wrong- +direction, dirty-restoration and non-idempotent mutants are rejected. + +The primary checks independently verify both rational alphabet/endpoint +symmetries, the four denominator-safe lattice characters, all eight integer +circle domains, and the three residual patterns. Controls include a +nonintegral character that cannot be reduced modulo two, manually computed +noncommuting products, and a negative-frame identity loop outside the +positivity hypothesis. Finite parameter/role grids test the implementation; +the statements for all denominators, word lengths and workspace widths +follow from PROOF.md. + +Local environment: CPython 3.12.14, macOS arm64. Source metadata, normal and +optimized verification, and publication/export integrity are checked +separately. No native tariff, formal-kernel proof, independent human +acceptance or new selected-frontier cold replay is claimed. + +## Task, overlap and sources + +Canonical base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8; +chooser seed `9da5de6c63f0e0f69135ef2d1c7c085d`. The selected binding-only +orientation passed after materializing its pinned files; it does not +validate the full selected construction. + +Task `bit-new-register-model`, scope key `7084092dd726e7ba1f2f`, +**scope changed** to PR6079's all-length positive-use question. This is a +formal alphabet classification, rather than the card's native +larger/nonabelian supplier. The full original card, relevance and stopping +rule are retained in [TASK.json](TASK.json). +[Canonical claim/status](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19233896). + +Live all-state searches on 2026-10-28 for rank-one/reciprocal and scaled/frame +PRs, the current handoff and PR6079 were inspected. The local offline helper +searched 18 of 8,348 note records and had no usable remote cache. No matching +all-length classification was found; this limited coverage is not proof of +novelty or a survey of unpublished work. + +| Predecessor | Inspected head | Retained contribution | +|---|---|---| +| [PR2085](https://github.com/CrocSwap/integer-mult-bounds/pull/2085) | `5302b9bad6345413a0cabb0afd926d84e44c12e3` | Endpoint, model, augmentation method | +| [PR2910](https://github.com/CrocSwap/integer-mult-bounds/pull/2910) | `26ce4ed46112438b237fab54e6da1953c1d16174` | Earlier determinant obstruction and arbitrary dirty workspace | +| [PR6032](https://github.com/CrocSwap/integer-mult-bounds/pull/6032) | `3b098803eb854afbd5d63ad3bf4d75cdb1e515d5` | Support method, normalized slopes, alphabet question | +| [PR6079](https://github.com/CrocSwap/integer-mult-bounds/pull/6079) | `44745c427f710e406cb2d2c6de458b7f93d81f01` | Motivating all-length open question; signed minimum-eight result | + +[SOURCES.json](SOURCES.json) pins the first three canonical READMEs. PR6079 +is pending context only: no theorem, code, certificate or Git object from +it is required to replay or prove this result. All needed invariants are +rederived here, so this package can be reviewed independently. + +## Open next questions + +Structured relevance, first steps and blockers are in TASK.json. + +1. Can **two** positive added rank-one frames enable a saving? Begin with + the joint determinant equation and target exponent supports. The + single-frame rank-one residual argument no longer applies; an exact + word and full native invoice are required for a multiplication gain. +2. For reciprocal subdivisions, is the third necessary count profile + `(0,1,3,3,m)` realizable for any `m>=2`? The proof excludes `m=1`. + Start at `m=2`, or find a coefficient obstruction uniform in `m`. This would classify count-profile realizability; it + cannot improve the minimum or length spectrum already settled here. + +## Credit + +Prepared by **apoursh**, with substantial OpenAI Codex assistance in proof, +implementation, and separate agent proof/code audits. Apache-2.0. + +Cinna Davis (PR2085/2112), Nick Petalas (PR2910/6032), Philippe Van Velzen's +earlier fixed-frame result as retained in PR2910 and +[Discussion2091](https://github.com/CrocSwap/integer-mult-bounds/discussions/2091#discussioncomment-18935374), +and the retained BIT lineage keep their attribution. Determinant, support +and first-order rank methods are inherited. Agent audits are not human or +formal-kernel approval. diff --git a/research/bit-positive-frame-use/SOURCES.json b/research/bit-positive-frame-use/SOURCES.json new file mode 100644 index 0000000000..784c2b1ace --- /dev/null +++ b/research/bit-positive-frame-use/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-fifth-frame-determinant-obstruction/README.md", + "usage": "input", + "git_blob": "608a24af8bc3d27ee1554c94872601bb3a409f67", + "sha256": "fa3f0f951146caa5b1eb7b7417175eb7a380cae8674e4a470407517dac40f227" + }, + { + "path": "research/bit-fifth-rational-frame-every-rational-t/README.md", + "usage": "input", + "git_blob": "a7c6b3a06b8f215b983536934bb37cd6a0324945", + "sha256": "90ba9a56a928c4dc44fa771413e0356ea2ab05979b5cd91f14aa5ed2eeaafe3e" + }, + { + "path": "research/bit-four-register-rational-frame-floor-seed3573e12e/README.md", + "usage": "input", + "git_blob": "32f600d6cb56c94f931a4dc98fb97573ecc134f7", + "sha256": "40cbc4ec8e5c49930d7cb8ecf9e462a08266fe604ea426aa5c7b0d5e547fdffd" + } + ] +} diff --git a/research/bit-positive-frame-use/TASK.json b/research/bit-positive-frame-use/TASK.json new file mode 100644 index 0000000000..9d255c3cb9 --- /dev/null +++ b/research/bit-positive-frame-use/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Classify every nonzero positive symmetric rational rank-one added address usable in any exact word for the PR2085 endpoint, with arbitrary finite restored dirty workspace and free address-independent binary mixing. Prove the exact attainable R-using length spectrum {m+7,2m+6} when R=F/m.", + "scope_change_reason": "Selected the explicit all-length positive-frame follow-up left in PR6079. This changes the catalogue card from native larger/nonabelian construction to a formal alphabet classification. The proof is self-contained from canonical predecessor invariants and has no pending PR6079 theorem or executable dependency.", + "bottleneck_link": "Scoped side result: positive single-frame extensions can only subdivide old directions and cannot provide a cheaper primitive. Two-frame extensions, different endpoints and native paid implementations require separate work.", + "budget_minutes": 60, + "stop_rule": "Stop at one uniform classification and sharp construction with independent exact verification; stop earlier on a proof gap. No unbounded word search or expansion into native supplier construction.", + "outcome": "completed", + "evidence": "PROOF.md establishes usable iff R=F/m and exact R-using length set {m+7,2m+6}. Exact checker derives40 determinant families from 330 old-count profiles, 12 rank survivors and 48 finite support-weight certificates valid for arbitrary r. Corroboration: 3840 parameter support checks, 40 reciprocal/212 nonreciprocal scale fixtures, 20 rotated frames, 128 direct and 128 conjugated replacement words, 577 rejected mutants. Primary algebra checks cover symmetries, lattice characters, count patterns, noncommuting products and the negative-frame boundary. Universal statements rest on the proof.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, independent agent derivations and adversarial code/proof review. No human or formal-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can two positive added rational rank-one frames enable fewer than eight calls for this endpoint?", + "why_it_matters": "The single-frame classification leaves this explicit alphabet extension open.", + "first_step": "Write the joint determinant equation and exact target-support constraints for at most seven calls, then apply rank constraints before searching words.", + "blocked_by": "The residual is no longer a single rank-one matrix. An exact word and fully charged native supplier are required for any multiplication gain." + }, + { + "question": "Is the third necessary profile (0,1,3,3,m) realizable for any m>=2?", + "why_it_matters": "This would resolve count-profile realizability, though it cannot change the already sharp minimum or attainable total-length spectrum.", + "first_step": "The old-lattice character excludes m=1. Study m=2 with exact coefficient equations or find a coefficient obstruction uniform in m.", + "blocked_by": "Only the first two necessary profiles are constructed here; rank and support filters alone do not establish realizability." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19233896", + "scope_key": "7084092dd726e7ba1f2f", + "chooser_seed": "9da5de6c63f0e0f69135ef2d1c7c085d", + "orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY at unchanged canonical base721c03822, after materializing pinned sparse inputs. No scientific selected-frontier replay." +} diff --git a/research/bit-positive-frame-use/VERIFY.json b/research/bit-positive-frame-use/VERIFY.json new file mode 100644 index 0000000000..57a3422be9 --- /dev/null +++ b/research/bit-positive-frame-use/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-fifth-frame-determinant-obstruction/README.md", + "research/bit-fifth-rational-frame-every-rational-t/README.md", + "research/bit-four-register-rational-frame-floor-seed3573e12e/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hashes; all finite determinant/count families; unbounded support-weight certificates; exact symmetries and denominator-safe characters; literal subdivision words, length spectrum and semantic failure controls. No assertions or predecessor executable imports." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source hashes; all finite determinant/count families; unbounded support-weight certificates; exact symmetries and denominator-safe characters; literal subdivision words, length spectrum and semantic failure controls. No assertions or predecessor executable imports." + } + ] +} diff --git a/research/bit-positive-frame-use/independent.py b/research/bit-positive-frame-use/independent.py new file mode 100644 index 0000000000..76a50de8c5 --- /dev/null +++ b/research/bit-positive-frame-use/independent.py @@ -0,0 +1,420 @@ +"""Independent finite corroboration of positive rank-one address usability. + +Exact rational determinant families and literal subset support are checked here; +finite parameter and workspace grids are not a universal proof. The written +proof supplies the reduction for arbitrary positive rational R and all finite +restored dirty workspaces. No predecessor executable is imported. +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +from itertools import product + +F = Fraction +ZERO = (F(0), F(0), F(0)) +A = (F(1), F(0), F(0)) +B = (F(0), F(1), F(0)) +P = (F(1, 2), F(1, 2), F(1, 2)) +Q = (F(1, 2), F(1, 2), F(-1, 2)) +LABELS = (A, B, P, Q) +TOTAL = (F(4), F(4), F(0)) + + +def require(test, message): + if not test: + raise ValueError(message) + + +def plus(left, right): + return tuple(a + b for a, b in zip(left, right)) + + +def times(coefficient, address): + return tuple(coefficient * entry for entry in address) + + +def difference(left, right): + return plus(left, times(-1, right)) + + +def total_address(counts, labels): + result = ZERO + for count, label in zip(counts, labels): + result = plus(result, times(count, label)) + return result + + +TARGETS = (plus(A, P), plus(A, Q), plus(B, P), plus(B, Q)) + + +def determinant(address): + x, y, z = address + return x*y - z*z + + +def multiple_of(address, base): + """Exact rational ratio, or None if the full matrices are not parallel.""" + for entry, denominator in zip(address, base): + if denominator: + ratio = entry / denominator + return ratio if times(ratio, base) == address else None + raise ValueError('zero base in ratio computation') + + +def old_count_domain(): + """Every old multiplicity quadruple of total strictly less than eight.""" + for a in range(8): + for b in range(8 - a): + for p in range(8 - a - b): + for q in range(8 - a - b - p): + yield a, b, p, q + + +def derive_families(): + families = [] + visited = 0 + for counts in old_count_domain(): + visited += 1 + residual = difference(TOTAL, total_address(counts, LABELS)) + if determinant(residual) != 0 or residual[0] + residual[1] <= 0: + continue + n = sum(counts) + d = counts[0] - counts[1] + e = counts[2] - counts[3] + require(d*d + e*e == (8 - n)**2, 'determinant circle identity') + require(abs(d) + abs(e) <= n, 'count difference constraint') + require(4 <= n <= 7 and d*e == 0, 'axial integral circles') + matched = [(j, multiple_of(residual, label)) for j, label in enumerate(LABELS)] + matched = [(j, ratio) for j, ratio in matched if ratio is not None and ratio > 0] + require(len(matched) == 1, 'unique old direction derived from raw entries') + direction, scale = matched[0] + require(scale == 8 - n and scale.denominator == 1, 'positive integer residual scale') + families.append((counts, residual, direction, int(scale))) + require(visited == 330, 'complete old-count domain') + require(len(families) == 40, 'forty all-length determinant families') + require({residual for _, residual, _, _ in families} == + {times(d, label) for d in range(1, 5) for label in LABELS}, + 'sixteen residual matrices') + require([sum(direction == j for _, _, direction, _ in families) for j in range(4)] + == [10, 10, 10, 10], 'ten families per direction') + return families, visited + + +def perpendicular_character(direction, address): + """Integer-valued on each relevant lattice, even with fractional R. + + For A/B, twice the off-diagonal entry annihilates the added line. + For P/Q, the diagonal difference annihilates that line. Each functional + is integral on the old labels, hence on their lattice plus any R there. + """ + x, y, z = address + value = 2*z if direction < 2 else x-y + require(value.denominator == 1, 'character integrality') + return int(value) % 2 + + +def rank_capacity(counts, direction): + demand = sum(perpendicular_character(direction, target) for target in TARGETS) + capacity = sum(n * perpendicular_character(direction, label) + for n, label in zip(counts, LABELS)) + require(demand == 4, 'all four targets detected') + return capacity, demand + + +def subset_representations(target, counts, extra, extra_count): + """Enumerate old subset multiplicities; solve extra multiplicity exactly. + + This compares rational matrix entries directly. It assumes neither a + distinguished coordinate system nor the claimed reciprocal classification. + """ + witnesses = [] + for old in product(*(range(bound + 1) for bound in counts)): + remainder = difference(target, total_address(old, LABELS)) + multiplicity = multiple_of(remainder, extra) + if multiplicity is not None and multiplicity.denominator == 1: + integer = int(multiplicity) + if 0 <= integer <= extra_count: + witnesses.append(old + (integer,)) + return witnesses + + +def parameter_grid(families): + rank_survivors = [(counts, residual, direction, d) + for counts, residual, direction, d in families + if rank_capacity(counts, direction)[0] >= 4] + require(len(rank_survivors) == 12, 'three rank-compatible families per direction') + a_families = {counts: d for counts, _, direction, d in rank_survivors if direction == 0} + require(a_families == {(1, 2, 2, 2): 1, (0, 2, 2, 2): 2, (0, 1, 3, 3): 1}, + 'three canonical residual profiles') + checked = supported = 0 + for counts, residual, direction, d in families: + for r in range(1, 25): + extra = times(F(1, r), residual) + require(perpendicular_character(direction, extra) == 0, + 'rational added frame killed by character') + capacity, demand = rank_capacity(counts, direction) + supports = [subset_representations(target, counts, extra, r) for target in TARGETS] + checked += 4 + accepted = capacity >= demand and all(supports) + expected = capacity >= demand and r % d == 0 + require(accepted == expected, 'support forces a reciprocal old frame') + if accepted: + supported += 1 + m = r // d + require(extra == times(F(1, m), LABELS[direction]), 'reciprocal parameter') + require(sum(counts) + r >= m + 7, 'required-use tariff lower bound') + require(checked == 3840 and supported == 240, 'finite parameter grid coverage') + return rank_survivors, checked, supported + + +def symbolic_support(rank_survivors): + """Finite rational weights certify the unbounded integer parameter step. + + Write rR=dF. A target subset has remainder alpha*F after its old calls; + its extra-call multiplicity is alpha*r/d. Enumerating alpha, rather than + r, is finite because all old count profiles have already been derived. + """ + target_checks = 0 + for counts, _, direction, d in rank_survivors: + weights_by_target = [] + for target in TARGETS: + weights = set() + for old in product(*(range(bound + 1) for bound in counts)): + remainder = difference(target, total_address(old, LABELS)) + alpha = multiple_of(remainder, LABELS[direction]) + if alpha is not None and 0 <= alpha <= d: + weights.add(alpha) + require(weights and weights <= {F(0), F(1)}, 'exact remaining-weight alphabet') + weights_by_target.append(weights) + target_checks += 1 + require(d in (1, 2), 'rank-compatible residual coefficients') + if d == 2: + require({F(1)} in weights_by_target, 'some target forces r/2 integer') + # For d=1 every nonempty subset above gives integral multiplicity. + # For d=2 integrality of r/2 is necessary by the singleton witness, + # and sufficient for every weight set above. This is an exact finite + # certificate of the support reduction, not a bounded r search. + require(target_checks == 48, 'unbounded parameter support certificates') + return target_checks + + +def necessary_profiles(extra, families): + """No bound on r: determinant residual divided by the given R determines it.""" + require(determinant(extra) == 0 and extra[0] + extra[1] > 0, + 'positive nonzero rank-one input') + accepted = [] + for counts, residual, direction, _ in families: + r = multiple_of(residual, extra) + if r is None or r <= 0 or r.denominator != 1: + continue + r = int(r) + require(perpendicular_character(direction, extra) == 0, 'added-line character') + if rank_capacity(counts, direction)[0] < 4: + continue + if all(subset_representations(target, counts, extra, r) for target in TARGETS): + accepted.append(counts + (r,)) + return accepted + + +def rational_fixtures(families): + scales = {F(n, d) for n in range(1, 11) for d in range(1, 11)} + reciprocal = rejected = 0 + for label in LABELS: + for scale in sorted(scales): + profiles = necessary_profiles(times(scale, label), families) + require(bool(profiles) == (scale.numerator == 1), 'rational scale classification') + if scale.numerator == 1: + m = scale.denominator + require(len(profiles) == 3, 'exactly three necessary global profiles') + require(min(map(sum, profiles)) == m + 7, 'finite minimum tariff') + require(set(map(sum, profiles)) == {m + 7, 2*m + 6}, + 'necessary total-length spectrum') + reciprocal += 1 + else: + rejected += 1 + rotated = 0 + for u, v in ((1, 2), (2, 1), (1, -2), (2, -3), (1, 3)): + for scale in (F(1, 7), F(2, 3), F(1), F(5, 2)): + frame = times(scale, (F(u*u), F(v*v), F(u*v))) + require(not necessary_profiles(frame, families), 'rotated frame passed determinant obstruction') + rotated += 1 + return reciprocal, rejected, rotated + + +# Dense matrices over F2 are independent of the address-count computations. +def identity(width): + return tuple(tuple(int(i == j) for j in range(width)) for i in range(width)) + + +def zero_matrix(width): + return tuple((0,) * width for _ in range(width)) + + +def matrix_add(left, right): + return tuple(tuple(a ^ b for a, b in zip(lrow, rrow)) + for lrow, rrow in zip(left, right)) + + +def matrix_multiply(left, right): + width = len(left) + return tuple(tuple(sum(left[i][k] * right[k][j] for k in range(width)) % 2 + for j in range(width)) for i in range(width)) + + +def matrix_rank(matrix): + rows = [list(row) for row in matrix] + rank = 0 + for column in range(len(rows)): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for i in range(rank + 1, len(rows)): + if rows[i][column]: + rows[i] = [a ^ b for a, b in zip(rows[i], rows[rank])] + rank += 1 + return rank + + +def polynomial_product(left, right): + coefficients = {} + for exponent_left, matrix_left in left.items(): + for exponent_right, matrix_right in right.items(): + exponent = plus(exponent_left, exponent_right) + coefficient = matrix_multiply(matrix_left, matrix_right) + coefficients[exponent] = matrix_add( + coefficients.get(exponent, zero_matrix(len(matrix_left))), coefficient) + return {exponent: coefficient for exponent, coefficient in coefficients.items() + if any(any(row) for row in coefficient)} + + +def projector(width, role): + return tuple(tuple(int(i == j == role) for j in range(width)) for i in range(width)) + + +def paid_factor(address, projection): + require(address != ZERO, 'nonzero paid address') + require(matrix_rank(projection) == 1, 'rank-one paid projector') + require(matrix_multiply(projection, projection) == projection, 'idempotent paid projector') + return {ZERO: matrix_add(identity(len(projection)), projection), address: projection} + + +def replay(word, width): + result = {ZERO: identity(width)} + for address, projection in word: + result = polynomial_product(result, paid_factor(address, projection)) + return result + + +def endpoint(width): + result = {} + for role in range(width): + address = TARGETS[role] if role < 4 else ZERO + result[address] = matrix_add(result.get(address, zero_matrix(width)), projector(width, role)) + return result + + +def transvection(width, destination, source): + matrix = [list(row) for row in identity(width)] + matrix[destination][source] ^= 1 + return tuple(map(tuple, matrix)) + + +def replace_word(direction, m, width, replacements): + pairs = ((A, P), (A, Q), (B, P), (B, Q)) + word = [] + replaced = 0 + named_counts = [0] * 5 + extra_indices = [] + for role, pair in enumerate(pairs): + for label in pair: + projection = projector(width, role) + if label == LABELS[direction] and replaced < replacements: + extra_indices.extend(range(len(word), len(word) + m)) + word.extend([(times(F(1, m), label), projection)] * m) + named_counts[4] += m + replaced += 1 + else: + word.append((label, projection)) + named_counts[LABELS.index(label)] += 1 + expected = [2] * 4 + [m * replacements] + expected[direction] -= replacements + require(replaced == replacements and named_counts == expected, + 'labelled counts, including the duplicate-frame case m=1') + require(len(word) == 8 - replacements + m * replacements, 'replacement tariff') + require(len(extra_indices) == m * replacements, 'explicit extra-label uses') + return word, extra_indices + + +def word_fixtures(): + words = conjugated = mutants = 0 + m_grid = (1, 2, 3, 4, 5, 7, 8, 12) + for width in (4, 6): + first = transvection(width, 0, 1) + second = transvection(width, 2, width - 1) + third = transvection(width, width-1, 1) if width > 4 else identity(width) + mixing = matrix_multiply(third, matrix_multiply(first, second)) + unmixing = matrix_multiply(second, matrix_multiply(first, third)) + require(matrix_multiply(mixing, unmixing) == identity(width), 'free inverse') + for direction, m, replacements in product(range(4), m_grid, (1, 2)): + word, extra_indices = replace_word(direction, m, width, replacements) + result = replay(word, width) + require(result == endpoint(width), 'exact attaining word') + words += 1 + transformed = [(address, matrix_multiply(mixing, matrix_multiply(N, unmixing))) + for address, N in word] + require(any(N not in [projector(width, j) for j in range(width)] + for _, N in transformed), 'non-coordinate projectors exercised') + segment = replay(transformed, width) + if width > 4: + require(any(matrix[-1] != (identity(width)[-1] if address == ZERO else (0,)*width) + for address,matrix in segment.items()), 'temporary dirty-role write fixture') + restored = polynomial_product({ZERO: unmixing}, + polynomial_product(segment, {ZERO: mixing})) + require(restored == endpoint(width), 'conjugated endpoint and dirty-role restoration') + conjugated += 1 + index = extra_indices[0] + require(replay(word[:index] + word[index + 1:], width) != endpoint(width), + 'one fewer required call mutant survived') + require(replay(word + [word[index]], width) != endpoint(width), + 'one extra call mutant survived') + wrong = list(word) + wrong[index] = (times(F(1, m + 1), LABELS[direction]), wrong[index][1]) + require(replay(wrong, width) != endpoint(width), 'incorrect fraction mutant survived') + wrong = list(word) + wrong[index] = (times(F(1, m), LABELS[(direction + 1) % 4]), wrong[index][1]) + require(replay(wrong, width) != endpoint(width), 'wrong direction mutant survived') + mutants += 4 + if width > 4: + dirty_corruption = polynomial_product(result, {ZERO: transvection(width, 4, 0)}) + require(dirty_corruption != endpoint(width), 'unrestored dirty role mutant survived') + mutants += 1 + nilpotent = ((0, 1, 0, 0), (0, 0, 0, 0), (0, 0, 0, 0), (0, 0, 0, 0)) + require(matrix_rank(nilpotent) == 1, 'nilpotent rank-one fixture') + try: + paid_factor(A, nilpotent) + except ValueError: + mutants += 1 + else: + raise ValueError('rank-one non-idempotent mutant survived') + return words, conjugated, mutants + + +def run(): + families, visited = derive_families() + rank_survivors, support_checks, supported = parameter_grid(families) + symbolic_checks = symbolic_support(rank_survivors) + reciprocal, nonreciprocal, rotated = rational_fixtures(families) + words, conjugated, mutants = word_fixtures() + result = {'old_profiles': visited, 'determinant_families': len(families), + 'rank_survivors': len(rank_survivors), 'parameter_support_checks': support_checks, + 'symbolic_support_checks': symbolic_checks, + 'parameter_survivors': supported, 'reciprocal_fixtures': reciprocal, + 'nonreciprocal_rejections': nonreciprocal, 'rotated_rejections': rotated, + 'attaining_words': words, 'conjugated_words': conjugated, + 'mutants_rejected': mutants} + print('PASS_POSITIVE_FRAME_INDEPENDENT ' + ' '.join(f'{key}={value}' for key, value in result.items())) + return result + + +if __name__ == '__main__': + run() diff --git a/research/bit-positive-frame-use/verify.py b/research/bit-positive-frame-use/verify.py new file mode 100644 index 0000000000..139e518479 --- /dev/null +++ b/research/bit-positive-frame-use/verify.py @@ -0,0 +1,139 @@ +"""Source binding and algebraic checks for the all-length positive-frame proof. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as F +from hashlib import sha256 +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(value, message): + if not value: + raise ValueError(message) + + +def sources(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + declared = json.loads((PACKAGE / 'VERIFY.json').read_text())['inputs'] + count = 0 + for row in manifest['files']: + if row['usage'] == 'input': + require(row['path'] in declared, 'undeclared source input') + require(sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], + 'source hash changed: ' + row['path']) + count += 1 + require(count == 3, 'three canonical predecessor sources') + return count + + +A = ((F(1), F(0)), (F(0), F(0))) +B = ((F(0), F(0)), (F(0), F(1))) +P = ((F(1,2), F(1,2)), (F(1,2), F(1,2))) +Q = ((F(1,2), F(-1,2)), (F(-1,2), F(1,2))) +OLD = (A, B, P, Q) + + +def add(left, right): + return tuple(tuple(a + b for a,b in zip(lrow,rrow)) for lrow,rrow in zip(left,right)) + + +def scale(value, matrix): + return tuple(tuple(value*x for x in row) for row in matrix) + + +def multiply(left, right): + return tuple(tuple(sum(left[i][k]*right[k][j] for k in range(2)) + for j in range(2)) for i in range(2)) + + +def conjugate(matrix, basis, inverse): + return multiply(basis, multiply(matrix,inverse)) + + +TARGETS = tuple(add(OLD[i],OLD[j]) for i,j in ((0,2),(0,3),(1,2),(1,3))) + + +def algebra_checks(): + circles = 0 + for n in range(8): + radius = 8-n + points = {(d,e) for d in range(-n,n+1) for e in range(-n,n+1) + if abs(d)+abs(e)<=n and d*d+e*e==radius*radius} + require(points == (set() if n<4 else {(radius,0),(-radius,0),(0,radius),(0,-radius)}), + 'all possible positive residual circles') + circles += 1 + J = ((F(0),F(1)),(F(1),F(0))) + H = ((F(1),F(1)),(F(1),F(-1))) + identity = ((F(1),F(0)),(F(0),F(1))) + for basis, inverse, frame_perm, target_perm in ( + (J,J,(1,0,2,3),(2,3,0,1)), + (H,scale(F(1,2),H),(2,3,0,1),(0,2,1,3)), + ): + require(multiply(basis,inverse) == identity == multiply(inverse,basis), 'exact rational inverse') + require(tuple(conjugate(x,basis,inverse) for x in OLD) == tuple(OLD[i] for i in frame_perm), + 'old alphabet symmetry') + require(tuple(conjugate(x,basis,inverse) for x in TARGETS) == tuple(TARGETS[i] for i in target_perm), + 'endpoint symmetry with active-role permutation') + # Verify characters on generators. They vanish on the whole rational + # added line, not merely on the old frame modulo two. + for direction, extra_line in enumerate(OLD): + character = ((lambda x: 2*x[0][1]) if direction<2 + else (lambda x: x[0][0]-x[1][1])) + require(character(extra_line) == 0, 'annihilate rational line exactly') + require(all(character(x).denominator == 1 for x in OLD), 'old-label integrality') + require(all(int(character(x)) % 2 == 1 for x in TARGETS), 'rank-four demand') + for c in (F(1,3),F(2,7),F(17,5)): + require(character(scale(c,extra_line)) == 0, 'fractional added-line control') + old_character = lambda x: x[0][0]+x[1][1]-2*x[0][1] + require(tuple(int(old_character(x)) % 2 for x in OLD) == (1,1,0,0), 'old character') + require(sum(int(old_character(x)) % 2 for x in TARGETS) == 4, 'm=1 rank-four demand') + require(sum(n*b for n,b in zip((0,1,3,3,1),(1,1,0,0,1))) == 2, 'm=1 third-profile rank capacity') + # The tempting old-lattice functional trace-2offdiag is NOT integral + # on Q/3; reducing it mod2 would silently change the proof's lattice. + bad = scale(F(1,3),Q) + require((bad[0][0]+bad[1][1]-2*bad[0][1]) == F(2,3), 'nonintegral-character control') + profiles = {(a,4-s,s,s,4-s-a) for s in range(4) for a in range(4-s) if 2*s>=4} + require(profiles == {(1,2,2,2,1),(0,2,2,2,2),(0,1,3,3,1)}, 'symbolic residual patterns') + # A positive old A count leaves only residual scale1; otherwise A+P + # support forces an integral reciprocal directly, as proved in PROOF.md. + require(all(a == 0 or (a,b,p,q,d)==(1,2,2,2,1) for a,b,p,q,d in profiles), + 'positive-A branch requires r*c=1') + return circles + + +def main(): + source_count = sources() + circles = algebra_checks() + namespace = {'__name__':'independent_positive_frame_certificate'} + path = PACKAGE / 'independent.py' + exec(compile(path.read_bytes(),str(path),'exec'), namespace) + result = namespace['run']() + # A manual noncommuting product fixes matrix order independently of the + # (commuting) subdivision constructions. + N = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(0,0,0,0)) + M = ((1,1,0,0),(0,0,0,0),(0,0,0,0),(0,0,0,0)) + paid, prod = namespace['paid_factor'], namespace['polynomial_product'] + zero, a, b = namespace['ZERO'], namespace['A'], namespace['B'] + ab = namespace['plus'](a,b) + zero_forward = ((0,0,0,0),(0,1,0,0),(0,0,1,0),(0,0,0,1)) + middle = ((0,1,0,0),(0,0,0,0),(0,0,0,0),(0,0,0,0)) + zero_backward = ((0,1,0,0),(0,1,0,0),(0,0,1,0),(0,0,0,1)) + require(prod(paid(a,N),paid(b,M)) == {zero:zero_forward,a:middle,ab:M}, 'ordered product oracle') + require(prod(paid(b,M),paid(a,N)) == {zero:zero_backward,b:middle,ab:N}, 'reverse product oracle') + # Positivity is essential: append an A,-A cancellation pair to a valid word. + word, _ = namespace['replace_word'](0,1,4,1) + # The independent construction returns (address, projector) records. + negative_loop = [(a,N),(namespace['times'](-1,a),N)] + require(namespace['replay'](word+negative_loop,4) == namespace['endpoint'](4), 'negative boundary witness') + require(result['rank_survivors'] == 12, 'independent family count') + print('PASS_POSITIVE_FRAME_USE_CLASSIFICATION ' + f'live_sources={source_count} integer_circle_domains={circles} ' + 'alphabet_symmetries=2 lattice_characters=4 noncommuting_oracles=2 negative_boundary=1 m1_third_profile_excluded=1') + + +if __name__ == '__main__': + main()