Prove one-field sector workspace floor with rational overwrites (no κ)

research/sector-scalar-workspace/ENGINEERING.md

@@ -0,0 +1,25 @@
+# Verifier boundaries
+
+The autonomous local run playbook stopped at the first proved improvement:
+the workspace theorem for an enlarged ordinary alphabet. Build the Lever
+produced the standalone exact checker. Prove It Works required its normal,
+optimized, registered and portable export execution. Unslop shaped the claim
+and the separation of new lower bound from cited upper bound.
+
+Power of Ten inspection applies only to the new verifier. There is no recursion,
+subprocess, network call, mutation of inputs or generated runtime file. Matrix
+dimensions are bounded by 64; the independent permutation oracle is bounded
+by four. Projector axes are bounded by six, blocks by sixteen, ordinary-matrix
+enumeration by 8^4, and word checks by 5*80*24 cuts. Every function is below
+60 physical lines. Explicit contracts stay active under optimization.
+
+Python's fractions, lists and interpreter allocate dynamically. This is a
+managed-runtime deviation from fixed steady-state allocation, bounded here by
+the stated finite dimensions and loop counts. File reads and SHA256 hashing
+also allocate; at most sixteen top-level package files are accepted. Standard
+library allocation internals are not instrumented. There are no callbacks
+from external input, reflection or dynamic evaluation in the checker. Its
+four direct internal check functions are the finite dispatch list in main.
+Read-only package bytes and Python's standard library are the runtime trust
+boundary. Warning-strict normal and optimized execution supplies the available
+interpreted-code diagnostics; no separate static type checker is configured.

research/sector-scalar-workspace/PROOF.md

