Prove sharp C tensor prefix scales with integral endpoints (no κ)

research/native-c-endpoint-prefix-scale/PROOF.md

@@ -0,0 +1,145 @@
+# Sharp scale for endpoint-integral native C tensors
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+Put `O=Z[i]`, `pi=1+i`, and
+
+```text
+C = [[1+i,1-i],[1-i,1+i]]/2
+  = pi^-1 [[i,1],[1,i]].
+```
+
+For `f>=1`, let `C_a` apply C on binary address bit a, and set
+`F=C_0 ... C_(f-1)`. Let `C_S=product_(a in S) C_a`. Distinct axes
+commute. The endpoint-promised input domain is
+
+```text
+L_f = {x in O^(2^f) : F x in O^(2^f)}.
+```
+
+Both the input and final output are exact Gaussian integers. No assumption
+about intermediate integrality is made. Arbitrary signs, imaginary parts
+and independent spectator fibres are allowed.
+
+## Theorem
+
+For every `S subset {0,...,f-1}`, put `j=|S|` and `d=min(j,f-j)`.
+The least nonnegative integer e such that
+
+```text
+pi^e C_S L_f is contained in O^(2^f)
+```
+
+is exactly `d`. The least nonnegative integer s such that
+`2^s C_S L_f` is integral is exactly `ceil(d/2)`.
+
+Consequently the least common Gaussian scale for every partial axis product
+is `pi^floor(f/2)`, and the least common binary scale is
+
+```text
+2^ceil(floor(f/2)/2).
+```
+
+The same common scales are minimal for the prefixes of any single fixed
+axis ordering. They suffice for every ordering simultaneously. Minimality
+is over all inputs in `L_f`, rather than for each individual input.
+
+## Upper bound from the two endpoints
+
+Direct multiplication gives
+
+```text
+pi C       = [[i,1],[1,i]],
+pi C^-1    = [[1,i],[i,1]],
+C^2        = [[0,1],[1,0]],
+C (1,1)^T  = (1,1)^T.
+```
+
+In particular, `pi C` and `pi C^-1` are Gaussian integral. If `x in L_f`
+and `y=F x`, then
+
+```text
+C_S x is in pi^-j O^(2^f),
+C_S x = C_(S complement)^-1 y is in pi^-(f-j) O^(2^f).
+```
+
+For nonnegative a,b, the two fractional modules are nested and their
+intersection is `pi^-min(a,b) O^(2^f)`. This proves the bound d, using
+only the two endpoint promises. Since `pi^2=2i`, multiplying by
+`2^ceil(d/2)` clears those denominators.
+
+## Matching input at every cut
+
+Pair d distinct axes in S with d distinct axes outside S. On each pair
+use the integer array
+
+```text
+v = e_00 + e_11.
+```
+
+On every unpaired axis use `u=e_0+e_1`. Let x be their tensor product,
+with factors placed on the specified axes. This has only zero/one real
+entries and zero imaginary parts.
+
+The complete transform fixes u and sends each v to `e_01+e_10`.
+Indeed C is symmetric and `C^2` is the bit swap, so this identity follows
+by multiplying the displayed two-by-two matrices. Thus both x and F x
+are Gaussian integral, and x belongs to `L_f`.
+
+At the chosen cut, exactly one axis in each pair has been transformed.
+Its four entries, in address order, are
+
+```text
+(C tensor I) v = pi^-1 (i,1,1,i).
+```
+
+The same identity holds with the pair's axes exchanged. The unpaired u
+factors remain fixed. Every coordinate of `C_S x` is therefore a Gaussian
+unit times `pi^-d`. A Gaussian unit is not divisible by pi. Hence no
+smaller exponent e can clear the Gaussian denominator.
+
+Multiplication by `2^s` increases pi divisibility by exactly `2s`, because
+`2=-i pi^2`. The same example is integral after that multiplication if
+and only if `2s>=d`. This proves the binary lower bound. At a middle cut
+of any fixed ordering, `d=floor(f/2)`, proving both common-scale minima.
+
+## Arithmetic interface consequence
+
+Suppose a supplied array x and its intended `F x` are Gaussian integral.
+Scale the input by the theorem's common binary factor, apply the ordinary
+axis sequence, then divide the completed output by the same factor.
+Every axis output is integral, and the final division is exact. The
+returned mathematical output is exactly `F x`.
+
+This statement is an arithmetic composition. It supplies neither a
+literal scaling program nor a signed-range bound. An implementation must
+still pay both conversions, preserve ownership, allocate sufficient
+intermediate signed width and scratch, and admit its actual producer's
+endpoint promise. The argument applies independently to every spectator
+fibre of the positive rank-one native leaf, so it covers arbitrary f in
+the stated tensor model without asserting physical implementation.
+
+## Relation to earlier work and scope
+
+Jerry Chen / CubeJerry's PR7429 defines this positive C tensor at selected
+MOVE24472 and requires every axis output to be integral and fit the signed
+width. Its f=2 example already distinguishes final and intermediate
+integrality. That distinction and the machine implementation are credited
+premises, not new findings or replay targets here.
+
+Jose Manuel / jmbarrancoml's PR3091 supplies the physical axis method and
+retains Alejandro Zarzuelo Urdiales's sharp `ceil(f/2)` binary reserve for
+arbitrary inputs. The new bound uses the additional *integral final
+output* premise, so it does not replace that unrestricted-input reserve.
+
+Clear1nsight's PR3382 characterizes the integral entrance on which every
+partial coordinate product is already integral. That maximal exactness
+lattice is an established result. The proof here does not reconstruct
+or use its characterization. The new result is the exact scalar needed
+to move the larger endpoint-promised domain into every partial-product
+integrality domain, with a matching input at every cut.
+
+No denominator theorem for arbitrary Clifford words, intervening
+noncommuting maps, nonintegral final outputs or rounded trajectories is
+asserted. The statement concerns exactly the commuting coordinate C
+tensors defined above. All five selected framework assumptions remain.

