Independently check #4610's warp substitution: 34 of 72 G maps changed, all invertible and frame-transporting; 17,453 scalar opcodes unchanged, 422 labels; 3,298 paid calls (no new κ)

research/pr4610-warp-substitution-check/.gitattributes

@@ -0,0 +1 @@
+PR4610-ACTUAL-WORD.json.gz -text

research/pr4610-warp-substitution-check/README.md

@@ -0,0 +1,46 @@
+# Independent check of #4610's warp-substitution claims on its emitted word
+
+**Task:** independent-moment (independent check). **Base:** canonical main `f626db5c`. **No κ is claimed.**
+
+## The claim
+
+intqwq's #4610 (head `4b4c75bc`, conditional κ 0.00302152) states that its emitted word:
+
+- substitutes 34 of PR4470's 72 warp generators with other invertible binary maps, each transporting its declared input frame onto its output frame;
+- relabels 422 scalar frames;
+- keeps all 17,453 scalar opcodes, with their order and coefficients;
+- pays 3,298 calls, 12 fewer than PR4470's 3,310.
+
+#4610 certifies these claims in Lean shards. This package checks them independently in Python, against PR4470's word from main's pinned constructor and #4610's vendored emitted word (blob `79dad65b`, SHA256-pinned).
+
+## Results
+
+- **Warp maps.** All 72 bound G maps are invertible on F₂⁹, giving 512 distinct images. Each maps span(from_frame) **onto** span(to_frame). Exactly **34** differ from PR4470's maps, and op, lender and B_pos agree for all 72.
+- **Scalars.** In both orientations, the **17,453 scalar opcodes and coefficients agree in order** with PR4470's, and exactly **422** scalar frame labels differ.
+- **Paid calls.** Climbs drop from 3,302 to 3,290. With the 8 centre jobs, that gives **3,298 vs 3,310** paid calls.
+- **Other events.** Adapters (448), warps (240), phases (10) and centres (8) keep their counts.
+
+Together with my #4614 (endpoint frames and profile) and #4615 (raw crossing), every structural and arithmetic statement checked so far in #4610 holds.
+
+## Verify
+
+```text
+python3 -B research/pr4610-warp-substitution-check/verify.py
+```
+
+The check takes about 2 s and uses the standard library only.
+
+## Limitations
+
+**Not covered:**
+
+- the Clifford absolute phases and the monomial lowering of the changed maps;
+- the 632-column symbolic endpoint identity;
+- the outer-ledger checks;
+- whether substituting generators of the free-group identity is admissible under the supplier contract.
+
+## Open next questions
+
+- **Absolute phases.** Check them for the 34 changed maps independently. First step: rebuild each K_G from its binary G via the transported-frame lemma's integer column formulas (`research/transported-warp-frames/PROOF.md`), and compare with #4610's bound operators.
+
+Credit: intqwq (#4610), Cinna Davis (#4470). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/pr4610-warp-substitution-check/SOURCES.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/fresh-helper-boundary/native.py",
+      "usage": "input",
+      "git_blob": "1b36f6cb5f205c33bf48811e0b1b3621c55e8154",
+      "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29"
+    },
+    {
+      "path": "research/fresh-helper-boundary/CHANGES.json",
+      "usage": "input",
+      "git_blob": "45744fedd0e28967aa72586048b8bc0c72f419a9",
+      "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624"
+    },
+    {
+      "path": "research/missing-join-frame/PATCH.json",
+      "usage": "input",
+      "git_blob": "f96d295d40014d4dd503f58eb3cdabcbb4b8e101",
+      "sha256": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e"
+    },
+    {
+      "path": "research/joint-helper-lattice/PATCH.json",
+      "usage": "input",
+      "git_blob": "51304a6601061ed4e698f910b09135ef109555e3",
+      "sha256": "296d0e8c58cc70febe042c681ef30d6bb469818c0835fbcaac8aa8d330f5b727"
+    },
+    {
+      "path": "research/joint-helper-lattice/native_joint.py",
+      "usage": "input",
+      "git_blob": "0315f80e2fdef5e0eef13e3e9b8f72066238164d",
+      "sha256": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46"
+    },
+    {
+      "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz",
+      "usage": "input",
+      "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784",
+      "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61"
+    },
+    {
+      "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz",
+      "usage": "input",
+      "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c",
+      "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39"
+    }
+  ]
+}

research/pr4610-warp-substitution-check/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "unchanged",
+  "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "scope_change_reason": null,
+  "bottleneck_link": "Independent Python coverage of #4610's warp-substitution and scalar-preservation claims.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at warp maps and program comparison.",
+  "outcome": "completed",
+  "evidence": "72 G maps invertible and frame-transporting; 34 changed; op/lender/B_pos unchanged; 17,453 scalar opcodes unchanged in order; 422 label changes; climbs 3,302 -> 3,290; paid 3,310 -> 3,298; other event counts unchanged.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Independent absolute-phase check for the 34 changed maps.",
+      "why_it_matters": "Remaining unverified physical step.",
+      "first_step": "Rebuild K_G via transported-frame integer formulas.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4610-warp-substitution-check/VERIFY.json