@@ -0,0 +1,126 @@
+# One owned field remains necessary under rational overwrites
+
+## Contract
+
+This is a scoped algebraic proof. Work over the commutative rational group
+algebra
+
+`B = Q[q,j_1,...,j_(s-1)] / (q^4-1, j_1^2-1,...,j_(s-1)^2-1)`,
+
+where `s>=1`. Put `J_0=q^2` and `J_k=j_k` for `k>=1`. The ordinary subalgebra
+`A` is generated by the `J_k`. Its elements do not distinguish `q=1` from
+`q=-1` when the spectator involutions have the same values. These are the
+formal faithful-sector interfaces of the cited Boolean-sector family.
+
+For every `a in F2^s`, let
+
+`E_a = 2^(-s) product_k (1 + (-1)^(a_k) J_k)`.
+
+There are `r>=1` blocks, each containing `2^s` independent data fields. The
+desired data map multiplies field `a` in every block by
+
+`F_a = 1 + q E_a/2`.
+
+Any finite number of borrowed fields is allowed, with independent arbitrary
+initial values and exact restoration. Every data field must produce its own
+specified output independently of those borrowed values. An owned field has
+arbitrary initial data and must finish zero. The question is whether a program
+can have zero owned fields.
+
+Grant the following enlarged instruction alphabet:
+
+- Any square matrix with entries in `A` on all current fields, for free.
+  This includes arbitrary rational scalar overwrites, dense ordinary mixing, shifts and
+  CLEAR. The maps need not be assumed invertible in advance.
+- Multiplication of one field by `q` or `q^-1`, with any finite number of calls.
+
+All instructions are `B`-linear. The program is a fixed finite word on these
+fields. It has no data-dependent branches, nonlinear operations, discarded outputs or other
+`q`-dependent ordinary gates. Dynamically borrowed fields can be included from
+the start as unused fields, because their values are arbitrary and restored.
+
+## The new lower bound
+
+**Theorem.** No word in this enlarged alphabet realizes the target with zero
+owned fields. Consequently the exact minimum owned-field count is one,
+using the cited one-field construction for the upper bound.
+
+**Proof.** Fix the spectators to `j_k=1` and evaluate at `q=1` and `q=-1`.
+Write these rational algebra homomorphisms as `chi_+` and `chi_-`. Both send
+every `J_k` to `1`, so they agree on every ordinary coefficient in `A`.
+
+Suppose there are `N=r 2^s+b` fields, including `b` borrowed fields and no
+owned fields. Every instruction therefore gives two square rational matrices.
+For an ordinary instruction these matrices are identical, so their
+determinants agree. A query has determinant `1` at `chi_+` and `-1` at
+`chi_-`. Its inverse has the same two determinants. Multiplicativity gives
+the invariant
+
+`det M_+ = (-1)^t det M_-`,
+
+where `t` is the total number of query and inverse-query instructions.
+This equality holds even if an ordinary gate is singular.
+
+Exactly `E_0` evaluates to `1`; all other `E_a` evaluate to `0`. Each target
+block thus has determinant `3/2` at `chi_+` and `1/2` at `chi_-`. Restoration
+of borrowed fields contributes an identity block, while independence of the
+data outputs removes off-diagonal borrowed-to-data terms. The target is
+exactly `diag(F_data,I_b)`. It follows that
+
+`det M_+ / det M_- = 3^r`.
+
+Both determinants are nonzero. Since `r>=1`, this ratio is neither `1` nor
+`-1`, contradicting the invariant. This proves the lower bound for every
+finite number of restored borrowed fields and every finite word length.
+
+For the upper bound, PR #5658 constructs an ordinary involutive route that
+collects `sum_a E_a x_a` at role zero. In each block it clears one owned field,
+copies that role to it, queries it, adds half its value to the role, and clears
+it again. Applying the ordinary route again gives precisely the required
+`F_a` outputs. One owned field is reused across all blocks. That published
+construction is a cited upper bound, not a result audited in this package.
+Its dyadic alphabet is contained in the enlarged alphabet. Hence the lower
+and upper bounds match. QED.
+
+## What changed from the predecessor
+
+Ali Romman's PR #5658, section 5, proves the workspace lower bound when scalar
+overwrites are restricted to dyadic units. Its rank-loss argument reduces
+modulo three. Allowing `SCALE 3/2` defeats that invertibility premise, as the
+source explicitly notes. Our argument works in characteristic zero and
+compares two characters that every ordinary instruction shares. It covers
+all rational scalar overwrites and, more strongly, arbitrary ordinary linear
+mixing. It does not extend the predecessor's sharp `r+1` CLEAR bound to this
+larger alphabet.
+
+The invariant is a classical determinant argument. The new contribution is
+its application to the explicitly open scalar-overwrite interface and the
+resulting sharp workspace theorem, produced by Nick Petalas.
+
+## Scope controls and limitations
+
+A primitive overwrite by `1+q/2` distinguishes the two characters and directly
+evades the hypothesis. It is outside the ordinary algebra. If borrowed outputs
+may change, a reciprocal factor on a borrowed field can cancel the determinant
+ratio, so the displayed obstruction also disappears. Neither control supplies
+a legal implementation in the stated model. No characteristic-two or
+nonlinear/adaptive claim follows from this proof.
+
+The formal algebra and the finite linear instruction interface are explicit
+premises. No claim is made that every possible native implementation factors
+through this algebra, or that every physical caller has the exact restoration
+contract. The theorem concerns temporary field count. Precision, tape cost,
+ordinary operation count, a complete supplier, the selected conditional kappa
+and the five framework assumptions remain outside its conclusion.
+
+## Finite corroboration
+
+The standalone checker expands the projectors literally at every paired
+character through six axes. It checks the target ratio through sixteen blocks
+and both query parity choices. Every two-by-two ordinary matrix over a fixed
+eight-element rational alphabet is checked against an independent permutation
+determinant, including singular maps and both query locations. Seeded longer
+words exercise rational nonunit scales, row mixing, swaps and queries,
+checking the invariant at every cut. Explicit changed-model and rank-loss
+controls mark the theorem boundary. These are finite checks of the argument's
+algebra, not a finite search offered as a universal proof.

research/sector-scalar-workspace/README.md

