Prove the exact fixed-cubic coframe rank frontier (no new κ)

research/fixed-cubic-coframe/PROOF.md

@@ -0,0 +1,167 @@
+# Exact fixed-cubic coframe frontier
+
+This is a scoped rank-graph theorem with a concrete Clifford realization. It
+does not optimize an unrestricted circuit or change the selected supplier.
+
+## Contract and result
+
+For an integer m >= 1 let V = F2^m plus F2^m, with
+
+```
+omega((x,z),(y,w)) = x.w + z.y
+S(x,z) = (z,x+z)
+L0 = {(0,z): z in F2^m}
+d(A,B) = m - dim(A intersect B), for Lagrangians A,B.
+```
+
+Fix one internal Lagrangian L. Both its entrance from L0 and its exit to L0
+are paid. Every internal occurrence of the prescribed transport S must use
+this same L. Write
+
+```
+a = d(L0,L), b = d(L,S L).
+```
+
+The exact componentwise minimal attainable pairs are
+
+```
+(a,b) = (j,m-2j),  j = 0,...,floor(m/2).                 (1)
+```
+
+In particular, all charts satisfy 2a+b >= m and b = m modulo 2. Every
+feasible pair is dominated by a pair in (1), and every pair in (1) is
+attained. This characterizes the Pareto frontier, not every attainable pair.
+
+Let phi be increasing and concave on [0,m], with phi(0)=0, and let k>0.
+The exact minimum complete graph bill is
+
+```
+min_L [2 phi(a) + k phi(b)]
+  = min(k phi(m), 2 phi(floor(m/2)) + k phi(m mod 2)).   (2)
+```
+
+For the power tariff phi(r)=r^t, 0<t<=1, and even m, division by m^t gives
+
+```
+normalized optimum = min(k, 2^(1-t)).                  (3)
+```
+
+For odd m the exact unnormalized value is
+
+```
+min(k m^t, 2 ((m-1)/2)^t + k).                         (4)
+```
+
+Thus two copies and two prescribed native occurrences have normalized bill
+2^(1-t), strictly below the one-copy value 2 for every t>0. Both boundary
+transitions are included. At t=1 the values are respectively 1 and 2.
+
+The contract requires a common internal coframe. Different coframes at
+different occurrences and replacement of the prescribed word by another
+word are excluded. In particular S^3=I permits cancellations in unrestricted
+synthesis. The theorem makes no lower-bound claim for that larger problem.
+
+## Lower bound and parity
+
+The distance d is invariant under symplectic transport and satisfies the
+triangle inequality. Indeed dim(A intersect C) is at least
+dim(A intersect B)+dim(B intersect C)-m, by applying the dimension formula
+inside B. Since L0 and S L0 are complementary, d(L0,S L0)=m. Hence
+
+```
+m <= d(L0,L) + d(L,S L) + d(S L,S L0) = 2a+b.          (5)
+```
+
+Put W=L intersect S L. The polynomial identity S^2+S+I=0 implies
+S^-1=I+S. If v is in W, then v is in L and S^-1 v is in L. Consequently
+S v = v+S^-1 v is in L. Also S v is in S L. Thus W is S-invariant.
+
+The polynomial X^2+X+1 is irreducible over F2. On W, multiplication by its
+class X can therefore be defined as S, making W a vector space over F4.
+Its binary dimension m-b is even. This proves b=m modulo 2. No estimate
+from a finite search is used here.
+
+For any attainable pair, put j=(m-b)/2. Parity makes j an integer in
+[0,floor(m/2)], and (5) gives j<=a. Once attainment below is proved,
+(j,m-2j)=(j,b) dominates the original pair. The displayed pairs are mutually
+incomparable, which establishes exactly the frontier (1).
+
+## Attainment
+
+Use the coordinate symplectic planes with bases e_i,f_i. On each of j
+disjoint pairs of planes use the two-dimensional subspace
+
+```
+span(e_(2i-1)+e_(2i), f_(2i-1)+f_(2i)).
+```
+
+The displayed generators pair to zero because 1+1=0 in F2. Their span is
+Lagrangian in its four-dimensional block and is S-invariant. Its
+intersection with L0 has dimension one. On each remaining plane use the
+original line span(f_i). Its intersection with its S-image is zero.
+
+Taking their direct sum gives a Lagrangian with a=j and b=m-2j. Every
+rank in (1) is therefore attained for every positive m.
+
+After restriction to (1), the objective is
+f(j)=2 phi(j)+k phi(m-2j). It is concave as a function of real j on
+[0,floor(m/2)]. A concave function is at least the smaller of its two
+endpoint values. Both endpoints are attainable. This proves (2), and
+(3)-(4) follow by substitution. No numerical root calculation is needed.
+
+## A phase-exact Gaussian-dyadic witness
+
+Let H_g=(1+i)[[1,1],[1,-1]]/2, P=diag(1,i), and U=-P H_g. These are
+Gaussian-dyadic Clifford matrices. Direct multiplication gives U^3=I,
+U X U*=Z, and U Z U*=Y. Thus U induces exactly S on Pauli labels.
+Put
+
+```
+B = CNOT (H_g tensor I), M = B* (U tensor U) B.
+```
+
+B takes the standard Z chart to the paired-plane chart above. It has
+Fourier rank one; U tensor U has rank two; M is monomial and has rank zero.
+The exact monomial phases and its four columns are generated in RESULT.json.
+The full forward and inverse identities are
+
+```
+B M B* = U tensor U
+B M* B* = (U tensor U)*.
+```
+
+They hold on every input, by equality of the full matrices. For any positive
+integer k, B M^k B*=(U tensor U)^k. The graph invoice is therefore two
+rank-one boundary children and k rank-zero internal occurrences, compared
+with k rank-two occurrences in the original common chart. Tensoring these
+blocks and adding an unpaired U supplies the general attaining recipe.
+No relative or global phase is discarded. A monomial internal operator
+still has ordinary arithmetic, routing and precision costs; zero Fourier
+rank is not zero machine cost.
+
+## Relation to earlier work
+
+Ali Romman's PR6171 proves tensor reduction for a fixed scalar contact
+graph with fixed repeated canonical boundaries and no prescribed native
+transport equation. That theorem is a cited predecessor, not an object of
+verification here. Its projection inequality is credited to Cinna Davis /
+PR5140, and the canonical subspace-frame construction to icekylinx.
+
+The present positive-cost graph prescribes S on a loop at its internal
+chart. It therefore changes the native-transport hypothesis excluded by
+PR6171. The invariant paired chart demonstrates why that excluded
+hypothesis matters, with both boundary costs paid. PR6172's signed graph
+instead varies productive boundaries and has negative edges; it supplies
+neither this transported model nor this optimum. Classical symplectic
+distance, F4 linear algebra and Bell-basis facts are background. The new
+contribution is the exact paid rank frontier and all-width tariff formula
+for this specified common-coframe native contract.
+
+Ross Richardson / PR4081 supplies an earlier Gaussian order-three tensor
+family and its distinct whole-bank quadratic-response restriction. No new
+gate family or quadratic-response theorem is claimed here. The present
+objective prices a conjugated native map rather than requiring every
+tensor power to satisfy U_m^2+U_m+I=0.
+
+This contribution was produced by Nick Petalas. Independent human and
+formal proof-kernel review are unclaimed. Apache-2.0.

