Audit #4100 COMPLEX.md's common cover and native warps: |O(73,2)|, X_delta correction, stock arithmetic and Z4-monomial warps hold (no new κ)

research/complex-cover-lift-audit/README.md

@@ -0,0 +1,179 @@
+# Audit of #4100 COMPLEX.md: common cover, defect correction and stock arithmetic
+
+**Audit with a positive scoped result; no new κ.** The selected κ is unchanged.
+
+Pinned #4100 head: `337d04939571a637aeab54a0f58f54fde811663a`
+(`research/unconditional-batched-crt/COMPLEX.md`). The provider words are the
+literal PR4088 inputs `research/staged544-mixed-fourth-entry/inputs/{THREE,FOUR}-{base,extra}.json.gz`.
+
+The #4311 coverage map lists "COMPLEX.md's arbitrary-f lift and complete-cover
+execution" with no audit. Its free-word lift row, however, shows #4184
+(ToikY) as positive: an exact formal cancellation on all four PR4088
+programs. This package therefore audits the common-cover algebra: the cover
+size, the terminal `X_delta` defect correction, the `H0` factorization and
+the depth and row-stock arithmetic. It only cross-checks the lift, with
+phase-carrying representations. The complex moment and root are already
+certified by #4171 and are not redone.
+The reading of the rank-r transition (one `C⊗rf` child versus f copies) is
+#4375's subject and is not redone either.
+
+## Results
+
+| Statement in COMPLEX.md | Outcome |
+|---|---|
+| `Gamma = 2^1296 prod_{i=1}^{36}(2^(2i)-1) = |O(73,2)|` | Holds (proof below). Brute-force counts of `O(n,2)` for n = 1, 3, 5, 7 are 1, 6, 720, 1,451,520 = `|Sp(n-1,2)|` (n = 7 with `--full`, about 8 minutes). |
+| `P_g C_all P_g^-1 = C_all X_delta`, `delta_i = (wt(row_i g)-1)/2 mod 2` | Holds for orthogonal g, with or without a translation (proof below). Checked on all of `O(3,2)` and `O(5,2)` and on 400 random elements of `O(73,2)` × 200 vectors each. It fails for non-orthogonal g, and `delta = 0` fails whenever `delta != 0`. |
+| `H0 = ((1-i)/2) D C D`, tensor diagonals `i^wt`, `((1-i)/2)^h` split by parity | Holds exactly (Gaussian rationals), tensor powers h ≤ 6. `H0` is `[[1,1],[1,-1]]/2`. |
+| `D(e) = 1 + D(48 floor(e/73))`; every child decreases D; two levels halve e | Holds (proof below; scanned for e ≤ 2·10^5, and ≤ 2·10^6 in the development run). |
+| Row stock padded to `R = ceil(2^q/M) M`, `M = (W Gamma)^D(h)`, factor below two | Factor below two holds. **Presentational correction:** `R > 2^q` at every tested h (73 … 10^30), so the padded range needs `q+1` reserved bits (or a radix-R field), not `q`. Only a constant changes. |
+| Each native warp is a monomial `i^a` matrix | Holds: all 720 warp edge classes of the four words (`native_warps.py`). |
+| Arbitrary-f lift: each warp generator `G -> G⊗f`, each scalar kept as a scalar, constant monomial phase `i^a -> i^(fa)` | Already audited by #4184 (exact pullback, all 5,784 output functionals). The supplementary check below agrees: there are no complex scalars, and `i^a` monomial representations pass for f = 1, 2, 3. |
+
+## Supplementary lift check (complements #4184)
+
+#4184 proves the formal free-word cancellation exactly and specializes it
+over F101 and the rationals. This section adds two things: the phase/scalar
+separation that COMPLEX.md's `i^a -> i^(fa)` sentence relies on, and
+execution with phase-carrying monomial generators.
+
+**What the certificate is.** In PR4088's exact interpreter
+(`vendor/audit_core.py`) a register value is a dict
+`{(input, reduced word): Fraction}`. Warps are free generators, reduced only by
+`g g^-1 = 1`. Every ADD, SCALE and correction coefficient is a rational. The
+four words have 17,428–17,429 scalars each, all real dyadic rationals (about
+9,040 negative), 72 warp generators and 36 initial corrections. The event kinds
+are only add, scale and warp. So the certificate cancels in `Q[F_72]` and has
+no complex phase coefficient at all. A phase `i^a` can only sit inside a warp
+generator, and it is tensored with that generator to give `i^(fa)`, as
+COMPLEX.md says. A sign or SCALE is a field coefficient and stays scalar.
+
+**Why that suffices.** `w -> rho(w)^(⊗f)` is a group homomorphism of the free
+group for any assignment `rho` of the generators. Extended linearly, it is an
+algebra homomorphism of `Q[F_72]`, and every identity certified in `Q[F_72]`
+survives. Corrections `c G_word x` stay separate terms, giving `G_word^(⊗f)`
+and not `(G_word - I)^(⊗f)`. The dual orientation uses `D_k = K_k^(-T)`, and
+`(K^(⊗f))^(-T) = (K^(-T))^(⊗f)`.
+
+**Execution check.** `verify.py` executes each word end to end with its own
+interpreter. The order is corrections, wrapper, A, cut, B with the warps,
+restore and cleanup, read from the pinned format, with nothing imported. Each
+generator becomes `M^(⊗f)` for a random 4×4 monomial matrix M with entries
+`i^a`, for f = 1, 2, 3. Inputs and the 91 dirty private buffers are random
+complex vectors. In all 24 runs (4 words × 3 widths × forward/dual), the
+contract holds to relative error ≤ 1.7·10^-14:
+
+- targets become `x_t + x_(t-V)` (forward), or sources `x_r - x_(r+V)` (dual);
+- every other live register returns;
+- every private buffer is restored, with no leakage.
+
+**Controls** (`test_verify.py`). Reading every scalar sign as a phase symbol
+breaks the lift. So does replacing each `G^-1` by an unrelated matrix.
+
+## Proofs
+
+**Cover size.** Let n be odd and `j` the all-one vector. For every x,
+`x·x = Σx_i = j·x`. So an isometry g gives `j·(gx) = j·x`, i.e. `g^T j = j`.
+Since `g^T` is also orthogonal, `g j = j`. Because `j·j = 1`,
+`F_2^n = ⟨j⟩ ⊕ j^⊥`, and on `j^⊥` (the even-weight vectors) the form is
+alternating and nondegenerate. Restriction is a bijection
+`O(n,2) → Sp(n-1,2)`: it is injective since g fixes j, and surjective since
+any symplectic map extended by `j ↦ j` is an isometry. At n = 73 this gives
+`2^(36^2) prod(2^(2i)-1)`.
+
+**Defect correction.** Entrywise, `C_all[x,y] = ((1+i)/2)^n (-i)^wt(x⊕y)`.
+With `P_g|x⟩ = |gx⟩`, the identity is equivalent to
+`wt(g^-1 z) ≡ wt(z ⊕ delta) (mod 4)` for all z. Since `g^-1 = g^T`, write
+`g^-1 z = Σ_k z_k c_k` with `c_k` the rows of g. Then
+
+    wt(g^-1 z) ≡ Σ_k z_k wt(c_k) - 2 Σ_{k<l} z_k z_l |c_k ∧ c_l|   (mod 4).
+
+Orthogonality makes each overlap even and each `wt(c_k) = 1 + 2 delta_k`, so
+`wt(g^-1 z) ≡ wt(z) + 2(delta·z)`. In the Hadamard picture
+`C_all = H S H` with `S = diag(i^wt)` and H the unitary Walsh–Hadamard
+transform, `H P_g H = P_(g^-T) = P_g`. So the conjugate is
+`H S' H` with `S' = diag(i^wt(g^-1 y)) = S Z^delta`, and
+`H S Z^delta H = C_all X^delta`. This proves the identity. Comparing the
+`z = 0` entries of both sides then forces `wt(delta) ≡ 0 (mod 4)` for every
+orthogonal g, which the check also observes on every sampled g. A translation `x → x+v` cancels in `x⊕y`.
+Applying the identity on each of the f columns gives `X_delta` columnwise.
+
+**Depth and stock.** `floor(e/73)` is nondecreasing, so D is nondecreasing by
+induction. A child `r floor(e/73)` with `r ≤ 48` has
+`D ≤ D(48 floor(e/73)) = D(e) - 1`. Two levels give at most
+`(48/73)^2 e < e/2`. A node passes `R/(W Gamma)` rows to its children, which
+is divisible by `(W Gamma)^(D-1)`, enough by monotonicity. Parked ancestor
+volumes `V/(W Gamma)^k` form a geometric series. From
+`M ≤ 2^q < 2M` we get `2^q ≤ R < 2^q + M ≤ 2^(q+1)`, with `R > 2^q` unless
+M divides `2^q`. M is divisible by odd primes (for example
+`2^2-1 = 3` divides Gamma), so that never happens for D ≥ 1.
+
+**Height and time (given #4171).**
+- `A(e) ≤ A(48f) + Sf + E` with `e ≥ 73f` gives `A(e) ≤ αe` once
+  `α ≥ (S+E)/25` and α covers the leaves. #4178's incoming height `t0` is a
+  separate reported defect and is not re-examined here.
+- Internal nodes cost `O(V e^(1-a2) polylog p) ≤ O(V e^tau polylog p)`, since
+  `a2 = 0.0017333948 > a_eff`.
+- A leaf of width `l ≤ h^eta` costs `l = l^(1-b) l^b ≤ l^(1-b) h^(eta b)`
+  per volume. The `(1-b)` moment then bounds the leaves by
+  `O(V h^(1-b+eta b))`, and `(1-eta) b > q` gives the stated
+  `O(V h^(1-q) polylog p)`.
+
+## Native warps are Z4 monomials
+
+`native_warps.py` (numpy) answers the native-realization question that #4184 left open. A warp
+event of operator k, moving its lender from frame U to frame E, executes
+`Z = T_E K_G^(±1) T_U^-1` on the lender's 9 hosted axes. Here `K_G` is the
+phase-corrected permutation `|x⟩ → i^(q(Gx)) |Gx⟩`, with q the Z4 form of
+`M = I + G^-T G^-1`, and `T_U = K_c (C on |U| axes) K_c^-1`. These
+definitions are read from PR4088's `bw_gauss.py`; the script imports nothing
+from it.
+
+- **Binding.** Each canonical word (`evidence/{NATIVE,THREE}-CANONICAL-*`, where
+  NATIVE is FOUR by its PHASES hash) matches its literal input word: the same
+  72 warps by B position and G columns, and the same frame spans. Only the
+  register labels are compacted.
+- **Result.** All 180 warp edge classes of each of the four words, 720 in
+  total, give a matrix with exactly one entry per row and column, each in
+  `{1, i, -1, -i}`, global phase included. So every native warp is a monomial
+  `i^a` matrix. Its `⊗f` lift is again monomial, with phase `i^(Σa)`, which is
+  COMPLEX.md's `i^a → i^(fa)` statement. This independently re-derives
+  PR4088's own `PASS_WARP_RECIPES_EXACT_ON_ALL_512_COLUMNS` receipt.
+- **Controls.** The plain permutation `P_G` without the quadratic phase is
+  not monomial on any of 40 tested classes, and swapping the frames breaks 86
+  classes. So the phase correction in `K_G` is essential.
+
+## Not covered
+
+- The composition of these local recipes into the global emitted program,
+  which PR4088's PHASES receipts list as a separate obligation (see
+  `TASK.json`).
+- The rank-r child reading (#4375), and the physical gather/execute schedule
+  and work-slot count of the cover.
+
+## Validation
+
+```sh
+python3.12 -B research/complex-cover-lift-audit/verify.py
+python3.12 -B research/complex-cover-lift-audit/test_verify.py
+python3.12 -B research/complex-cover-lift-audit/native_warps.py   # numpy, about 2.5 min
+python3.12 scripts/research_package.py --package research/complex-cover-lift-audit
+```
+
+The finite checks support the written proofs above; they do not replace them.
+
+## Credit
+
+The construction is by Cinna Davis (#4100, PR4088). The formal lift audit is
+#4184 (ToikY). The exact free-word
+interpreter whose format is read here is by Sagar Thakrar (in PR4088's
+vendor). The coverage map is #4311 (Ryanson Jonathan), the complex moment
+certificate is #4171 (petalas), and the rank-r reading is #4375 (unpaidmoon).
+Prepared for Mark (Matarener) with substantial Claude Code assistance.
+Apache-2.0.
+
+## Open next questions
+
+Does each PR4088 word's global emitted program compose its local frame,
+centre and warp recipes into exactly the free-word shadow? First step:
+regenerate LOCAL-PROGRAMS for one word and check that the frame labels between
+consecutive events cancel exactly. See `TASK.json`.

research/complex-cover-lift-audit/SOURCES.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/unconditional-batched-crt/COMPLEX.md",
+      "usage": "input",
+      "git_blob": "c3be56fbfdb4fb29c1ace88cbcdfa7475fb6e343",
+      "sha256": "853e1295850862752e4f854aa9e8b28f9ca6eaa9306e2af110b7b77526d1b5e1"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/vendor/audit_core.py",
+      "usage": "input",
+      "git_blob": "8b5e1d5f2a106402f036b63028ecef31a4e4c462",
+      "sha256": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/inputs/THREE-base.json.gz",
+      "usage": "input",
+      "git_blob": "137793e275870db2161048405017b83dcc1824ee",
+      "sha256": "df31495cff95a1e512da398f52841c6b5ade29067869b3d68b89d756a5641112"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/inputs/THREE-extra.json.gz",
+      "usage": "input",
+      "git_blob": "7cce921b20dc0504cea954ab3297c5b55a9468dc",
+      "sha256": "9a28f7ef91938c0866e408eb06e03eb5f8e727a00b44eb936ddd5ed48704bd4c"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/inputs/FOUR-base.json.gz",
+      "usage": "input",
+      "git_blob": "65957e5ca322049d985f23fdc0bd8da07ffa4c2a",
+      "sha256": "aecaddba48fdff6353a6511c3623346b05aa607e30103fb016604a2b1025ce95"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/inputs/FOUR-extra.json.gz",
+      "usage": "input",
+      "git_blob": "1f3239c30e9343cf4e34b4371fcbeebb94a19011",
+      "sha256": "615093190aa5479034bb8acdd8925d7a910e082b84dec7df84b459b62421235a"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/evidence/NATIVE-CANONICAL-base.json.gz",
+      "usage": "input",
+      "git_blob": "77ee265be3cc15d76054c023d825578d9c62fa5c",
+      "sha256": "bff67890d0d350646d11f45aa1b098d6a415b1850b4982e8a05b4c146d247eda"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/evidence/NATIVE-CANONICAL-extra.json.gz",
+      "usage": "input",
+      "git_blob": "bc6433bbf5c355d53eec218448fa49c5f4d45346",
+      "sha256": "e0c473d62127a09cb3cbf451564dbdd19c0c10f1674dab0575e65251aa5e1e3c"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/evidence/THREE-CANONICAL-base.json.gz",
+      "usage": "input",
+      "git_blob": "40d74e5638d08ccb0b8270e6c47843cc45762c72",
+      "sha256": "f07fae1011160b53e2df1f3135465db1277a093319de2a1da52d648f00a39542"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/evidence/THREE-CANONICAL-extra.json.gz",
+      "usage": "input",
+      "git_blob": "2af11b77b0d1f9ed54584fb1ec63f808d08071e6",
+      "sha256": "882271d70602354cbada8d77f479703ccc6c47e689e8ccd91f9e4c87de0f4379"
+    }
+  ]
+}

