Prove a sharp Fano cut gap for a GL3 Singer target (no new κ)

research/gl3-singer-cut-gap/PROOF.md

@@ -0,0 +1,120 @@
+# A sharp point-and-line cut obstruction
+
+This scoped proof uses a finite exact certificate on two seven-element sets.
+It does not establish the optimum of a multi-target formal word.
+
+## Model
+
+Let `G=GL_3(F_2)`, with `s_ij=I+E_ij`, `i!=j`, at unit price. Matrices act
+on column vectors. The ordered generator list is
+`(s_01,s_02,s_10,s_12,s_20,s_21)`. Let
+
+```text
+        [1 1 1]
+g   =   [1 0 1]       binary columns (7,1,3).
+        [1 0 0]
+```
+
+In `M_R(F_2[G])`, a paid call is `I+([s_ij]+[e])uv^T`, with binary
+`v^T u=1`. Any invertible scalar register mixing is free. There are `t>=1`
+active roles with targets `[g]` or `[g^-1]`; every other role is an arbitrary
+dirty spectator with exact identity output. All off-diagonal outputs vanish.
+
+Use the point set `P=F_2^3\{0}` with action `x -> A x`, or the line set
+`L`, labelled by nonzero normal covectors, with action `a -> A^-T a`.
+The latter convention makes incidence invariant. Modules may be arbitrary
+finite direct sums of these permutation modules. A coordinate cut chooses
+any subset of the basis in each summand, identically for every scalar role.
+
+For an address permutation `A` and cut `H`, write
+
+`c_H(A)=#{x in H : A x not in H}`.
+
+This is the rank over `F_2` of the crossing block of the permutation matrix.
+The number is unchanged on replacing `A` by `A^-1` or `H` by its complement.
+
+## The finite certificate
+
+On **each** of P and L, every one of the 128 subsets satisfies
+
+`2 c_H(g) <= sum_(i!=j) c_H(s_ij)`.                         (1)
+
+Here is the complete slack histogram for either module. The slack is the
+right-hand side minus the left-hand side, without dividing by two.
+
+| Slack | 0 | 2 | 4 | 6 | 8 |
+|---|---:|---:|---:|---:|---:|
+| Number of subsets | 34 | 46 | 34 | 10 | 4 |
+
+`verify.py` enumerates all subsets and checks (1) with integer arithmetic.
+It constructs both actions from all 168 invertible binary matrices, checks
+all their composition pairs, and checks line incidence independently of
+the inverse-transpose formula. This finite enumeration is the proof of
+(1), not a sampled experiment or a numerical optimization claim.
+
+Matching cuts make the upper bound sharp. Label points and covectors by
+their binary integers 1 through 7, with coordinate zero the low bit. Take
+`H_P={2,4,6}` and `H_L={2,4}`. Their exact profiles are
+
+| Cut | s_01 | s_02 | s_10 | s_12 | s_20 | s_21 | g |
+|---|---:|---:|---:|---:|---:|---:|---:|
+| H_P on P | 2 | 2 | 0 | 0 | 0 | 0 | 2 |
+| H_L on L | 0 | 0 | 1 | 1 | 1 | 1 | 2 |
+
+Weight the first cut by 1/2 and the second by 1. Every paid generator
+then has weight exactly 1, and g has weight exactly 3. Equivalently, use
+one point copy and two line copies with a single coordinate cut, then
+divide all ranks by two.
+
+## Passage to every finite module sum and role count
+
+For a fixed coordinate cut, crossing rank is subadditive under composition.
+Indeed `(AB)_(out,in)=A_(out,in)B_(in,in)+A_(out,out)B_(out,in)`, so its
+rank is at most the sum of the two crossing ranks. Free scalar register
+mixing has zero crossing block. A paid factor has crossing block
+`uv^T tensor (s_ij)_(out,in)`, up to the order of tensor factors. Its rank
+is exactly `c_H(s_ij)`, since `uv^T` has rank one. At the required diagonal
+endpoint the crossing rank is `t c_H(g)`. Every restored spectator adds zero.
+This proves the inherited cut inequality for any finite dirty workspace.
+
+Coordinate cuts on a direct sum split across the summands. Their crossing
+ranks add, so (1) continues to hold for every allowed module sum. If a
+nonnegative combination of these cut inequalities has paid-generator
+coefficients `b_ij<=1`, its endpoint coefficient is at most
+
+`(t/2) sum_(i!=j) b_ij <= 3t`.                             (2)
+
+The two matching cuts attain `3t`. Thus the complete normalized cone of
+the declared coordinate-cut inequalities has **exact value 3t**, for
+every t and every choice of target orientations. Taking more copies,
+more coordinate cuts, or more dirty roles cannot improve this value.
+No linear-program solver is needed to verify the upper or lower certificate.
+
+## Comparison with the direct bill
+
+In chronological execution order, the four labels
+`s_01,s_02,s_10,s_21` have product `s_21 s_10 s_02 s_01=g`. Direct execution
+on each active coordinate therefore costs `4t`, restoring all spectators.
+The full group-algebra verifier checks this endpoint for t=1,2,3, including
+all omitted-call controls and dirty-coupling detours. The Cayley traversal
+also finds that g has distance four. The inverse has the reversed word.
+
+For a single target, every formal coefficient in a k-paid-call word is
+supported on products of at most k paid address labels, even with free
+scalar mixing and dirty roles. The coefficient `[g]` therefore requires
+at least four calls. This standard support argument, already used in
+JoyboyBrian's PR #4974, is not a new contribution here. The new certificate
+shows that the specified point-and-line cut cone stops at three even in
+this singleton case. For multiple targets, **4t is a direct upper bound**;
+this package does not claim an all-workspace lower bound of 4t.
+
+## Limits
+
+Arbitrary subspace cuts, modules other than finite sums of P and L,
+role-dependent cuts, nonlinear or integer-combined invariants and different
+paid alphabets are outside (2). In particular the full regular module is
+not a sum of these two modules as a permutation module. The theorem neither
+constructs shared paid work nor excludes it. Native implementation,
+compiler/hosting/precision invoices, recursive suppliers and the complete
+multiplication theorem remain unproved here. No proof-kernel or independent
+human review is claimed.