research/native-c-endpoint-prefix-scale/README.md

@@ -0,0 +1,149 @@
+# Sharp integral-prefix scale for the positive native C tensor
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped written proof with exact finite corroboration.
+No new kappa or selected-frontier change is claimed.
+
+For `C=[[1+i,1-i],[1-i,1+i]]/2`, suppose both x and `C^(tensor f) x`
+are Gaussian-integer arrays. The least common binary input scale making
+every axis prefix integral is exactly
+
+```text
+2^ceil(floor(f/2)/2).
+```
+
+More precisely, at any cut with j processed axes, the sharp Gaussian
+denominator exponent is `min(j,f-j)`, in units of `pi=1+i`. The sharp
+binary scale at that cut is `2^ceil(min(j,f-j)/2)`. This covers every
+subset of axes and therefore every fixed axis order. It allows arbitrary
+Gaussian-integer inputs satisfying the final-output promise, with arbitrary
+spectator fibres.
+
+[PROOF.md](PROOF.md) proves the all-f statement. From the input, the cut
+has at most j Gaussian denominator factors. From the integral output, its
+inverse suffix has at most f-j. Paired-coordinate integer inputs attain
+the smaller exponent at every cut.
+
+## What changes
+
+Jerry Chen / CubeJerry's [PR7429](https://github.com/CrocSwap/integer-mult-bounds/pull/7429)
+implements this tensor as the positive rank-one central leaf of selected
+MOVE24472. It requires integral, width-fitting outputs at every axis and
+already gives an f=2 example with integral endpoints but a nonintegral
+intermediate. That example and the implementation are credited prior work.
+
+The new arithmetic bridge is to multiply an endpoint-promised input by the
+sharp scale, run the ordinary axes with exact divisions, and divide the
+completed output by the same scale. Every intermediate axis output is
+integral and the original mathematical output is returned exactly.
+
+The unrestricted-input reserve `ceil(f/2)` is established prior work,
+retained in Jose Manuel / jmbarrancoml's [PR3091](https://github.com/CrocSwap/integer-mult-bounds/pull/3091)
+and credited there to Alejandro Zarzuelo Urdiales. The smaller exponent
+here uses an additional endpoint promise. Clear1nsight's
+[PR3382](https://github.com/CrocSwap/integer-mult-bounds/pull/3382) characterizes
+the different entrance where all partial products are already integral.
+Neither predecessor theorem nor executable is audited or replayed here.
+
+## Exact finite evidence
+
+The standard-library checker imports no predecessor code. It checks:
+
+- 164 sharp cut witnesses, covering every axis subset through f=6 and
+  every prefix cut for f=7 through 10. Each also executes the complete
+  scaled arithmetic program and exact final division.
+- All 65,808 Gaussian arrays with real and imaginary components in `{0,1}`
+  for f=1,2,3. Exactly 968 have integral final outputs; all their 3,792
+  checked prefixes satisfy both denominator bounds. The other 64,840
+  inputs are outside the promised endpoint domain.
+- 180 signed complex prefixes checked against a separately coded rational
+  butterfly, with direct tensor-entry comparisons through f=4.
+- All 153 axis permutations at f=1 through 5 on the paired witnesses.
+- Eight named semantic controls, including a scale one bit too small at
+  f=6, a missing endpoint promise, inexact divisions, inverse-phase
+  confusion and a signed complex dirty offset.
+
+Finite checks corroborate the written proof. They do not enumerate the
+unbounded input lattice. Every acceptance check remains active under `-O`.
+The verifier writes nothing and prints a generated receipt containing the
+results, Python version and SHA256 of every package file. No receipt is
+hand-written or checked in.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/native-c-endpoint-prefix-scale/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/native-c-endpoint-prefix-scale/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/native-c-endpoint-prefix-scale
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/native-c-endpoint-prefix-scale --check-source-history
+```
+
+Substitute any installed CPython 3.12 path on another host. Expected markers
+are `PASS_NATIVE_C_ENDPOINT_PREFIX_SCALE`, `PASS_REGISTERED_RESEARCH_PACKAGE`
+and, after committing, `PASS_RESEARCH_COMMIT_BYTES`. The standalone verifier
+also works in a Git-free package copy. Each registered command has a
+120-second cap. Normal and optimized direct runs take less than a second
+locally; these are check durations, not physical performance measurements.
+
+## Scope and source boundary
+
+The claim is a new numerical interface theorem for a stated tensor, with
+no changed supplier word. It does not establish that a production caller
+supplies the endpoint promise. Signed range, scratch width, physical
+scaling/unscaling, ownership, tape movement, compiler closure, stock and
+the complete paid/productive invoice remain separate obligations. All five
+selected framework assumptions remain. No native machine, selected cold
+replay, Lean, Docker or complete multiplication theorem is run or claimed.
+Independent human and formal proof-kernel review are unclaimed.
+
+The base is canonical main `e54523517d0f03e58352e647c403a5af3e525a57`,
+priority revision 8, selected #7000. [TASK.json](TASK.json) records the
+explicit change from the formal-interface card to this written arithmetic
+proof. [SOURCES.json](SOURCES.json) pins canonical provenance only. The
+definition and proof are self-contained, with no external executable or
+data inputs. TASK also records #7429's exact head, README path and the SHA256
+of the source text inspected. That external document is provenance, not a
+registered replay dependency or an asserted independently certified input.
+
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19571939).
+Live claims, the account's recent contributions, the main-tree READMEs and
+merged PRs were checked for the formula, tensor, endpoint promise and more
+general partial-product forms. The overlap snapshot reported complete
+pagination of 760 open PRs and 7,346 Discussion records, without warnings.
+No same-scope result was found in that coverage. Arbitrary unpublished work
+and unsearched diffs remain outside it.
+
+Power of Ten inspection found no recursion, dynamic evaluation, subprocesses
+or writes in the verifier. All arithmetic domains are fixed: f is at most
+10, arrays have at most 1,024 entries, and the exhaustive loop has at most
+65,536 cases at one f. Every function is under 60 physical lines. All gates
+use exact integers or Fractions and explicit failure checks. Receipt hashing
+caps the inventory at twelve files and each file at 1 MiB. Managed Python
+allocation is a deviation from fixed steady-state allocation; the fixed
+domains bound live collections, but runtime allocation internals are not
+measured. Warning-strict normal and optimized execution supplies the available
+diagnostics; no separate static analyzer or native fixed-allocation version
+is supplied.
+
+## Open next questions
+
+Can the sharp scale be installed around one literal positive C leaf with
+a favorable complete physical bill? First supply an actual producer with
+the required endpoint promise, bound every scaled intermediate magnitude,
+and price both exact conversions together with movement, owners and retained
+history. Those missing contracts prevent a supplier or kappa claim. This
+package stops at the first sharp arithmetic result and reserves no follow-up.
+
+## Credit
+
+The new proof, matching all-cut witnesses and checker were produced by
+Nick Petalas. Jerry Chen / CubeJerry supplies PR7429's literal leaf and its
+explicit integrality boundary. Jose Manuel / jmbarrancoml supplies PR3091's
+physical axis method, retaining Alejandro Zarzuelo Urdiales's C/parity and
+tensor-reserve credit. Clear1nsight supplies PR3382's maximal simultaneous
+exactness lattice. The selected native, Gaussian, controller and physical
+lineage retains its predecessor credit. Fractional-ideal arithmetic and
+tensor-product identities are classical; no literature-wide priority is
+claimed for those methods.

research/native-c-endpoint-prefix-scale/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/physical-gaussian-leaf/README.md",
+      "usage": "provenance",
+      "git_blob": "573a0c3c9df984a397c112026dfc2d8e2cc94c66",
+      "sha256": "60f82399ac13f3c0f1f10de6488021b64240711190a09962568f2d72ea302eb0"
+    },
+    {
+      "path": "research/p104-clifford-exactness/README.md",
+      "usage": "provenance",
+      "git_blob": "581edcfcbcc31cf78c02f9873c14094f9b37e1bf",
+      "sha256": "7374b6b360fa6755f68ee513467de1c0436a48a22a9584a3c27687e73a16a7db"
+    }
+  ]
+}