research/fixed-cubic-coframe/README.md

@@ -0,0 +1,127 @@
+# Exact paid frontier for a fixed cubic native coframe
+
+This contribution was produced by Nick Petalas. It is a scoped proof with
+exact finite corroboration and a phase-exact Clifford circuit witness.
+No new kappa or selected-frontier change is claimed.
+
+## Result
+
+On m repeated binary symplectic planes, prescribe S(x,z)=(z,x+z). Choose
+one internal Lagrangian L, retain the standard boundary L0 at both ends,
+and charge both entrance and exit. Each prescribed S occurrence must use
+that same internal coframe. Put a=d(L0,L), b=d(L,S L).
+
+The exact Pareto frontier is (j,m-2j), for 0<=j<=floor(m/2). All charts
+obey 2a+b>=m and b=m modulo 2. For any increasing concave tariff phi with
+phi(0)=0 and positive loop weight k, the exact full graph optimum is
+
+```
+min(k phi(m), 2 phi(floor(m/2)) + k phi(m mod 2)).
+```
+
+For phi(r)=r^t, 0<t<=1, and even m, its normalized value is
+min(k,2^(1-t)). Two copies and two native occurrences improve the
+one-copy value 2 to 2^(1-t), with both boundary children paid. For odd m
+the exact unnormalized optimum is min(k m^t,2((m-1)/2)^t+k).
+
+[PROOF.md](PROOF.md) gives the universal proof, explicit attaining charts,
+and an actual Gaussian-dyadic two-plane circuit. Its conjugated internal
+operator is monomial, with every phase retained. This settles the exact
+cost of this transported common-coframe contract; it does not extend
+Ali Romman's PR6171 tensor-reduction theorem to prescribed native maps.
+That theorem and its explicit native-equation limitation are cited, not
+audited or replayed.
+
+## Evidence and reproduction
+
+Use CPython 3.12 with its standard library, from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fixed-cubic-coframe/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/fixed-cubic-coframe/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fixed-cubic-coframe
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fixed-cubic-coframe --check-source-history
+```
+
+A clean CPython 3.12 interpreter can replace the absolute local path.
+Expected direct output:
+
+```
+PASS_FIXED_CUBIC_COFRAME lagrangians=2448 constructions=288 concave_tariffs=200 rejections=12
+```
+
+The verifier enumerates every Lagrangian for m=1,2,3,4 using unique RREF
+bases. Literal point-set intersections independently check both distances
+and the S-invariance of L intersect S L. Every efficient pair is checked,
+as are the complete optimums for 200 exact rational concave-hinge/weight
+fixtures. Another 288 constructions cover all efficient pairs for m<=32.
+The exact Gaussian-rational checker compares full 2x2 and 4x4 matrices,
+both Pauli-generator images, actual cubic order, unitarity, all forward
+and inverse columns, and both charged boundary ranks. Omitting the exit
+fails. Twelve domain/rank/isotropy controls reject. Checks remain active
+under optimized Python. Finite evidence corroborates the written proof;
+it is not a proof of the all-width theorem by extrapolation.
+
+RESULT.json is generated by the verifier and binds every other package
+file by SHA256. To regenerate it, pass
+`--write-receipt /absolute/scratch/path/result.json`, then compare that
+file with the committed receipt. Ordinary replay never writes files or
+regenerates an absent receipt. No predecessor source is imported or run.
+SOURCES.json pins citation/provenance bytes in canonical Git history.
+
+## Scope and implementation limits
+
+The common internal coframe and prescribed native occurrences are part of
+the model. Time-varying coframes, changing the scalar word, and synthesis
+that shortcuts U^k are excluded. U^3=I is an immediate reason unrestricted
+synthesis can have a different optimum. This is a local changed-model
+result, not a rank optimum or emitted word for P104. Rank-zero native
+operators still have ordinary costs. Dirty-helper hosting, rounded
+precision, tape movement, stock, compiler closure, productive output
+delivery, the BIT interface and the outer theorem are unpriced here.
+No selected cold replay, Lean or Docker run, physical supplier admission,
+complete multiplication theorem, or independent human/formal review is
+claimed.
+
+The reference construction supports m<=32, with at most 64 binary
+coordinates and 64 rows per elimination. Exhaustive RREF enumeration is
+capped at m<=4, with at most 16 free bits per pivot set and 70 pivot
+sets. Literal sets have at most 16 points; dense matrices are at most
+4x4. Functions are below 60 lines, control flow is nonrecursive, and
+explicit exceptions enforce capacities and mathematical invariants.
+Warning-strict normal and optimized replay provide the available Python
+diagnostics. Power-of-Ten rule 3 has a managed-runtime deviation: Python
+allocates integers, Fractions and finite collections during this bounded
+one-shot computation. The stated caps bound live mathematical data.
+No fixed-allocation or real-time implementation is asserted.
+
+## Open next questions
+
+- Does an actual complete supplier have repeated cubic native operations
+  whose common coframe can be replaced by these paired charts? Start with
+  one named source interval, retain every scalar contact and productive
+  endpoint, and price both boundaries plus ordinary monomial work.
+  A source-compatible physical word and complete caller bill are missing.
+- What is the exact optimum if each native occurrence may choose a
+  different coframe while the original scalar contacts are retained?
+  Start with a short explicit graph rather than erasing its common-chart
+  equalities. The present theorem intentionally fixes those equalities.
+
+TASK.json records the changed card scope, stopping rule and structured
+questions. The first verified result is packaged without a wider search.
+
+## Credit
+
+Ali Romman / PR6171 supplies the tensor-reduction question and its
+native-transport limitation. Cinna Davis / PR5140 retains the projection
+inequality; icekylinx retains the canonical subspace-frame construction.
+Nick Petalas / PR6172 supplies a distinct signed-boundary result.
+Cao Yifan, Dugongue, Cinna Davis and the
+retained native/helper/caller/compiler lineage retain their contributions.
+Ross Richardson / PR4081 retains the earlier cubic native tensor-family
+and response-gate results; the new result is not a new gate family.
+Classical symplectic geometry, F4 linear algebra and Bell-basis identities
+are not claimed as new. The exact frontier and its complete charged
+common-coframe tariff formula were produced by Nick Petalas.
+Independent human and formal proof-kernel review are unclaimed.
+Apache-2.0.