@@ -0,0 +1,82 @@
+# Rational scalar overwrites do not remove the sector workspace field
+
+For every `s>=1` and `r>=1`, the formal Boolean-sector perturbation map
+`x_(b,a) -> (1+q E_a/2)x_(b,a)` requires at least one owned field, even with
+arbitrary rational scalar overwrites and free ordinary linear mixing. Any
+finite number of dirty borrowed fields may be used, provided they are exactly
+restored. The minimum is exactly one, using the cited PR #5658 construction
+for the upper bound.
+
+This is a scoped algebraic proof with finite corroboration. The new result is
+the lower bound in the enlarged alphabet. It resolves the scalar-overwrite
+workspace question explicitly left open in [Ali Romman's PR #5658](https://github.com/CrocSwap/integer-mult-bounds/pull/5658).
+The predecessor's route, cost counts and one-field upper bound are cited,
+not independently replayed or audited here.
+
+Ordinary instructions are matrices over the algebra generated by the commuting
+involutions `J_0=q^2,J_1,...,J_(s-1)`. Native queries multiply one field by
+`q` or `q^-1`. The paired evaluations `q=1` and `q=-1` agree on every
+ordinary coefficient. Thus every zero-owned-field program with nonsingular
+paired outputs has determinant ratio `+1` or `-1`; the target's ratio is `3^r`. [PROOF.md](PROOF.md)
+gives the complete argument and exact instruction boundary.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sector-scalar-workspace/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sector-scalar-workspace/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sector-scalar-workspace
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sector-scalar-workspace --check-source-history
+```
+
+The expected scientific marker is `PASS_SECTOR_SCALAR_WORKSPACE`. Both
+registered commands use explicit checks that remain enabled under `-O`.
+[RESULT.json](RESULT.json) records 63 literal projector characters, 2,016 target
+parity checks, all 4,096 two-by-two ordinary matrices over the declared rational
+alphabet, including 402 singular matrices, and 400 seeded words with 9,600
+checked cuts. Eight scope/rank controls and three invalid-matrix controls mark
+the boundary. The checker prints a generated SHA256 receipt for every package
+file. It writes no files and imports no predecessor implementation.
+
+The all-parameter result is the written proof. Finite corroboration is neither
+a proof-kernel certificate nor independent human acceptance. Source pins in
+[SOURCES.json](SOURCES.json) are historical provenance; the standalone replay
+has no live external inputs. Hosted CI status belongs in the PR, not in this
+proof's claim.
+
+## Limits
+
+The theorem covers fixed finite linear words in the formal faithful-sector
+algebra. It excludes nonlinear or adaptive instructions, discarded borrowed
+outputs and ordinary primitives with additional `q` dependence. Arbitrary
+rational scales are allowed, including nonunits such as `3/2`. The argument
+does not extend the predecessor's `r+1` CLEAR lower bound to that alphabet.
+No physical native realization, complete caller, precision/tape tariff,
+supplier admission or new kappa follows. The selected frontier is unchanged.
+
+## Open next questions
+
+- What is the sharp CLEAR count when arbitrary rational scalar overwrites
+  are allowed? First fix one block and seek an erasure invariant or a cheaper
+  complete word. The predecessor's modulo-three proof no longer applies.
+- Can an actual caller use the sector-supported demand profitably? First pin
+  its complete input/return contract and price shifts, precision and storage.
+  No such caller or complete ledger is supplied here.
+
+## Credit
+
+The new proof and checker were produced by Nick Petalas. Credit Ali Romman
+for PR #5658's butterfly construction, formal contract and explicit broader
+alphabet question, and PR #5626's query interface. Credit Dugongue for T6/T7
+and C8, and the retained Nick Petalas, Cao, DaysSky, Cinna Davis, Ryanson,
+zxv and Jacob Alan Sussman native/controller/compiler lineage. The paired
+character and determinant methods are classical. Independent human and formal
+proof-kernel review are unclaimed. Apache-2.0.
+
+The scientific base is canonical main
+`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216883)
+records the changed alphabet and scope. Text overlap coverage and its limits
+are in [TASK.json](TASK.json).

research/sector-scalar-workspace/RESULT.json

@@ -0,0 +1,10 @@
+{
+  "projector_characters": 63,
+  "target_parity_checks": 2016,
+  "ordinary_matrices": 4096,
+  "singular_matrices": 402,
+  "seeded_words": 400,
+  "checked_word_cuts": 9600,
+  "scope_and_rank_controls": 8,
+  "invalid_matrix_controls": 3
+}

research/sector-scalar-workspace/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/sector-routing-butterfly/README.md",
+      "usage": "provenance",
+      "git_blob": "c5f618d370549f03bf771e215470db2648909a07",
+      "sha256": "6c2a125d25a74ee5d170932fd1fa66d91ade855f519b33c1f48e9b363f9795e2"
+    },
+    {
+      "path": "research/sector-routing-butterfly/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "1e29da09270b673f6e4cdd8c31c07f57af56b60d",
+      "sha256": "dcb3f6bf2715f6aff0efb6b72ac7ff1a56487e1ad8e103793be9eebf6403d5bc"
+    }
+  ]
+}