research/gl3-singer-cut-gap/README.md

@@ -0,0 +1,119 @@
+# Fano point and line cuts stop at three for a four-call Singer target
+
+For the binary GL3 target with columns `(7,1,3)`, every nonnegative
+combination of coordinate-cut rank inequalities from finite sums of the
+Fano point and dual-line permutation modules has normalized value at most
+**three per target**. Two explicit cuts attain three. The independent
+coordinate word costs four per target.
+
+The sharp cone value is `3t` for any number `t>=1` of targets, each either
+g or its inverse, with any finite restored dirty workspace and free
+invertible binary scalar mixing. This is a **scoped proof with a finite
+256-cut certificate**. It rules out this particular invariant route for
+closing the direct-word gap. It does not prove shared paid work or the
+actual multi-target optimum. No new kappa or selected-frontier change.
+
+[PROOF.md](PROOF.md) defines the model, proves the passage from the finite
+certificate to all finite module sums and role counts, and gives the
+matching rational primal and dual certificates. Every one of the 128
+point cuts and 128 line cuts is checked exactly. The decisive inequality is
+`2*c_H(g) <= sum_(i!=j) c_H(I+E_ij)`. The attaining point cut is `{2,4,6}`
+with weight `1/2`; the line cut is `{2,4}` with weight `1`.
+
+## Reproduce
+
+From the repository root, Python 3.12 and the standard library only:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gl3-singer-cut-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gl3-singer-cut-gap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gl3-singer-cut-gap --check-source-history
+```
+
+A reviewer can replace that interpreter path with any CPython 3.12 binary.
+`VERIFY.json` registers warning-strict normal and optimized checks. Each
+prints `PASS_GL3_SINGER_CUT_GAP` inside a generated JSON receipt that binds
+all package files and both declared predecessor README inputs by SHA256.
+No receipt is hand-written or accepted in place of recomputation. The
+verifier writes no files and needs neither Git nor network in a source
+export with its declared inputs.
+
+Coverage includes all 168 group elements, 56,448 action-composition checks,
+1,176 point-line incidence checks, all 256 cuts, and 2,520 actual paid
+crossing blocks from all 35 rank-one idempotents through three roles on
+six declared cuts. Formal group-algebra controls check the direct endpoint
+with one to three targets and a dirty spectator, 24 omitted calls, three
+restored dirty detours and three corresponding leaks. Four malformed-input
+controls remain active under optimization. These controls support the
+specified finite certificate; they are not larger-register word searches.
+
+Both direct commands and the complete registered replay passed locally on
+CPython 3.12.15, macOS arm64. Each registered command completed in under one
+second. Hosted CI certification is separate from these local checks.
+
+## Verifier bounds
+
+The checker has no recursion, dynamic evaluation or subprocesses. All 21
+functions are at most 29 lines. Group enumeration considers 343 column
+triples; Cayley traversal has seven rounds and at most 168 states; each
+action table has 168 rows. Formal coefficients have at most 168 group
+keys and four scalar roles in the controls; each word has at most 14
+factors. Rank elimination has at most 21 columns. Every rejection uses an
+explicit exception, so optimization cannot disable it.
+
+Python necessarily allocates managed objects during these computations.
+This is a deviation from fixed allocation after initialization, confined
+to the stated finite domains. Fixed matrix sizes, group support and loop
+bounds constrain live mathematical data; Python allocator overhead is not
+statically certified. Expanding these domains requires a fresh resource
+bound. Warning-strict normal and optimized execution, source compilation
+and the repository package checks are the available diagnostics; no
+separate Python linter is installed in the environment used here.
+
+## Scope and next decision
+
+The original `bit-new-register-model` card is changed to the quotient-based
+invariant question in Josie Elliston's PR #1974, Open next question 2.
+That predecessor already proves the complete two-role tariff by a word
+census. Its census is cited, not replayed. This package adds the exact
+point-and-line coordinate-cut cone obstruction for the specified order-seven
+endpoint. A natural-representation alias alone does not prove this closure.
+
+Stop this certificate family for this target. Arbitrary subspaces,
+other permutation modules, role-dependent cuts and nonlinear or integer
+combinations are outside the proof. Native address realization, compiler,
+hosting, precision, tape accounting, recursive profiles and the complete
+multiplication theorem are unproved here. No human or proof-kernel review
+is claimed; no predecessor engine, selected supplier, Lean or Docker replay
+is run.
+
+## Open next questions
+
+- Can a coordinate cut in a different GL3 permutation module certify more
+  than three for this exact target? Start with one explicit finite G-set
+  and report its six generator crossings and target crossing. It must lie
+  outside the point/line direct-sum class. A stronger valid cut is missing.
+- Can a noncoordinate subspace cut in a point/line module sum exceed three?
+  Start with one explicit binary subspace and compute all seven quotient
+  ranks. The present proof uses coordinate subsets and does not settle it.
+
+## Sources and credit
+
+The proof and verifier were produced by Nick Petalas. Apache-2.0.
+Credit Josie Elliston's
+[PR #1974](https://github.com/CrocSwap/integer-mult-bounds/pull/1974) and
+Hanson Sun's seed18 package for the formal mixed-target model and written
+invariant question; Adam Gall and Ross Richardson for the cut-rank method;
+JoyboyBrian's [PR #4974](https://github.com/CrocSwap/integer-mult-bounds/pull/4974)
+for the existing single-target support argument; and the retained eumemic,
+Ali Romman and Gareth Davidson register-model lineage. The cut inequality
+and single-target distance principle are inherited. The matching finite
+cone certificates for this Singer endpoint are the new contribution.
+
+[SOURCES.json](SOURCES.json) pins the source bytes at canonical main
+`de5ec2e7a6074068452f45b1a191b5c72832df4a`. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217837)
+records the exact scope. Main-tree, merged-PR, open-PR and live claim
+searches found no matching Singer point/line certificate. This is search
+coverage, not a guarantee about unpublished work. The existing three-cycle
+cut-ceiling work has a different endpoint and is not extended here.

research/gl3-singer-cut-gap/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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-gl3-mixed-targets-length10/README.md",
+      "usage": "input",
+      "git_blob": "59ac7008af69ffb41e10e6574308d68c33d44c48",
+      "sha256": "f1f88a618fa998baa2bb5e8bc69c225405b6106b4c0a5646d84c42166cd4aff5"
+    },
+    {
+      "path": "research/bit-gl3-mixed-targets-seed18/README.md",
+      "usage": "input",
+      "git_blob": "3e5f714a9ae2113afdf00352f29c73073843d2a8",
+      "sha256": "885674f74ba2f40256f0d3388a8e856aae7b27063aea84b2687eda08787e101f"
+    }
+  ]
+}

research/gl3-singer-cut-gap/TASK.json

@@ -0,0 +1,82 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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": "Prove exact normalized point/line coordinate-cut cone value 3t for t copies of the GL3 Singer target with columns (7,1,3) or its inverse, versus direct bill 4t.",
+  "scope_change_reason": "Take PR1974 Open next question 2 and rule out one explicit quotient-based invariant family. This is a proof-method side result, not a new register construction or a predecessor census replay.",
+  "bottleneck_link": "An exact obstruction prevents pursuing this cut family to prove the direct tariff; other modules or noncoordinate invariants are needed.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first matching exact primal/dual certificate. Do not expand to other modules or targets.",
+  "outcome": "completed",
+  "evidence": "All 256 point/line cuts satisfy the exact dual inequality; two explicit cuts attain value three. A written direct-sum and cut-rank argument gives every finite module sum and dirty-role count.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can another GL3 permutation module certify more than three for this Singer target?",
+      "why_it_matters": "This would leave the exact closed certificate family.",
+      "first_step": "Give one explicit finite G-set and its six generator cuts and target cut.",
+      "blocked_by": "No stronger valid cut is supplied."
+    },
+    {
+      "question": "Can a noncoordinate subspace cut in a point/line module sum exceed three?",
+      "why_it_matters": "Such a cut changes the coordinate-subset hypothesis.",
+      "first_step": "Provide one explicit binary subspace and compute all seven quotient ranks.",
+      "blocked_by": "No such subspace or upper certificate is known here."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217837",
+  "question_source": {
+    "pr": 1974,
+    "author": "JosieElliston",
+    "question": "Open next question 2, written invariant for additive tariffs"
+  },
+  "environment": {
+    "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "Python standard library only",
+    "receipt": "Generated on stdout from a fresh complete computation; no stored receipt accepted."
+  }
+}

research/gl3-singer-cut-gap/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/bit-gl3-mixed-targets-length10/README.md",
+    "research/bit-gl3-mixed-targets-seed18/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Complete exact point/line cut certificate, action/endpoint and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same complete certificate and controls with assertions disabled."
+    }
+  ]
+}