Show the #4100 common-cover row pad does not fit

research/complex-cover-row-reservation/PROOF.md

@@ -0,0 +1,150 @@
+# The #4100 common-cover row reservation does not fit
+
+Audited text: `research/unconditional-batched-crt/COMPLEX.md`, section
+"Common cover, fresh rows and fixed tapes", bytes identical at base
+`fbc9ea0249746acca4f504d4fda2b84e0e36cf0d` and at the retained #4100 head
+`337d04939571a637aeab54a0f58f54fde811663a`. The obligation named in that
+package's `AUDIT.md` is the arbitrary-`f` complete-cover execution. This note
+audits the row-bit reservation and the group order that execution cites. It
+does not accept #4100 and does not change the selected frontier.
+
+## Statement
+
+Let `W = 322560` and let
+
+```text
+Gamma = 2^1296 * product_{i=1}^{36} (2^{2i} - 1).
+```
+
+`COMPLEX.md` says `Gamma = |O(73,2)|`, reserves
+
+```text
+q = ceil(log2((W Gamma)^{D(h)}))
+```
+
+row bits, and pads the complete range to
+
+```text
+R = ceil(2^q / (W Gamma)^{D(h)}) * (W Gamma)^{D(h)},
+```
+
+"a factor less than two."
+
+For every integer `D >= 1`, that `R` equals `2N` with `N = (W Gamma)^D`, so
+the factor `R/N` equals 2, and `R` is strictly larger than the reserved
+`2^q` addresses. The same `q` does hold exactly one copy of `N`, and
+`1 < 2^q/N < 2`. The group order itself is the integer `Gamma`.
+
+## The dot-product group has order Gamma
+
+Let `n = 2m + 1` and let `V = F_2^n` with `B(x,y) = sum_i x_i y_i`. The matrix
+of `B` is the identity, so `B` is nondegenerate. Let `1` be the all-ones
+vector. Then `B(1,1) = n mod 2 = 1`, and `B(x,x) = B(x,1)`.
+
+Let `U = 1^perp`. Then `dim U = 2m`. Every `x in U` has `B(x,x) = 0`, so `B`
+restricted to `U` is alternating. It is nondegenerate: a vector of `U` orthogonal
+to all of `U` is orthogonal to `V = U ⊕ <1>`, hence is zero.
+
+Let `O` be the group of linear automorphisms of `V` that preserve `B`.
+Every `g in O` fixes `1`. Indeed `B(gx,gx) = B(x,x)` gives `B(gx,1) = B(x,1)`,
+so `g^T 1 = 1`. Preservation of `B` is `g^T g = I`, so `g^T = g^{-1}` and
+therefore `g 1 = 1`.
+
+Restriction to `U` is an isomorphism `O → Sp(U,B)`. It is a homomorphism into
+the symplectic group. It is injective because a map that fixes `1` and fixes
+`U` is the identity. It is surjective: for `S in Sp(U)` the rule
+`g(u + a 1) = S(u) + a 1` is linear, and
+
+```text
+B(Su + a 1, Sw + b 1) = B(Su, Sw) + ab B(1,1) = B(u,w) + ab,
+```
+
+since `Su` and `Sw` lie in `U`. The right-hand side is `B(u + a 1, w + b 1)`.
+
+An ordered symplectic basis of a `2m`-dimensional space is chosen one hyperbolic
+pair at a time. In dimension `2k` there are `2^{2k} - 1` choices for the next
+nonzero vector and `2^{2k-1}` vectors pairing with it to `1`. The stabilizer of
+a full basis is trivial, so
+
+```text
+|Sp(2m,2)| = product_{k=1}^{m} (2^{2k} - 1) 2^{2k-1}
+          = 2^{m^2} product_{i=1}^{m} (2^{2i} - 1).
+```
+
+At `m = 36` the right-hand side is `Gamma`. The prose sentence that the all-ones
+vector has norm 1, that its perpendicular space is symplectic of dimension 72,
+and that one counts successive symplectic pairs, is this identification.
+Thus `Gamma = |O(73,2)|` for the standard dot product. The integer has 2628
+bits. Its decimal SHA-256 is
+`50b58aaac98e621e9917d6c3bced5e276398b68918bbd57ac8d784d3d58db00b`.
+
+The verifier enumerates both groups for `n = 1, 3, 5` (so `m = 0, 1, 2` on the
+symplectic side, with the `m = 0` orthogonal count equal to 1) and checks that
+every orthonormal basis sums to the all-ones vector. It also checks that the
+two product writings agree for every `m <= 36`.
+
+## The displayed pad does not fit
+
+Factor `W = 2^{10} * 315` with `315 = 3^2 * 5 * 7`. Every term `2^{2i} - 1` is
+odd, and `2^2 - 1 = 3`, so the odd part `Odd` of `Gamma` is an odd multiple of
+`3`. Hence
+
+```text
+W Gamma = 2^{1306} * M_1,    M_1 = 315 * Odd,
+```
+
+with `M_1` odd and `M_1 >= 945`. For an integer `D >= 1`,
+
+```text
+N = (W Gamma)^D = 2^{1306 D} * M_1^D.
+```
+
+The odd part `M = M_1^D` satisfies `M >= 945 > 1`, so `N` is not a power of two.
+Let `q = ceil(log2 N)`. Then `2^{q-1} < N < 2^q`, so `1 < 2^q / N < 2` and
+
+```text
+ceil(2^q / N) = 2,    R = 2N.
+```
+
+In particular `R/N = 2`, which is not strictly less than two, and
+`R = 2N > 2^q`, so `R` is not a subset of the `q` reserved bits.
+
+The repair inside the same bit budget replaces `ceil` by `floor`. Then
+`floor(2^q / N) = 1`, and the only positive multiple of `N` that fits in
+`2^q` addresses is `N` itself. The reservation factor `2^q / N` lies in the
+open interval `(1, 2)`. Holding the written range `R = 2N` instead would take
+`q + 1` bits, because `2^q < 2N < 2^{q+1}`. Either repair leaves the row-bit
+count at `log2(N) + O(1) = O(D log(W Gamma))`. The sentence as written describes
+neither a fitting range nor a factor strictly less than two.
+
+`D(h) >= 1` for every width `h >= 73`, by the recurrence in the same paragraph,
+so the failure applies at every recursive node that reserves row bits.
+
+## The depth recurrence does halve
+
+The same paragraph defines `D(e) = 0` for `e < 73` and
+`D(e) = 1 + D(48 floor(e/73))` otherwise, and says that every child of rank
+`r <= 48` decreases `D` and that two levels halve `e`.
+
+`D` is nondecreasing. For the inductive step at `f >= 73`, the argument
+`48 floor(f/73)` is strictly smaller than `f`, and `t(e) = 48 floor(e/73)` is
+nondecreasing, so the claim reduces to the inductive hypothesis on that
+smaller argument.
+
+For `e >= 73` and `1 <= r <= 48` the child width
+`c = r floor(e/73)` is at most `48 floor(e/73)`, hence
+`D(c) <= D(48 floor(e/73)) = D(e) - 1`.
+
+Let `e1 = 48 floor(e/73)` and `e2 = 48 floor(e1/73)`. Then
+`e2 <= 48^2 e / 73^2`. Since `2 * 48^2 = 4608 < 5329 = 73^2`,
+`(48/73)^2 < 1/2`, so `2 e2 < e`. Two maximum-rank steps more than halve the
+width. This half of the paragraph stands. It is not the padding claim.
+
+## What this does not establish
+
+The fitting copy `N` is still one `W` by `Gamma` by remaining-stock product.
+This note does not bound the parked ancestor volumes, does not build the
+depth-first tapes, and does not execute a transversal of `O(73,2)`. The
+free-word cancellation audited in #4184, the rank-`r f` moment sign in #4375,
+and the common-grid height defect in #4178 are different sentences.
+No selected-frontier change is claimed.

