Prove a fifth rational frame needs eight calls for every rational slope, settling the #2112 seven-call case (no new κ)

research/bit-fifth-rational-frame-every-rational-t/README.md

@@ -0,0 +1,157 @@
+# A fifth rational frame never saves a call: the minimum is eight for every rational t
+
+**Scoped proof in a formal register model, with a finite exact check. No
+selected supplier or new κ is claimed.**
+
+## Result
+
+Take the four-role target of
+[PR #2085](https://github.com/CrocSwap/integer-mult-bounds/pull/2085),
+
+$$
+T=\operatorname{diag}([A+P],[A+Q],[B+P],[B+Q]),
+$$
+
+with $A=E_{11}$, $B=E_{22}$, $P=\tfrac12\begin{pmatrix}1&1\\1&1\end{pmatrix}$
+and $Q=A+B-P$. A paid call is $I_4+([F]-1)N$ with $N$ any of the 120 rank-one
+idempotents in $M_4(\mathbb F_2)$, and free role mixing is allowed. Add the
+fifth rational rank-one address
+
+$$
+R_t=(1,t)^T(1,t)=\begin{pmatrix}1&t\\t&t^2\end{pmatrix},\qquad t\in\mathbb Q .
+$$
+
+**Theorem.** For every rational $t$, every word over $\{A,B,P,Q,R_t\}$ that
+equals $T$ in $M_4(\mathbb F_2[\Lambda_t])$, $\Lambda_t=\mathbb ZA+\mathbb ZB+\mathbb ZP+\mathbb ZR_t$,
+has at least eight calls. The direct eight-call word attains this, so the
+exact minimum is eight.
+
+For $t=1/2$ this settles the seven-call case that
+[PR #2112](https://github.com/CrocSwap/integer-mult-bounds/pull/2112) left
+open: its bound $7\le\min\le8$ becomes $\min=8$. It also answers the family
+question in #2085's open-next-questions for the whole slope family $R_t$.
+
+## Proof
+
+Coordinates. Write a symmetric matrix $\begin{pmatrix}a&c\\c&b\end{pmatrix}$ as
+$(a-c)A+(b-c)B+2cP$. Then $R_t=(1-t)A+(t^2-t)B+2tP$, and the four target
+frames are $A+P$, $2A+B-P$, $B+P$ and $A+2B-P$.
+
+**Step 1 (exponent support).** Over $\mathbb F_2$,
+$I+([F]-1)N=(I+N)+[F]N$. Expanding a product of $k$ such factors gives a sum
+over subsets $S$ of calls of $[\sum_{j\in S}F_j]$ times a binary matrix. The
+group elements $[x]$ are a basis of $\mathbb F_2[\Lambda_t]$, so the diagonal
+entry $[C_i]$ of $T$ forces $C_i=\sum_F n_FF$ with $0\le n_F\le k_F$, where
+$k_F$ is the number of calls with label $F$. This is an equality of rational
+matrices, not a congruence.
+
+With $n_R=0$ each target has exactly one such representation:
+$A+P$, $A+Q$, $B+P$, $B+Q$. With $n_R\ge1$, the $P$-coordinate equation
+$n_P-n_Q+2n_Rt=c_P$ fixes $t$. Enumerating every $n$ with $\sum n_F\le7$ shows
+that the only rational $t$ admitting such a representation is $t=0$, where
+$R_0=A$. Hence, for $t\ne0$, a word with at most seven calls uses each of
+$A,B,P,Q$ at least once.
+
+**Step 2 (first order).** Let $L$ be a lattice containing all labels and
+targets. Modulo the square of the augmentation ideal, a word equal to $T$
+satisfies $\sum_F S_F\otimes\bar F=\sum_iE_{ii}\otimes\bar C_i$ in
+$M_4(\mathbb F_2)\otimes L/2L$, where $S_F$ is the sum of the idempotents on
+calls labelled $F$. A sum of $k$ rank-one idempotents has rank at most $k$ and
+trace $k\bmod2$; write $f(S)$ for the resulting floor. This is the method of
+#2085 and #2112.
+
+**Step 3 (lattice by denominator parity).** Let $t=p/q$ in lowest terms. The
+coordinate $t^2-t=p(p-q)/q^2$ has exact denominator $q^2$, so
+$\Lambda_t/\Lambda$ is cyclic of order $q^2$, with $\Lambda=\mathbb ZA+\mathbb ZB+\mathbb ZP$.
+
+- *$q$ odd.* The index is odd, so $\Lambda/2\Lambda\to\Lambda_t/2\Lambda_t$ is
+  an isomorphism. Two-adically $1-t\equiv1+p$, $t^2-t\equiv0$ and $2t\equiv0$,
+  so $R_t\equiv A$ ($p$ even) or $R_t\equiv0$ ($p$ odd). In the first case the
+  calls labelled $A$ or $R_t$ together sum to the old $S_A$; in the second,
+  $R_t$ calls add cost without first-order effect. Either way the floor is the
+  #2085 floor $\min_S f(S)+f(S+P_A)+f(S+P_B)+f(S+I)=8$, with
+  $P_A=\operatorname{diag}(1,0,0,1)$ and $P_B=\operatorname{diag}(0,1,1,0)$.
+  This case needs no support argument and holds for every word length.
+- *$q$ even.* The two-part of $\Lambda_t/\Lambda$ is cyclic and nontrivial, so
+  $\Lambda/2\Lambda\to\Lambda_t/2\Lambda_t$ has a one-dimensional kernel. The
+  kernel is spanned by $q^2R_t\bmod 2\Lambda$, whose $B$-coordinate $p(p-q)$ is
+  odd and whose other coordinates are even: $B\in2\Lambda_t$. So $A,P,R_t$
+  give a basis of $\Lambda_t/2\Lambda_t$, $Q\equiv A+P$, and the targets reduce
+  to $A+P$, $P$, $P$, $A+P$. A word that uses no $R_t$ lies in
+  $\mathbb F_2[\Lambda]$ and has the #2085 floor of eight. A word that uses
+  $R_t$ has $S_{R}=0$, so an even number $k_R\ge2$ of $R_t$ calls. By Step 1
+  it also has $k_B\ge1$ and $k_A,k_P,k_Q\ge1$. With $g(S)=f(S)$ when $f(S)>0$
+  and $g(0)=2$,
+  $$k_A+k_P+k_Q\ge\min_Sg(S)+g(S+P_A)+g(S+I)=5,$$
+  so $k\ge5+2+1=8$.
+
+The case $t=0$ has odd denominator. This proves the theorem.
+
+The verifier recomputes every finite input:
+
+- both first-order minima over all 65,536 masks;
+- the support enumeration over all rational $t$;
+- the 120 idempotents, each of rank one and trace one;
+- the parity classification of $\Lambda_t/2\Lambda_t$ on all 1,431 reduced
+  $t=p/q$ with $q\le24$ and $|p|\le48$. This is a check on the general
+  argument above, not its proof.
+
+It also multiplies the direct eight-call word exactly in the group algebra.
+Two controls must fail: dropping one call, and dropping the $P$-bits of roles
+2 and 3 from the even-case mask, which lowers that floor from five to three.
+
+## What is new and what is reused
+
+The model, target, rank/trace floor and the $t=1/2$ lattice come from Cinna
+Davis's #2085 and #2112. #2112 excludes six calls at $t=1/2$ by enumerating
+388,800 words; this package does not repeat or check that enumeration. The
+new parts are the exponent-support step, which forces a $B$ call that the
+first-order relaxation cannot see, the resulting seven-call exclusion, and the
+reduction of every rational slope to the two denominator-parity cases.
+Expanding a product of such factors over subsets of calls is elementary and
+is not claimed as a new technique.
+
+## Scope
+
+This is a scoped proof in the formal paid-call model above: all word lengths
+for odd-denominator $t$, and all words of at most seven calls for even
+denominators (enough for the exact minimum). It does not cover other rank-one
+addresses such as scalar multiples $cR_t$, two or more added frames, other
+targets, frame construction, addition, precision, or interface charges. It
+gives no supplier mapping and no κ change. Python 3.12 is the registered
+runtime. The general lattice argument is a hand proof checked on a finite grid,
+not a proof-assistant verification.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+python3.12 -I -B research/bit-fifth-rational-frame-every-rational-t/verify.py
+python3.12 -B scripts/research_package.py --package research/bit-fifth-rational-frame-every-rational-t
+```
+
+Expected line (under a second):
+
+```text
+PASS_FIFTH_RATIONAL_FRAME_EVERY_T_EXACT_MINIMUM_8 grid_odd=949 grid_even=482 support_exceptions=['0'] idempotents=120 odd_floor=8 even_visible_floor=5 even_total=8 mutated_visible_floor=3 direct_calls=8
+```
+
+## Open next questions
+
+- **Scaled and two-frame alphabets.** Does any rational rank-one address
+  $c\,v^Tv$ in the symmetric span, or any pair of added frames, lower eight?
+  The support step still applies. The first step is to classify which
+  addresses can enter a target's exponent support with at most seven calls.
+  Only those can matter beyond the first-order floor.
+- **Support-plus-first-order as a general screen.** The support step is
+  valid for any torsion-free address alphabet. Combining it with the
+  first-order floor may decide other open minimum-length cases in this model
+  family without enumerating words. The blocker is targets whose supports are
+  not unique.
+
+## Credit
+
+Produced by Nick Petalas. The model, target, rank/trace floor and the
+$t=1/2$ instance are Cinna Davis's (1337isnot1337) #2085 and #2112, cited
+above and pinned in [SOURCES.json](SOURCES.json). New work is Apache-2.0.

research/bit-fifth-rational-frame-every-rational-t/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-four-register-rational-frame-floor-seed3573e12e/README.md",
+      "usage": "provenance",
+      "git_blob": "32f600d6cb56c94f931a4dc98fb97573ecc134f7",
+      "sha256": "40cbc4ec8e5c49930d7cb8ecf9e462a08266fe604ea426aa5c7b0d5e547fdffd"
+    },
+    {
+      "path": "research/bit-fifth-rational-frame-six-call-seed0d9888a6/README.md",
+      "usage": "provenance",
+      "git_blob": "9784de6be0f4a63995b63bcfa3bf8dacafe65e6b",
+      "sha256": "df38ee78d19b203a8847cba1342feeeb1d8cbab87fdf7850d3329404bb93183c"
+    }
+  ]
+}

research/bit-fifth-rational-frame-every-rational-t/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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": "For the four-role target diag([A+P],[A+Q],[B+P],[B+Q]) of PR #2085 and the five-address alphabet {A,B,P,Q,R_t}, R_t=(1,t)^T(1,t), with paid factors I+([F]-1)N over all rank-one idempotents N in M4(F2), determine the exact paid-call minimum for every rational t. This settles the seven-call case left open by PR #2112 at t=1/2.",
+  "scope_change_reason": "The card permits a specified legal operation alphabet. This keeps the four roles, target and model of PRs #2085/#2112 and answers their stated open questions (the R_t slope family and the seven-call case) instead of searching a new alphabet.",
+  "bottleneck_link": "Side result for the bit primitive in a favorable formal paid-call model: it removes one candidate saving route (a fifth symmetric rank-one frame) for this target. The selected result's complex primitive still binds; no supplier or kappa change follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the exact minimum is decided for every rational t; do not extend to scaled frames or two added frames in this session.",
+  "outcome": "completed",
+  "evidence": "Exponent support: each target frame must equal a nonnegative subset sum of the word's labels; with at most seven calls R_t can enter such a sum only at t=0, so for t!=0 each of A,B,P,Q is used. First order: for odd-denominator t, L/2L is the old lattice mod 2 and R_t is A or 0, giving the PR #2085 floor 8 at every length. For even-denominator t, B lies in 2L, A,P,R_t give a basis mod 2, and a word using R_t needs an even number (>=2) of R_t calls, at least one B call and at least 5 A/P/Q calls (exact minimum over 65,536 masks), so at least 8. The direct eight-call word attains 8.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a scaled rational rank-one address c v^T v, or a pair of added frames, lower the eight-call minimum for this target?",
+      "why_it_matters": "This package closes only the one-parameter slope family R_t; the support step suggests that only addresses entering a target's exponent support can matter.",
+      "first_step": "Classify the addresses that can appear in a nonnegative support of a target frame using at most seven calls, then apply the first-order floor to those alone.",
+      "blocked_by": "Two added frames can make target supports non-unique, so the forced-label count used here no longer follows."
+    },
+    {
+      "question": "Does exponent support plus the first-order floor decide other open minimum-length cases in torsion-free address models?",
+      "why_it_matters": "It replaces word enumeration by a small exact computation when target supports are unique.",
+      "first_step": "Apply the two screens to a recorded open minimum-length case with a torsion-free address group.",
+      "blocked_by": "Targets with several supports and finite (torsion) address groups, where the support step is weaker."
+    }
+  ]
+}

research/bit-fifth-rational-frame-every-rational-t/VERIFY.json

@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Frame identities; parity classification of L/2L on 1,431 reduced slopes; exact exponent-support enumeration over all rational t (exceptions {0}); 120 idempotents; rank/trace first-order minima over all 65,536 masks (odd 8, even visible 5); direct eight-call word in the exact group algebra; dropped-call and mutated-mask controls."
+    }
+  ]
+}