Separate the tensor-frame child from factorwise repetition.

research/tensor-frame-child-interface/PROOF.md

@@ -0,0 +1,122 @@
+# Two readings of the tensor-frame child
+
+## Proposition
+
+Let the pinned mixed profile from
+`research/staged544-mixed-fourth-entry/RESULT.json` be
+
+```
+n = {1: 8060060, 2: 2310120, 3: 751813, 4: 327210, 5: 66425, 8: 25920, 48: 138492}
+```
+
+and let `W = 896 * 360`, `m = 73`, and
+
+```
+k = 43274477891769811819 / 25000000000000000000000
+```
+
+be that file's `root_lower`. Write
+
+```
+M(f, a) = sum_r a(r) * r^(1-k) - W * (m*f)^(1-k).
+```
+
+For a positive integer `f`, the two readings of one rank-`r` transition inside
+a core of width `73f` are
+
+- **single child:** `a(r*f) = n_r` and `a` is zero elsewhere below the parent;
+- **factorwise copies:** `a(r) = f * n_r` and `a` is zero on every rank that is
+  not one of the original ranks.
+
+At this fixed `k`:
+
+1. The scalar bill `M(1, n)` is strictly negative.
+2. The single-child bill `M(f, a)` is strictly negative for every integer `f >= 1`.
+3. The factorwise bill is strictly positive for every integer `f >= 2`.
+4. Both pinned recipe reports, `RECORD-base.json` and `RECORD-extra.json`,
+   list local child ranks inside `{1,2,3,4,5,8}` and do not name a tensor frame.
+
+No new κ follows. The selected frontier stays the conditional value in
+`certificates/selected-result.json`.
+
+## Why these two readings
+
+`research/unconditional-batched-crt/COMPLEX.md` says that every rank-`r`
+native transition executes one proper `C tensor (r f)` child, and that
+replacing a frame label `T` by `T tensor f` is supplied by the native directed
+recipe identities. The same paragraph says those corrections add no unpriced
+child. PR #4184 certifies the free-word cancellation on the four actual
+programs and states that the native frame and rank-child coordinate is still
+unpriced.
+
+The #4088 moment compares `sum n_r r^(1-k)` with `W * 73^(1-k)`. Substituting
+one child of rank `r*f` and parent width `73f` multiplies every term by
+`f^(1-k)`, so the sign is unchanged. Repeating the scalar child once per
+tensor factor multiplies only the child side by `f` and the parent side by
+`f^(1-k)`. Those are different bills. The recipe files on the same base are
+the scalar records: 72 warps, a local histogram on ranks at most 8, and no
+tensor-frame field.
+
+## Proof
+
+All logarithms and exponentials below are enclosed by alternating series with
+explicit tails. `ln 2 = 2 artanh(1/3)`. For a positive integer `n = m * 2^e`
+with `1 <= m < 2`, `ln n = ln m + e ln 2`, and `ln m = 2 artanh((m-1)/(m+1))`
+when `m > 1`. The artanh tail after `N` terms is at most the next geometric
+majorant `z^(2N+1) / ((2N+1)(1-z^2))`. Then
+
+```
+r^(1-k) = r * exp(-k ln r).
+```
+
+For `0 <= x < 1`, the Taylor remainder of `exp(-x)` after term `N` is smaller
+than the next term and has its sign. The verifier uses `N = 80` for artanh and
+`N = 30` for the exponential. Every rank that occurs satisfies `k ln r < 1`.
+
+Let `P = sum_r n_r r^(1-k)` and `Q = W * 73^(1-k)`, so the scalar moment is
+`M = P - Q`. The enclosures give
+
+```
+-3.85 * 10^-14 < M < -3.84 * 10^-14 < 0,
+Q > 2.337 * 10^7.
+```
+
+The displayed decimals in the receipt are truncated toward zero. The
+pass/fail comparisons use the exact rational enclosures.
+
+**Single child.** For `a(r*f) = n_r`,
+
+```
+M(f, a) = f^(1-k) * M.
+```
+
+Since `f^(1-k) > 0` and `M < 0`, the product is negative. The verifier also
+encloses the multiplied histogram directly at `f in {1,2,3,4,8,73}` and checks
+that each upper bound is negative.
+
+**Factorwise copies.** The bill is
+
+```
+h(f) = f*P - Q*f^(1-k) = f*M + Q*(f - f^(1-k)).
+```
+
+Its derivative is `h'(f) = P - (1-k) Q f^(-k)`. At `f = 2` the enclosed
+lower bound of `h'(2)` is greater than `68435`, so `h'(2) > 0`. For `f > 2`,
+`f^(-k) < 2^(-k)`, and `(1-k)Q > 0`, hence `h'(f) > h'(2) > 0`. Therefore `h`
+is increasing on `[2, infinity)`, and `h(f) > h(2)`. The direct enclosure
+gives `h(2) > 56052 > 0`. Every integer `f >= 2` is therefore positive.
+The samples `f in {3,4,8,73}` are checked directly as well.
+
+**Controls.** At `f = 1` both readings reproduce the scalar sign. Adding
+`10^9` rank-1 children makes the scalar upper bound positive, so the sign
+test is not vacuous. The pinned `lower_moment_interval` upper bound in
+`RESULT.json` is negative; that is a file pin, not an input to the series.
+
+## What this does not prove
+
+The single-child sign does not exhibit a native program that emits a child of
+rank `r*f`, and it does not price the left and right monomials. A monomial
+that adds another paid child, or that changes `W`, can destroy the negative
+sign. Factorwise failure does not forbid some third schedule whose child
+ranks are neither `r` nor `r*f`. The argument uses one rational endpoint of
+one finite histogram. It is not an all-size theorem and it does not move κ.