research/complex-cover-row-reservation/README.md

@@ -0,0 +1,92 @@
+# Common-cover row reservation in #4100
+
+**Negative result on one displayed formula. No new κ.** The selected frontier
+stays `0.00302015`. #4100 is not accepted.
+
+## Scope and evidence
+
+Card `uniform-transfer-audit`, scope **refined**. The card asks for one
+quantified implication of the proposed all-size construction at its actual
+caller. This package takes the complete-cover execution named in
+`AUDIT.md`: the row-bit reservation in `COMPLEX.md`, section "Common cover,
+fresh rows and fixed tapes."
+
+`COMPLEX.md` sets `W = 322560` and
+
+```text
+Gamma = 2^1296 * product_{i=1}^{36}(2^{2i}-1),
+```
+
+calls `Gamma` the order of `O(73,2)`, reserves `q = ceil(log2(N))` row bits for
+`N = (W Gamma)^{D(h)}`, and pads to
+
+```text
+R = ceil(2^q / N) * N,
+```
+
+"a factor less than two."
+
+For every integer `D >= 1`, `N` is not a power of two. The displayed `R` equals
+`2N`, so the factor is 2, and `R` is strictly larger than the `2^q` reserved
+addresses. Replacing `ceil` by `floor` leaves exactly one copy of `N` inside
+those addresses, and the reservation factor `2^q/N` lies in `(1, 2)`. Holding
+the written `2N` addresses would take one extra bit. Either repair stays in the
+same `O(D log(W Gamma))` bit budget. The sentence as written does not.
+
+The order claim is the other half of the same sentences, and it holds.
+`Gamma` equals the order of the standard dot-product orthogonal group on
+`F_2^{73}`: the all-ones vector has norm 1, its perpendicular space is
+symplectic of dimension 72, and counting hyperbolic pairs gives
+`|Sp(72,2)| = Gamma`. The integer has 2628 bits. The depth recurrence in the
+same paragraph does decrease on every rank-`r <= 48` child, and two maximum-rank
+steps halve the width.
+
+The proof is `PROOF.md`. `verify.py` binds the audited sentences, checks the
+2-adic failure for `D = 1..4`, enumerates the dot-product and perpendicular
+groups at dimensions 1, 3 and 5, and checks the depth inequalities through
+width `100000`.
+
+This is not the free-word cancellation in #4184, the rank-`r f` moment sign in
+#4375, the common-grid height defect in #4178, or the BIT.md stock audit in
+#4432.
+
+## Reproduce
+
+From the repository root, with Python 3.12:
+
+```sh
+python3 -B research/complex-cover-row-reservation/verify.py
+python3 -B scripts/research_package.py --package research/complex-cover-row-reservation
+```
+
+Expected verifier line:
+
+```text
+PASS_COMPLEX_COVER_ROW_RESERVATION gamma_bits=2628 gamma_sha256=50b58aaac98e621e9917d6c3bced5e276398b68918bbd57ac8d784d3d58db00b written_factor=2 written_fits=false repair_copy=1 repair_factor_lt_2=true depth_halves=true dot_orders=1,6,720 no_new_kappa
+```
+
+Pins are in `SOURCES.json`. Base `fbc9ea0249746acca4f504d4fda2b84e0e36cf0d`.
+The audited `COMPLEX.md` blob is also the blob at retained head
+`337d04939571a637aeab54a0f58f54fde811663a`.
+
+## Open next questions
+
+1. Once the fitting stock is the single copy `N`, do the depth-first parked
+   ancestor volumes still form a geometric series bounded by a constant times
+   the child payload `V/(W Gamma)`? The time section charges parking inside
+   `O(V e^{1-a2} polylog(p))`. The first step is to write the parked volume at
+   depth `k` from the product split into `W` families, one `Gamma` cover, and
+   the remaining stock. This package does not replay the four provider words
+   or the tape schedule.
+2. `Gamma` is a finite cardinality, not an executed transversal. A constructive
+   cover still needs an encoder that turns one symplectic basis of the
+   72-dimensional perpendicular space into the fixed control `COMPLEX.md`
+   allows. The integer has 2628 bits, so listing the group is not a next step.
+
+## Credit
+
+The construction and the audited sentences are Cinna Davis's #4100, with
+OpenAI Codex assistance. The coverage map that left this execution unaudited
+is Ryanson Jonathan's #4311. #4184 (ToikY), #4178 (Jose Manuel), #4375, and
+#4432 (Mark / Matarener) are neighbouring audits of different sentences.
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