research/complex-cover-lift-audit/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "One #4100 obligation group: COMPLEX.md's common cover (Gamma=|O(73,2)|, the X_delta defect correction, H0 factorization, depth and row-stock arithmetic), plus a supplementary phase-representation check of the arbitrary-f lift already audited by #4184.",
+  "scope_change_reason": "The #4311 coverage map lists COMPLEX.md's complete-cover execution with no audit; its free-word lift is covered by #4184, so this package audits the cover algebra and only cross-checks the lift.",
+  "bottleneck_link": "Side result for the #4100 admission audit: confirms one all-size premise group of the proposed unconditional exponent; it does not move the selected frontier.",
+  "budget_minutes": 90,
+  "stop_rule": "Stop after the cover algebra and the lift of the literal PR4088 words are proved or refuted; do not re-derive the complex moment (#4171) or the rank-r child reading (#4375).",
+  "outcome": "completed",
+  "evidence": "Written proofs in README.md; verify.py binds sources and runs the finite cover checks and the supplementary lift; native_warps.py shows every native warp edge class of the four PR4088 words is a Z4-monomial matrix; test_verify.py has rejecting controls.",
+  "author": "Mark (Matarener)",
+  "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.",
+  "open_questions": [
+    {
+      "question": "Does the expanded global emitted program of each PR4088 word compose its local frame, centre and warp recipes into exactly the free-word shadow (the scalar-interface integration that PR4088's PHASES receipts list as a separate obligation)?",
+      "why_it_matters": "The lift proof needs each executed event to be the representation of its free symbol in context; local recipes are now checked, their global composition is not.",
+      "first_step": "Regenerate LOCAL-PROGRAMS for one word with PR4088's emitter and check that the frame labels between consecutive events cancel exactly (global phase included).",
+      "blocked_by": "none"
+    }
+  ]
+}