research/tensor-frame-child-interface/README.md

@@ -0,0 +1,67 @@
+# Tensor-frame child: factorwise repetition fails the pinned moment
+
+**Scoped separation; no new κ.** At the #4088 mixed profile and its pinned
+lower root endpoint, one child of rank `r*f` inside width `73f` keeps the
+scalar moment negative, and `f` copies of each scalar child make that moment
+positive for every integer `f >= 2`. The pinned native recipe records are
+still the scalar histograms. This does not accept #4100 and does not change
+the selected frontier.
+
+## Scope and evidence
+
+Card `uniform-transfer-audit`, scope **refined** to the frame/child coordinate
+left open by the free-word audit #4184. The caller is the #4088 histogram in
+`research/staged544-mixed-fourth-entry/RESULT.json`, not a new profile.
+[PROOF.md](PROOF.md) gives the two bills and the series tails. `verify.py`
+recomputes the enclosures with the standard library and checks both recipe
+reports. The receipt status is `PASS_TENSOR_FRAME_CHILD_GAP`.
+
+Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json).
+The selected record and catalogue are historical provenance. The three
+`--source` files are live inputs and must match their pins.
+
+The scalar moment at the pinned endpoint is about `-3.843e-14`. The factorwise
+bill at `f = 2` is greater than `56052`, and its derivative in `f` is greater
+than `68435`, so every larger integer `f` is worse. The single-child bill is
+`f^(1-k)` times the scalar moment.
+
+## Reproduce
+
+From the repository root, with Python 3.12:
+
+```sh
+python3 scripts/research_package.py --package research/tensor-frame-child-interface --check-only
+python3.12 scripts/research_package.py --package research/tensor-frame-child-interface
+```
+
+The verifier does not import the predecessor moment engine, the native runner,
+or the #4184 checkers. A direct run is:
+
+```sh
+python3 -B research/tensor-frame-child-interface/verify.py
+```
+
+## Open next questions
+
+**Question:** What tape-action and child count do the left and right monomials
+of one actual #4088 warp add when the frame is replaced by its `f`-fold tensor?
+
+It matters because the rank-`(r*f)` child keeps the scalar sign, while
+COMPLEX.md also inserts two monomials on that transition. An extra paid child,
+or a change in the role count `W = 896*360`, can erase the negative sign.
+First step: take warp 0 of `recipe/RECORD-base.json`, write those monomials as
+explicit `F2` row additions, and charge the compact primitive once per column
+for one fixed `f >= 2`. Blocker: this package does not lower a warp to tape
+actions, and the scalar recipe record has no monomial invoice.
+
+## Credit
+
+The mixed profile, the endpoint `k`, and the moment shape are Cinna Davis's
+#4088 package, with the earlier rational-enclosure lineage named there.
+COMPLEX.md's `C tensor (r f)` sentence is Cinna Davis's #4100. ToikY's #4184
+certifies the free-word cancellation and leaves this coordinate open; this
+package does not repeat that algebra. The recipe records are the #4088
+sources.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human or formal-kernel review is claimed.