@@ -0,0 +1,28 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "docs/research/agent-task-catalog.json",
+    "research/fresh-helper-boundary/CHANGES.json",
+    "research/fresh-helper-boundary/native.py",
+    "research/joint-helper-lattice/PATCH.json",
+    "research/joint-helper-lattice/native_joint.py",
+    "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz",
+    "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz",
+    "research/missing-join-frame/PATCH.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Vendored word hash; 72 G maps invertible and transporting; 34 changed; scalar opcodes and 422 labels vs pinned PR4470 constructor; climbs and paid-call counts."
+    }
+  ]
+}

research/pr4610-warp-substitution-check/verify.py

@@ -0,0 +1,95 @@
+#!/usr/bin/env python3
+"""Independent check of PR #4610's warp-substitution claims on its emitted word (intqwq, head 4b4c75bc).
+
+#4610 states that its emitted word substitutes 34 of PR4470's 72 warp generators by other invertible binary maps,
+each transporting its declared input frame onto its output frame, relabels 422 scalar frames, keeps all 17,453
+scalar opcodes with their order and coefficients, and pays 3,298 calls (12 fewer than PR4470's 3,310).
+Against PR4470's word from main's pinned constructor (run isolated) and the vendored, sha256-pinned emitted word, this
+verifier checks in Python, independently of #4610's Lean shards and Python admission:
+  * all 72 bound G maps are invertible on F2^9 (512 distinct images) and map span(from_frame) onto span(to_frame);
+    exactly 34 differ from PR4470's maps; op, lender and B_pos agree for all 72;
+  * in both orientations the 17,453 scalar opcodes/coefficients agree in order with PR4470's and exactly 422 scalar
+    frame labels differ; climbs drop from 3,302 to 3,290, so with the 8 centre jobs the paid calls are 3,298 vs 3,310;
+    adapters (448), warps (240), phases (10) and centres (8) keep their counts.
+Not covered: Clifford absolute phases / monomial lowering, the symbolic endpoint identity, contract admissibility.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from collections import Counter
+import gzip
+import hashlib
+import json
+from pathlib import Path
+import subprocess
+import sys
+import tempfile
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+WORD = HERE / "PR4610-ACTUAL-WORD.json.gz"
+WORD_SHA256 = "d578875344095047c383ef513e69b9deb9d99d2b75abe14f7359d06365a924ac"
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def span(basis):
+    s = {0}
+    for v in basis:
+        s |= {x ^ v for x in s}
+    return frozenset(s)
+
+
+def apply(cols, x):
+    y = 0
+    for j in range(9):
+        if x >> j & 1:
+            y ^= cols[j]
+    return y
+
+
+def pr4470():
+    with tempfile.TemporaryDirectory(prefix="audit-cache-") as cache:
+        code = ("import json,sys;sys.path.insert(0,sys.argv[1]);import native_joint;"
+                "c,p,b,o,n=native_joint.construct();print(json.dumps({'c':c,'p':p}))")
+        run = subprocess.run([sys.executable, "-I", "-B", "-X", "pycache_prefix=" + cache, "-c", code,
+                              str(ROOT / "research/joint-helper-lattice")], capture_output=True, check=True, timeout=180)
+    out = json.loads(run.stdout)
+    return out["c"], out["p"]
+
+
+def main():
+    raw = WORD.read_bytes()
+    need(hashlib.sha256(raw).hexdigest() == WORD_SHA256, "vendored #4610 ACTUAL-WORD")
+    word = json.loads(gzip.decompress(raw))
+    a, (c, p) = word["canonical"], pr4470()
+    changed = 0
+    for w, w0 in zip(a["warps"], c["warps"]):
+        g = w["G_columns"]
+        need(len({apply(g, x) for x in range(512)}) == 512, "G invertible")
+        need({apply(g, x) for x in span(a["frames"][w["from_frame"]])} == span(a["frames"][w["to_frame"]]),
+             "G transports its input frame onto its output frame")
+        need(all(w[k] == w0[k] for k in ("op", "lender", "B_pos")), "op, lender, B_pos unchanged")
+        changed += g != w0["G_columns"]
+    need(len(a["warps"]) == 72 and changed == 34, "34 of 72 G maps changed")
+    summary = {}
+    for side in ("forward", "backward"):
+        new, old = word["programs"][side], p[side]
+        sn, so = [e for e in new if e[0] == "scalar"], [e for e in old if e[0] == "scalar"]
+        need(len(sn) == len(so) == 17453 and all(x[1] == y[1] for x, y in zip(sn, so)), "scalar opcodes unchanged")
+        labels = sum(x[2:] != y[2:] for x, y in zip(sn, so))
+        need(labels == 422, "422 scalar frame labels changed")
+        kn, ko = Counter(e[0] for e in new), Counter(e[0] for e in old)
+        need(ko["climb"] - kn["climb"] == 12 and kn["climb"] + kn["center"] == 3298 and ko["climb"] + ko["center"] == 3310,
+             "12 fewer climbs; 3,298 vs 3,310 paid calls")
+        need(all(kn[k] == ko[k] for k in ("adapter", "warp", "phase", "center")), "other event counts unchanged")
+        summary[side] = {"scalars": len(sn), "label_changes": labels, "climbs": [ko["climb"], kn["climb"]]}
+    print(json.dumps({"status": "PASS_PR4610_WARP_SUBSTITUTION_CHECK", "warps": 72, "changed_G": changed,
+                      "all_transport_and_invertible": True, "programs": summary, "paid_calls": [3310, 3298],
+                      "not_covered": ["absolute phases / monomial lowering", "symbolic endpoint identity",
+                                      "contract admissibility"], "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())