research/complex-cover-row-reservation/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/unconditional-batched-crt/AUDIT.md",
+      "usage": "input",
+      "git_blob": "cd59c5e786a3d37de027b8d0f7376fbb00d52efd",
+      "sha256": "2a6c84ba32c6febee0cbc205210a8935c481d40ec1d52d621442e03221cacc3d"
+    },
+    {
+      "path": "research/unconditional-batched-crt/COMPLEX.md",
+      "usage": "input",
+      "git_blob": "c3be56fbfdb4fb29c1ace88cbcdfa7475fb6e343",
+      "sha256": "853e1295850862752e4f854aa9e8b28f9ca6eaa9306e2af110b7b77526d1b5e1"
+    }
+  ]
+}

research/complex-cover-row-reservation/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "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": "Audit the arbitrary-f complete-cover row reservation in COMPLEX.md: the displayed ceil pad R = ceil(2^q/N)*N does not fit in the q reserved row bits for any D>=1, while floor leaves exactly one copy and 1<2^q/N<2. Gamma equals the dot-product orthogonal order |O(73,2)|. The depth recurrence halves. This is not a free-algebra cancellation, a moment sign, or an acceptance of #4100.",
+  "scope_change_reason": "The card asks for one quantified implication at its actual caller. The #4311 coverage map's shortest unaudited list leaves COMPLEX.md's arbitrary-f complete-cover execution after the BIT, 2^{-4p}, row-field, and uniform-evaluator obligations were subsequently audited. This package takes that execution's row-bit reservation and the group order it cites, not another pass over those closed obligations.",
+  "bottleneck_link": "The common cover is the complex-side stock that feeds every recursive child in the #4100 layer. A pad that does not fit in the reserved row bits is a hole in that execution. The one-copy repair stays inside the same bit budget, so this obstruction does not by itself change the selected kappa 0.00302015.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the group-order identification, the ceil-pad failure, the one-copy repair, and the depth-halving check. Do not price parked tapes, enumerate O(73,2), or rerun the #4100 ledger.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md. verify.py binds the COMPLEX.md and AUDIT.md sentences, checks the written factor 2 for D=1..4, enumerates dot-product orders 1, 6 and 720 at dimensions 1, 3 and 5, and checks depth halving through width 100000. Gamma has 2628 bits and decimal SHA-256 50b58aaac98e621e9917d6c3bced5e276398b68918bbd57ac8d784d3d58db00b.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance with the proof and the verifier.",
+  "open_questions": [
+    {
+      "question": "With the fitting stock equal to one copy of N, do depth-first parked ancestor volumes still form a geometric series bounded by a constant times V/(W Gamma)?",
+      "why_it_matters": "COMPLEX.md charges parking inside O(V e^{1-a2} polylog(p)). The row-bit repair does not estimate those volumes.",
+      "first_step": "Express the parked volume at depth k from the product split into W families, one Gamma cover field, and the remaining divisible stock.",
+      "blocked_by": "This package does not replay the four PR4088 provider words or the fixed-tape schedule."
+    },
+    {
+      "question": "Is there a fixed-control encoder for one symplectic basis of the 72-dimensional perpendicular space, short of listing O(73,2)?",
+      "why_it_matters": "Gamma is only a cardinality. The complete-cover execution still cites an enumeration or an encoded counter of that group.",
+      "first_step": "Write an encoder that sends one ordered hyperbolic basis of 1^perp to the fixed control fields COMPLEX.md allows, and check it on the n=5 model.",
+      "blocked_by": "Gamma has 2628 bits, so a listing is not a feasible check. This package stops at the order."
+    }
+  ]
+}

research/complex-cover-row-reservation/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/AUDIT.md",
+    "research/unconditional-batched-crt/COMPLEX.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Sentence binding in COMPLEX.md and AUDIT.md; Gamma order and decimal hash; dot-product and perpendicular counts at n=1,3,5; written ceil pad fails for D=1..4; power-of-two control fits; floor repair keeps one copy; depth decreases and two levels halve."
+    }
+  ]
+}