research/tensor-frame-child-interface/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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/staged544-mixed-fourth-entry/RESULT.json",
+      "usage": "input",
+      "git_blob": "1174e25e2ef8f8bc9a0815c43ba5d64c8af08349",
+      "sha256": "6346ee768637aa9a1891d1d61d800d640235420b320fb7e659d1bf664ec42b3d"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/recipe/RECORD-base.json",
+      "usage": "input",
+      "git_blob": "d1c13c2ea786f790e96d45f18f58ec1ef2be7507",
+      "sha256": "221b56acc02ceeee35000f26f7098426421c0c90a075d81f9629170284f4aa25"
+    },
+    {
+      "path": "research/staged544-mixed-fourth-entry/recipe/RECORD-extra.json",
+      "usage": "input",
+      "git_blob": "8d5a8d22ddb5450abf414f9ec814077d16033111",
+      "sha256": "b1963fba45032238f773f3b375412d7db5f6e184edb59dcd05be15f6f70116f2"
+    }
+  ]
+}

research/tensor-frame-child-interface/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": "At the pinned #4088 mixed profile and its lower root endpoint, compare two readings of COMPLEX.md's rank-r native transition inside width 73f: one child of rank r*f, versus f copies of the scalar rank-r child. The pinned recipe records stay scalar.",
+  "scope_change_reason": "The uniform-transfer card asks for one quantified #4100 implication at its actual caller. #4184 already audited the free-word cancellation. This package takes that audit's stated next obligation, the frame/child coordinate, and prices only the child-rank alternative on the #4088 histogram. It does not replay native code or accept the all-size proof.",
+  "bottleneck_link": "The proposed all-size core is C tensor 73f. Repeating the scalar children factorwise makes the #4088 moment positive for every integer f>=2, so that reading cannot carry the conditional root. The single rank-(r*f) child keeps the scalar sign and is the coordinate the pinned recipes do not record.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the sign separation for the two child readings at the pinned endpoint. Do not search for a new profile, rerun native admission, or price monomial tape actions.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py; receipt status PASS_TENSOR_FRAME_CHILD_GAP.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance. No independent human or formal-kernel review.",
+  "open_questions": [
+    {
+      "question": "What tape-action and child count do the left and right monomials of one actual #4088 warp add when the frame is replaced by its f-fold tensor?",
+      "why_it_matters": "The rank-(r*f) child keeps the scalar moment sign, but COMPLEX.md also inserts two monomials per transition. An extra child, or a role-count change, can erase that sign.",
+      "first_step": "Take warp 0 of recipe/RECORD-base.json, write the two monomials as explicit F2 row additions, and charge PR2250's compact primitive once per column of one fixed f>=2.",
+      "blocked_by": "This package does not lower a warp to tape actions. The scalar recipe record has no monomial invoice."
+    }
+  ]
+}

research/tensor-frame-child-interface/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/staged544-mixed-fourth-entry/RESULT.json",
+    "research/staged544-mixed-fourth-entry/recipe/RECORD-base.json",
+    "research/staged544-mixed-fourth-entry/recipe/RECORD-extra.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact rational enclosures: scalar moment negative, single rank-(r*f) child negative, factorwise bill positive for every integer f>=2, recipe reports scalar, and one billion extra rank-1 children rejected."
+    }
+  ]
+}