Research: prove four-site idle-rank rigidity under the fixed schedule

research/idle-four-site-rigidity/PROOF.md

@@ -0,0 +1,197 @@
+# Four idle positions cannot exchange rank across the fixed schedule
+
+This is a scoped mathematical proof under the inherited completed-call
+contract, with a finite source check. It is not a proof-assistant verification
+or an audit of the native implementation of that contract.
+
+## Statement and assumptions
+
+Fix one replica, one port, and cover identity in the pinned data schedule.
+Number its streams `(X0,Y0,X1,Y1,X2,Y2,X3,Y3)` by `0,...,7`.
+Allow simultaneous replacements of idle children **8, 10, 12, 13** only.
+At each position, both the original and replacement child have a linearly
+independent axis set in `F_2^m`, followed by an optional address translation.
+An orthonormal axis set, as required by the source construction, is sufficient.
+
+Assume:
+
+1. A completed child with axes `A` and translation `t` acts on its one physical
+   stream as the product of the `C_v` for `v in A`, followed by `X_t`, in the
+   source convention below. The number of independent axes is its rank.
+2. Every operation outside the four positions is fixed. The completed local
+   data calls are the source F/B shears conjugated by diagonal Fourier frames;
+   completed hosted-helper actions on this replica/port are nonzero diagonal
+   multipliers. They keep the character fixed. In particular, a replacement
+   cannot silently alter a hosted helper, its frame, or its scheduling.
+3. The unchanged prefix, intervening operator and suffix are invertible on
+   arbitrary inputs to the eight streams. Equality means equality of these
+   physical operators, not equality on a proper subspace of inputs.
+
+**Theorem.** If the replacements preserve the physical operator for every
+Fourier character at cover identity, then each child separately preserves
+its Fourier phase function and its rank. In particular, arbitrary matched
+swaps, cycles and simultaneous changes confined to these four positions
+cannot change any of their individual ranks.
+
+There is no assumption that different children's axis sets are orthogonal,
+that the combined multiset of axes is retained, or that only a few axes move.
+Preserving the operator over every cover implies preserving it at cover
+identity, so this necessary condition suffices to rule out a rank change.
+No claim that cover identity alone suffices for full admission is needed.
+
+## 1. The schedule separates the two phase positions
+
+All event indices below are zero-based. `verify.py` derives them from
+`TEMPLATE.json.gz` and checks the physical child mappings against `PLAN.json.gz`.
+The exact input pins are in [SOURCES.json](SOURCES.json).
+
+| Event | Operation | Streams mixed |
+|---|---|---|
+| 14 | idle children 8, 10 on pair 3 | diagonal on 6, 7 |
+| 15 | bridge, pair 2 receiving from pair 3 | 4, 5, 6, 7 |
+| 16 | local stage 6 on pair 2 | 4, 5 |
+| 17 | idle children 9, 11 on pair 3 | diagonal |
+| 18 | inverse bridge, pairs 2 and 3 | 4, 5, 6, 7 |
+| 19 | local stage 7 on pair 3 | 6, 7 |
+| 20 | local stage 8 on pair 3 | 6, 7 |
+| 21 | idle children 12, 13 on pair 0 | diagonal on 0, 1 |
+
+For a fixed character `u`, write `M(u)` for everything strictly between events
+14 and 21, including any interleaved completed hosted-helper phases. Put
+`V = span(e_0,e_1)`. Every listed factor preserves `V`; so does every diagonal
+frame or helper factor allowed by the contract. The factors are invertible:
+F/B and bridges are elementary shears and the diagonal factors are nonzero.
+Consequently `M` is invertible and `M(V)=V`. Neither the values of its phases
+nor the actual hosted occupancy are needed for this fact.
+
+Write the original interval as `D_B M D_A`, where `D_A` acts only on streams
+6, 7, and `D_B` only on streams 0, 1. Primes denote the replacement factors.
+Cancel the unchanged invertible prefix and suffix from physical equality.
+Then multiply on the left by `D_B^(-1)` and on the right by `D_A^(-1)`:
+
+```
+D'_B M D'_A = D_B M D_A
+E_B M E_A = M,
+E_B = D_B^(-1) D'_B,   E_A = D'_A D_A^(-1).
+```
+
+For every `v in V`, `E_A v = v`, so `E_B M v = M v`. Since `M(V)=V`,
+`E_B` is identity on `V`. It is identity off `V` by its support, hence
+`E_B=I`. Invertibility of `M` then gives `E_A=I`. The four diagonal entries
+are individual child multipliers, so **each of the four phases is unchanged**.
+Apply the same argument separately at every `u`.
+
+This strengthens the single-stream interval argument in Nick Petalas's
+[PR #3187](https://github.com/CrocSwap/integer-mult-bounds/pull/3187), following
+Gareth Davidson's physical-stream obstruction in
+[PR #1387](https://github.com/CrocSwap/integer-mult-bounds/pull/1387).
+The two-coordinate invariant subspace makes the argument simultaneous and
+removes the need to isolate one moved axis by choosing a character.
+
+## 2. Polarization recovers rank from a child's phase
+
+In the source convention,
+
+```
+X_v f(x) = f(x+v),
+C_v = ((1+i) I + (1-i) X_v)/2.
+```
+
+For `chi_u(x)=(-1)^(u dot x)`, the multiplier of `C_v` is
+`i^(u dot v mod 2)`, and that of `X_t` is `(-1)^(u dot t mod 2)`.
+Thus a child has multiplier `i^q(u)`, where
+
+```
+q_A,t(u) = sum_{v in A} (u dot v mod 2) + 2(u dot t mod 2)  (mod 4).
+```
+
+For bits `a,b`, `a+b-(a xor b)=2ab`. Therefore the even residue
+`q(u)+q(w)-q(u+w)` can be divided by two as a map from `{0,2}` in `Z/4`
+to `F_2`, giving
+
+```
+B_q(u,w) = (q(u)+q(w)-q(u+w))/2
+         = sum_{v in A} (u dot v)(w dot v)
+         = u^T P_A w                 (over F_2),
+P_A = sum_{v in A} v v^T.
+```
+
+The translation term disappears: its contribution before reduction is
+`4(u dot t)(w dot t)`. Let `R` be the `r by m` binary matrix with the axes
+as rows. Then `P_A=R^T R`. Because the rows are independent, `R:F_2^m -> F_2^r`
+is surjective and `R^T:F_2^r -> F_2^m` is injective. The image of `R^T R`
+is exactly the image of `R^T`, which has dimension `r`. Hence
+
+```
+rank_F2(P_A) = r = |A|.
+```
+
+Equal phase functions have equal polar forms. If both axis sets are
+independent, their ranks are therefore equal, even if their translations
+and their bases differ. Combining this with section 1 proves the theorem.
+Notice that this rank argument does not require a nondegenerate restriction
+of the dot product to the axis span.
+
+## 3. An exact, small representation of phase equality
+
+Expanding a binary parity modulo four gives
+
+```
+q(u) = sum_j d_j u_j + 2 sum_{j<k} (P_A)_{jk} u_j u_k  (mod 4),
+d_j = sum_{v in A} v_j + 2t_j  (mod 4).
+```
+
+Terms of degree three or more have coefficients divisible by four.
+Consequently a complete phase signature consists of the linear residues
+`d_j` and the off-diagonal binary coefficients of `P_A`. The diagonal of
+`P_A` is redundant, equal to `d_j mod 2`, but is retained for rank computation.
+Equivalently the phase is determined by `q(e_j)` and `q(e_j+e_k)` for `j<k`.
+At `m=73` these are **2,701 nonzero character values**, rather than `2^73`.
+The checker computes the coefficients directly; it does not enumerate the
+large character domain. This is a representation of one child's phase,
+not a 2,701-probe completeness theorem for an arbitrary eight-stream circuit.
+
+## 4. Application, coverage and boundaries
+
+The pinned phase catalogue contains 112 ports. At each port the four **full
+recipe** axis sets at positions 8, 10, 12, 13 are orthonormal and rank 48.
+`verify.py` checks all 448 sets and their polar ranks. Where these four
+children are unhosted, the theorem rules out the target `[51,51,51,39]`,
+as well as every other change of those four ranks, with the rest fixed.
+For a hosted instance the same theorem preserves the original residual rank
+at each position; the full-recipe rank 48 must not be substituted for it.
+
+This package does **not** reconstruct the T740 fill or certify that these
+four positions are unhosted at every replica/port. The current literal
+unhosted witness and its hosting chronology were checked in #3187; #3196
+extends the occupancy-bound paired census over all 112 ports of replica zero.
+Our source check authenticates the common template, plan and full phase
+catalogue. Their completed helper semantics remain an inherited assumption.
+
+The proof is not a general barrier to better suppliers. It excludes rank
+redistribution at exactly four fixed positions. Other positions, changed
+intervening interactions, changed child semantics or a different input/output
+contract require a new argument. It does not audit native words, the all-size
+compiler, precision, tape recovery, or outer analytic assumptions. It gives
+no new kappa and does not assert full correctness of the baseline supplier.
+
+The verifier includes controls demonstrating these limits:
+
+- In dimension six, standard axes and the six vectors `63 xor (1<<j)` are
+  different orthonormal bases with the **same phase**. Rank rigidity does
+  not imply basis uniqueness.
+- In dimension four, standard axes and `15 xor (1<<j)` have equal polar
+  matrices but different phases (`u=1` is a witness). Translation 15 repairs
+  the difference. A polar matrix alone is insufficient for phase equality.
+- Four copies of axis 1 have zero phase. Without independence, the number
+  of axes is not recovered by polar rank.
+- If `M` swaps streams 0 and 6, the phase changes `(3,0,1,0)` satisfy
+  `E_B M E_A=M`. This violates the invariant-subspace hypothesis and admits
+  a transfer. A singular zero `M` also accepts nontrivial changes, showing
+  why cancellation needs invertibility.
+
+The finite checks are independent arithmetic controls and source-hypothesis
+checks, not the logical justification for the unrestricted theorem. That
+justification is the argument in sections 1 and 2.
+
+Tekalign (@tekuuu), with substantial OpenAI Codex assistance. Apache-2.0.

research/idle-four-site-rigidity/README.md

@@ -0,0 +1,129 @@
+# Four-site phase rigidity closes the rank-changing swap/cycle question
+
+**Scoped negative result, with a written proof and exact source checks. No new
+kappa or admitted supplier.** Under the inherited completed-call contract,
+every operator-preserving replacement of idle children **8, 10, 12, 13** in
+the fixed schedule preserves **each child's rank separately**. This includes
+arbitrary simultaneous independent-axis replacements, not just single moves,
+paired transfers, matched swaps or short cycles.
+
+The reason is structural. The interval between the two idle events preserves
+the receiver's two-dimensional coordinate subspace, forcing all four phase
+functions to remain unchanged. The binary polar form of an independent-axis
+child's Z4 phase has rank equal to its number of axes. Equal phases therefore
+force equal ranks. The [proof](PROOF.md) states the assumptions and derives
+both steps; no enumeration of candidate assignments is needed.
+
+This answers the four-position matched-swap/cycle question left open by
+[Gonzalo-Mier's #3196](https://github.com/CrocSwap/integer-mult-bounds/pull/3196)
+and the finite assignment experiment in
+[#3199](https://github.com/CrocSwap/integer-mult-bounds/pull/3199), inspected at
+`ba34486f40f558fe3ac57bdb1ec263daeaa3fb5b` (including its same-centre
+star isolation argument).
+It extends the physical-stream obstruction of Gareth Davidson/#1387 and
+Nick Petalas/#3187; it does not replace or re-credit those discoveries.
+
+## What this saves and what it does not establish
+
+A packing optimizer confined to these four positions cannot achieve a
+rank-changing improvement without changing the schedule or another premise.
+For an unhosted baseline of four rank-48 children, this excludes the proposed
+`[51,51,51,39]` profile and every other changed rank profile. The fixed rank
+profile also fixes any recursive charge depending only on those four ranks;
+the theorem does not exclude savings in frame costs from rank-preserving
+basis changes.
+
+There is also a compact equality representation: a child's entire phase on
+`F_2^73` is determined by **2,701** linear/quadratic coefficients (equivalently,
+its values on singleton and pair characters). This can reject incompatible
+child phases before an expensive physical replay. Equal polar matrices alone
+are insufficient; the linear residues modulo four must also match. This is
+not a completeness bound for testing an arbitrary eight-stream circuit.
+
+The source checker validates all **448 full recipe bases across 112 ports**,
+their rank 48, the physical child mapping, and the unmixed coordinate cut.
+It does not rebuild the T740 fill. Rank 48 therefore describes the full
+recipe axes, not a newly verified claim about all hosted residuals. The
+theorem also applies to residual subsets, preserving their own starting
+ranks while hosted operations remain fixed. The actual unhosted witness and
+helper chronology remain credited to #3187/#3196.
+
+Changed interactions, additional changed child positions, dependent-axis
+implementations and new local contracts are outside this result. It neither
+certifies the baseline supplier nor audits native words, the all-size compiler,
+precision, tape recovery or outer analytic assumptions. The selected record
+and frozen predecessor packages are unchanged.
+
+## Reproduce
+
+From the repository root, Python 3.12 or later, standard library only:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/idle-four-site-rigidity
+```
+
+Expected verifier markers:
+
+```text
+PASS_IDLE_FOUR_SITE_RIGIDITY ports=112 axesets=448 full_recipe_ranks=48,48,48,48 phase_tuples=8192
+PASS_IDLE_FOUR_SITE_EXPORT optimized_runs=6 rejecting_controls=3
+```
+
+For a Git-free source export containing this package and the three live input
+paths in [VERIFY.json](VERIFY.json), the direct command is
+`python3 -I -B research/idle-four-site-rigidity/verify.py`.
+`--emit-result` prints the deterministically recomputed receipt; normal replay
+compares it with [RESULT.json](RESULT.json) and writes no generated artifacts.
+The registered runner additionally checks historical Git provenance.
+
+Controls cover all 1,447 independent axis sets in dimensions one through four
+(22,584 full-character evaluations), all 256 four-phase tuples for each of
+32 deterministic diagonal fixtures (seed 40), and five rejected source-schedule
+mutations. Positive boundary controls include equal phases from different
+bases, a translation repair, and a transfer after changing the interval to
+cross the invariant cut. The export tests exercise optimized Python, missing
+or changed source bytes, receipt type mutation, and formatting invariance.
+These finite controls check the implementation and hypotheses; the unlimited
+assignment statement rests on the written proof, not on their coverage.
+
+Base: `463113d675af7410ac91d53a4fed51ec6494eb9a`, priority revision 6.
+[SOURCES.json](SOURCES.json) pins input bytes, Git blobs and predecessor proof
+provenance. [TASK.json](TASK.json) records OS assignment seed 40, the explicit
+task-card scope change, candidate selection, coverage and stopping rule.
+[Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-19001658).
+
+## Open next questions
+
+The structured handoffs are in [TASK.json](TASK.json). A changed interaction
+crossing the invariant cut is a concrete escape: first price its complete
+bridge, frame, copy, restoration and recursive-child costs. The verifier's
+stream-swap control is only an algebraic example, with no supplier budget.
+
+Other sets of idle positions need their own phase insertion equation and
+source-derived invariant-subspace test. Ross Richardson's
+[concurrent handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/2612#discussioncomment-18999338),
+updated at 17:25 UTC on 2026-10-17, reports a broader normalized twenty-slot
+obstruction with local-only evidence. We credit that report without claiming
+exclusive priority or auditing its unpublished argument. This package supplies
+a separate, source-bound four-position proof, its phase-rank implication and
+compact phase representation; no result from that handoff is used as a premise. The four-position theorem does not
+rule out proposals involving additional hosted-remainder positions.
+
+## Credit
+
+Gareth Davidson (@bitplane), #1387, established the physical-stream obstruction
+on selected #1094 inputs. Nick Petalas, #3187, bound a literal counterexample
+to the current candidate and proved the single-receiver-line interval argument.
+Gonzalo-Mier, #3196/#3199, supplied paired/single-transfer censuses and exposed
+the simultaneous-assignment question. The axis rule and star lineage retain
+Gonzalo-Mier/#1252, Guéorgui Maissouradze/#1276 and Jeremy Kothe/#1324's credit.
+
+The current fill and word context retain Jeremy Diviney/#3148, dcharb78/#3133,
+Marius-Paul Dumitrean/#2979, Rohan Arun/#3184 and the predecessor packages'
+full selected-supplier lineage. No predecessor code is imported by this checker,
+and no fill or native-word evidence is regenerated or claimed as new here.
+
+The simultaneous four-site proof, phase-rank application and independent
+checker are by Tekalign (@tekuuu), with substantial OpenAI Codex assistance
+in research, code, checking and writing. Author-checked, without independent
+human or proof-kernel review. New work is Apache-2.0.