Prove sharp paid-history threshold for phase-complete Pauli operations (no new kappa)

research/pauli-twisted-history-threshold/PROOF.md

@@ -0,0 +1,127 @@
+# Sharp paid-history threshold for the phase-complete Pauli alphabet
+
+Let K=Q(i), X=[[0,1],[1,0]], Z=diag(1,-1), and
+G=<iI,X,Z>. This is the 16-element group of actual matrices
+{i^c X^u Z^v: 0<=c<4, u,v in {0,1}}. Its projective quotient has
+four classes. At each positive width f define P=X^tensor f,
+C=Z^tensor f and R=span_K{I,P,C,PC}. Ordinary operations are left
+actions from R, arbitrary K-linear row combinations, COPY and CLEAR.
+Scalar coefficients, word lengths and choices may vary with f.
+
+Begin with ordinary combinations of N independent whole-field inputs,
+including every independent dirty input, and zero scratch. A paid call
+acts on one actual current field and returns one additional K-linear row
+(not assumed linearly independent of earlier rows) at
+the same capacity. It may depend on earlier paid outputs and need not
+commute with R. Conceptually retain all actual paid rows after overwrites
+or clears. No freely supplied nonordinary initial observation is allowed.
+
+For q distinct input owners v_j, request H_j w_vj up to ordinary initial
+backgrounds, where H_j=(a_j I+b_j X)^tensor f and
+a_j b_j (a_j^2-b_j^2) != 0. Correctness is on the entire independent
+input space. Then every such program has at least q paid returns for
+every f>=2. At f=1 all targets are ordinary and zero returns suffice.
+If each H_j is an available paid primitive, q direct calls attain the
+bound for f>=2. Without this last hypothesis this is a lower bound,
+not a supplier construction or an attainable native-call count.
+
+## 1. Exact phases and actual algebra
+
+The lift of i^c X^u Z^v is i^(cf) P^u C^v. In particular,
+PC=(-1)^f CP, P^2=C^2=I. Phases merge into K scalars; the algebra is
+the actual matrix image, not the untwisted group algebra of four labels.
+For positive f the four matrices I,P,C,PC are independent. To see this,
+use the X-eigenbasis of each tensor factor: P is diagonal with entry
+(-1)^k on a binary string of weight k, and C maps each string to its
+complement. The diagonal supports I,P are disjoint from the complement
+supports C,PC; within each pair both parities occur. Thus dim R=4.
+R is commutative at even f and noncommutative at odd f.
+
+For one target write l+=a+b and l-=a-b. Both are nonzero. In this basis
+H is diagonal with entry t_k=l+^(f-k) l-^k. For 0<=k<=f-2,
+
+    t_k - t_(k+2) = 4ab l+^(f-k-2) l-^k != 0.             (1)
+
+The basis change is an exact invertible common conjugation, used only
+in the proof; it is not granted as a free physical instruction.
+
+## 2. Odd widths at least three: full module separation
+
+Suppose A H belongs to R, where A=alpha I+beta P+gamma C+delta PC.
+The diagonal entries of AH on parity epsilon are
+(alpha+beta epsilon)t_k. An ordinary matrix has a constant diagonal
+coefficient on each parity. Compare k=0,2 in even parity and k=1,3 in
+odd parity. By (1), alpha+beta=alpha-beta=0, hence alpha=beta=0.
+
+At row complement(s), column s, the remaining entry is
+(gamma+delta (-1)^(f-k))t_k. Ordinary complement entries are constant
+within each input parity. The same two comparisons give
+gamma-delta=gamma+delta=0 at odd f, hence gamma=delta=0. This uses
+characteristic zero, invertibility of l+,l- and f>=3. Therefore
+
+    R intersect R H = {0}.                               (2)
+
+This proof allows coefficients in the full actual R. It does not
+pretend its odd-width matrix blocks are one-dimensional characters.
+
+Represent current fields as rows in End_K((K^2)^tensor f)^N. Let I0=R^N.
+After m returns t_1,...,t_m, every available field belongs to
+M=I0+sum_j R t_j: ordinary operations preserve it, and each paid
+call adjoins its actual output row. Thus dim M <=4N+4m. Each target
+generates R H_j e_vj, of dimension four because H_j is invertible.
+Equation (2) separates it from the ordinary row at that owner, and
+distinct owners separate the q modules from one another. Consequently
+dim M >=4N+4q and m>=q. A growing finite N or finite word length
+cancels at each width independently.
+
+## 3. Even widths at least two: one actual character suffices
+
+Now P,C commute. Set E=(I+P)(I+C)/4. It is a nonzero idempotent,
+EP=EC=E, so ER=K E. This assertion would be false at odd widths.
+In the same tensor eigenbasis, on every even-weight string s,
+E has entry 1/2 at (s,s) and at (s,complement(s)); odd-weight rows
+are zero. Complements are distinct at every positive width.
+
+The diagonal entries of EH at weights zero and two are t_0/2 and
+t_2/2. Both corresponding entries of E are 1/2. Their difference is
+2ab l+^(f-2), nonzero by (1). Hence EH is not a scalar multiple of E,
+including at f=2. This does not require R intersect RH to vanish.
+
+Project all history rows on the left by E. Initial projected history
+is the direct sum of K E at each independent owner. Since ER=K E,
+each actual paid return can enlarge this projected span by at most
+one dimension. Each requested EH_j e_vj adds one new dimension modulo
+initial history; distinct owners make these q directions independent.
+Therefore m>=q. This projection is an analysis of information already
+available, not a free additional paid call or an assumed field split.
+
+## 4. Sharp threshold, scope and predecessor distinction
+
+At f=1, R=M_2(K) and h_j=a_j I+b_j X is ordinary. This proves the
+width-one exception. With H_j available, one call on each original
+owner gives the matching upper bound. Calls can preserve originals
+by the allowed ordinary COPY; independent dirty inputs are not used
+as zero scratch. No claim is made about a more restricted paid alphabet.
+
+PR5446's general projective-coset theorem gives only f>=2p-1=7 here.
+PR5450 proves threshold two for the smaller R=span{I,X^tensor f}.
+Its projector (I+P)/2 does not have one-dimensional ER for the enlarged
+group: the extra C direction survives. The even-width projector and
+odd-width full module argument above discharge that missing implication.
+The history-dimension method and classical Pauli/character algebra are
+credited, not claimed as new general theorems.
+
+Free initial paid history can invalidate the count. Repeated owners
+cannot each be charged; projectively ordinary targets such as 2X cost
+zero despite lying outside the finite G. If a=0 or b=0 the target is
+ordinary; if a=+/-b the invertibility and comparisons used in the odd
+case fail. Changing geometry, cross-column ordinary operations,
+multiple independent outputs per call, nonlinear input-dependent
+programs and approximation are excluded. This standalone theorem does
+not establish a charge at a cached physical caller boundary, a new
+recursive profile, precision/tape costs, or an integer-multiplication kappa.
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+Predecessor credit: Chris R / Clear1nsight and PR5425/5446's retained
+history authors; Ali Romman's PR5450; classical tensor-power separation,
+finite group representation theory and the retained native/compiler lineage.

research/pauli-twisted-history-threshold/README.md

@@ -0,0 +1,124 @@
+# Full-Pauli paid history has sharp width threshold two
+
+The standalone one-return-per-owner lower bound survives enlarging the ordinary
+alphabet from `{I,X}` to the full phase-complete Pauli group `<iI,X,Z>`.
+For targets `(aI+bX)^tensor f` with `ab(a^2-b^2) != 0`, width one costs zero
+in this ordinary model; every width at least two requires at least q new
+single-row paid returns for q distinct independent input owners. The matching
+q-call upper bound requires each requested target operator to be an available
+paid primitive. This is a scoped algebraic result, with no new kappa.
+
+The [uniform proof](PROOF.md) accounts for the actual phase factor
+`(X Z)^tensor f = X^tensor f Z^tensor f` and
+`X^tensor f Z^tensor f = (-1)^f Z^tensor f X^tensor f`.
+At even widths, a one-dimensional character detects all requested owners.
+At odd widths at least three, the proof uses full ordinary/target module
+separation. The one-character argument from the smaller alphabet does not
+survive unchanged: its projected ordinary span has dimension two here.
+
+This answers the larger-group next question in
+[PR5450](https://github.com/CrocSwap/integer-mult-bounds/pull/5450).
+[PR5446](https://github.com/CrocSwap/integer-mult-bounds/pull/5446)'s general
+projective-group theorem gives only width at least seven when p=4. Its valid
+general proof is not repaired or replaced. At width two the full ordinary
+and target spans intersect in dimension two, so demanding disjoint full
+spans would miss the sharp bound. [SOURCES.json](SOURCES.json) records exact
+immutable proof citations and hashes of the inspected UTF-8 text.
+
+## Verification
+
+```sh
+python3.12 -B scripts/research_package.py --package research/pauli-twisted-history-threshold
+# Git-free direct commands, from any directory:
+python3.12 -I -B /path/to/package/verify.py
+python3.12 -I -O -B /path/to/package/verify.py
+python3.12 -I -B /path/to/package/check_modular.py
+python3.12 -I -O -B /path/to/package/check_modular.py
+python3.12 -I -B /path/to/package/test_mutations.py
+```
+
+All commands use only the standard library and explicit checks active under
+optimization. The first engine uses exact Gaussian rationals and literal
+Kronecker matrices, cross-checked against an independent Hamming-distance
+entry formula. [RESULT.json](RESULT.json) records 24 complete tensor cases,
+all 64 actual phase-group lifts across four widths, 18 full owner/history
+checks, 366 scalar identities and 13 boundary controls. The source
+square-root-of-X target is included. Owner rows retain an independent dirty
+coordinate and check that duplicate owners or a supplied cached target cannot
+be charged again. Other controls cover ordinary scalar multiples, singular
+targets, zero coefficients, invalid widths and using the even projector at
+odd width.
+
+The separate `check_modular.py` imports no primary-engine code. It constructs
+the operators directly from bit indices and uses independent modular Gaussian
+elimination: 512 complete target cases over F5 and F13, eight phase twists,
+eight projectively ordinary controls and 3,072 nonzero separation identities.
+These finite-field checks exercise the algebra; they are not physical Q(i)
+input tests. Neither executable proves the all-width theorem: that reasoning
+is in PROOF.md. Separate peer review and any limitations are reported with
+the publication rather than inferred from a PASS marker.
+
+Six additional semantic mutants run in disposable files under optimized Python,
+with receipt comparison disabled. They must fail at named predicates when
+width-dependent phase is dropped, the odd algebra is made commutative, the
+smaller projector is reused, the target coefficient sign changes, singular
+targets are accepted, or a cached target is charged again. These controls
+change no frozen source and cannot pass merely because RESULT.json differs.
+
+The package has no external executable input and imports no predecessor code.
+Public proof citations are not Git-object replay dependencies, so the
+predecessors' unmerged commits are not needed for cold execution. The only
+Git provenance pins are the task catalogue and selected record at the
+canonical base. The official committed exporter therefore needs no
+`--input-ref`; it preserves the unchanged package manifest. Source-history
+validation checks those declared provenance pins, not the availability or
+truth of the cited external proofs. The new argument is self-contained.
+
+## Scope and coordination
+
+The full initial state is independent, with only ordinary observations and
+zero scratch. Ordinary coefficients and finite word lengths may vary with
+width; paid calls may have feedback and need not commute with ordinary maps.
+Each call returns one actual transformed whole-field row at fixed capacity.
+The proof explicitly retains every paid output after overwrite or clear.
+It assumes neither a free arbitrary matrix coefficient nor multiple outputs
+from one call. A common eigenbasis is a proof device, not a free instruction.
+
+No actual parent-cut observation ledger is supplied. Cached paid history,
+dependent owners, noninvertible targets, cross-column ordinary operations,
+nonlinear programs, multiple-output paid calls and approximate recovery need
+different arguments. Physical phase/compiler admission, recursive profiles,
+precision, storage, tape cost and the selected frontier remain outside this
+result. It does not certify a complete multiplication theorem.
+
+[Discussion5476](https://github.com/CrocSwap/integer-mult-bounds/discussions/5476)
+is the canonical investigation. The base is
+`32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority revision seven.
+The scope change from the historical uniform-transfer card is explicit in
+[TASK.json](TASK.json). Initial overlap covered 342 open PRs and 4,736
+Discussion records with complete pagination, plus the latest released
+handoffs; public cached prose does not exclude unpublished work.
+PR5449's general finite history quotient and PR5447's physical input kernels
+are separate scopes. No physical application is inferred from either.
+
+## Open next questions
+
+Bind this lower bound to one actual versioned physical cut, including every
+cached observation and owner. Without that ledger the standalone hypothesis
+cannot justify another caller charge. A further target-family extension needs
+one justified physical target and a concrete cost consequence; this proof
+does not classify arbitrary Pauli-nonordinary matrices. See TASK.json for the
+first steps and blockers.
+
+## Credit
+
+Chris R / Clear1nsight and the retained PR5425/5446 authors supply the
+paid-history argument and general projective separation. Ali Romman's
+PR5450 supplies the smaller bit-flip specialization and larger-group handoff.
+Classical Pauli representation theory, involution characters, tensor-power
+separation and the retained native/helper/compiler/analytic lineage retain
+their credit. No predecessor implementation is imported.
+
+JoyboyBrian, with substantial OpenAI Codex assistance in proof, exact
+implementation, controls and writing. Apache-2.0. No independent human or
+formal-kernel acceptance is claimed.