Certify the SOURCE87 parent fibre count on the R437 carrier.

research/r437-source87-fibre-multiplicity/PROOF.md

@@ -0,0 +1,123 @@
+# SOURCE87 parent fibres
+
+The selected conditional exponent stays `60403/20000000`. This note does not
+admit the R437 carrier and does not change that exponent.
+
+## Pinned call
+
+`research/r437-carrier-integration/physical.py` evaluates
+`Layout.child_extents` on the SOURCE87 good plan with
+
+```text
+columns = 1, parent_size = 64, q = 3,
+before = 2, gap = 3, suffix = 2,
+first = 0, second = 126, width = 2.
+```
+
+The same file requires the returned triple to be `(2, 3 * 3^124, 2)` and
+requires `B * G * S * 3^4 = 12 * 3^128`. The executed child is the 972-bit
+fibre `2 * 3 * 2 * 3^4`. The unused-row count on that handoff is the literal
+`9475`, and the displayed parent volume is `9475 * 12 * 3^128`. Both arms use
+these arguments. The plan is good of rank 2.
+
+`layout.py` multiplies the external gap into exactly one of the three
+spectator regions: the prefix when the first chunk starts at or after
+`parent_size`, the suffix when the second chunk ends at or before
+`parent_size`, and the middle otherwise. `plan.py` sets the plan dimension
+`m` to the low-projector length and requires `1 <= rank < m <= 64`. A good
+plan stores that length as its dimension. `Layout` sets
+
+```text
+core = columns * m, remaining = parent_size - core,
+extra = 2 * remaining, total = 2 * parent_size.
+```
+
+A position below `core` stays put. A position at or above `core` moves by
+`extra`. At ring precision `w`, each address step scales a count by `q^w`.
+The published triple uses powers of `3`, so the fixture atom size is `3`.
+That is `w = 1`. The same triple is not the `w = 2` value.
+
+## Dimension 64
+
+Assume `w = 1` and the call above. For `m = 64`, `core = 64`, `extra = 0`
+and `total = 128`, so the physical map is the identity. The chunks are the
+address intervals `[0, 2)` and `[126, 128)`. They are ordered, disjoint,
+inside the body, contiguous, and on opposite sides of the external gap at
+`64`. The prefix exponent is `0`, the middle exponent is `124`, and the
+suffix exponent is `0`. The gap falls in the middle, once. Therefore
+
+```text
+B = 2, G = 3 * 3^124 = 3^125, S = 2.
+```
+
+The product test in the caller becomes
+
+```text
+2 * 3^125 * 2 * 3^4 = 12 * 3^128.
+```
+
+For every `m` with `1 <= m <= 63`, the same call either violates chunk
+placement or returns a different triple. In particular `m = 63` pushes the
+second chunk to address `128` and past `total = 128`. Thus, among the
+dimensions `plan.py` allows, the published assertion holds exactly at
+`m = 64`. The rank-2 constraint `2 < m` is compatible with that value.
+
+## Fibre count
+
+The executed fibre has volume
+
+```text
+972 = 2 * 3 * 2 * 3^4.
+```
+
+The parent volume displayed by the caller is `9475 * 12 * 3^128`. Hence the
+parent packet is exactly
+
+```text
+M = 9475 * 3^124
+```
+
+copies of that fibre:
+
+```text
+M * 972 = 9475 * 12 * 3^128.
+```
+
+The factor `3^124` is `G / gap`. The factor `9475` is the pinned unused-row
+literal. It is also `269241600 / 28416`, the integer appearing in the
+carrier's stock formula, but this note does not re-execute stock admission.
+A schedule that performs one common per-fibre action vector `v` on every
+copy, and nothing else, pays `M v` on this entry.
+
+## C and D
+
+The compiler receipt gives both arms two SOURCE87 records. Each record has
+rank `2` and the same chart digest. The four request identifiers differ, so
+these are not the same request objects. The extent arguments in `physical.py`
+do not depend on the arm. The leaf-scan bill of this entry is therefore the
+same number `M v` on C and on D, and its difference is zero.
+
+The same receipt's request profile changes by
+
+```text
+rank 1: +288, rank 2: -576, rank 3: +288,
+```
+
+and by zero at every other recorded rank. The rank-mass change is
+
+```text
+1*288 + 2*(-576) + 3*288 = 0,
+```
+
+and both arms have rank mass `1808352`. Net request count is also unchanged.
+The rank-2 count moves by `-576`, far more than the two SOURCE87 records, so
+other requests still differ. Equality of this entry is not equality of the
+sum over the profile.
+
+## What this does not price
+
+Inter-fibre gather, routing, parking, blank-return, source-table
+construction, and the leaf scan of every request outside this entry remain
+unpriced. The zero difference removes one term from the integration's
+whole-construction comparison. It does not show that the comparison holds,
+and it does not produce a new selected exponent.

research/r437-source87-fibre-multiplicity/README.md

@@ -0,0 +1,84 @@
+# SOURCE87 fibre multiplicity
+
+**Partial certificate. No new κ.** The selected conditional result stays
+`60403/20000000` (`0.00302015`, #4470).
+
+## Result
+
+On the pinned SOURCE87 rank-2 entry of the R437 carrier integration, the
+parent packet is exactly
+
+```text
+M = 9475 * 3^124
+```
+
+copies of the executed 972-bit fibre. Both arms C and D have this same `M`.
+A leaf scan that charges one common per-fibre vector on every copy therefore
+has C-minus-D difference zero on this entry.
+
+The published extent triple `(2, 3 * 3^124, 2)` holds for the call
+`(first, second, width) = (0, 126, 2)` at parent size 64 and atom size 3
+exactly when the plan dimension is 64, and at no smaller positive dimension
+through 64. The proof is [PROOF.md](PROOF.md). The checker recomputes the
+integer map, rejects the neighbouring dimensions and a doubled gap, and reads
+the compiler receipt.
+
+## What stays open
+
+The integration's whole-construction inequality is not settled. Gather,
+routing, parking, and blank-return between the `M` fibres are not priced.
+The compiler profile still changes by `{1: +288, 2: -576, 3: +288}`. Those
+other requests are outside this entry. The reverse-row coefficient is not
+rederived. No supplier and no new exponent is claimed.
+
+## Task and overlap
+
+- Task: `r437-carrier-integration`, scope **refined**.
+- Base: canonical main `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority revision 7.
+- Ordered eligible list, the priority table in `docs/research/current-priorities.md`, then catalogue tasks that are not already in that table. A row stays while its stated next decision is still open:
+  1. `uniform-transfer-audit` — #4100 still has caller-bound implications.
+  2. `supplier-boundary-audit` — the full mixed engine has not been rerun.
+  3. `joint-query-controller` — the matched whole-caller comparison remains stated.
+  4. **This package.** `r437-carrier-integration`.
+  5. `p104-side-correction`.
+  6. `independent-moment`.
+  7. `formal-interface-lemma`.
+  8. `bit-helper-contract`.
+  9. `bit-new-register-model`.
+  10. `complex-rank-shape-decoder`.
+- #4067 is the paid exchange. #4147 is the reverse coefficient, reused and not recomputed. #4176 (`research/r437-carrier-integration`) regenerates the compiler and checks the extent triple on one execution. This package classifies the dimension, names `M`, and separates this entry's zero leaf-scan difference from the nonzero profile delta.
+- #4160 prices a different constructor tape and is not this geometry.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B scripts/research_package.py --package research/r437-source87-fibre-multiplicity --check-only
+python3 -B scripts/research_package.py --package research/r437-source87-fibre-multiplicity
+```
+
+`verify.py` prints `PASS_R437_SOURCE87_FIBRE_MULTIPLICITY`. Not run: the
+integration's `physical.py` replay, Lean, Docker, and the selected cold replay.
+The universal statement on dimensions `1..64` is the finite check in
+`verify.py` together with the closed form in `PROOF.md`.
+
+## Open next questions
+
+1. Price the fixed-tape gather, routing, parking, and blank-return that
+   separate these `M` fibres. That bill is what the integration still names
+   as blocking a global paid improvement. Start with one spectator step on
+   the pinned layout. Blocked here because no tape machine for the `3^124`
+   gap is executed.
+2. Apply the same extent map to one request in the profile delta. SOURCE87
+   does not account for the `288` extra rank-1 requests or the `576` missing
+   rank-2 requests. Blocked because the compiler receipt does not list those
+   plan coordinates.
+
+## Credit
+
+Chris R / Clear1nsight, PR #4067 and PR #4176, for the carrier, the compiler
+receipt, and the extent assertion. The reverse coefficient remains
+unpaidmoon's PR #4147. The layout and plan sources are the retained
+selected-bit caller. Prepared by unpaidmoon with substantial Cursor Grok
+assistance. Apache-2.0. No independent human or formal-kernel review is claimed.

research/r437-source87-fibre-multiplicity/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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/r437-carrier-integration/COMPILER-RESULT.json",
+      "usage": "input",
+      "git_blob": "1a1c1ab9e7732df3a65964e089ed15e59f47f5d2",
+      "sha256": "753874f3e1563dadb606ecdb3997f61a20af8a15e69d50b1b11de8877f6f4f08"
+    },
+    {
+      "path": "research/r437-carrier-integration/physical.py",
+      "usage": "input",
+      "git_blob": "e314799b5c6deeb45a790534539d846a27d2d60c",
+      "sha256": "d41ea48bc8fd6e449ef17f122dfbea05adf06e7ab448063e4afd06add1152cf0"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/inputs/pr2753/layout.py",
+      "usage": "input",
+      "git_blob": "aa554b14fe0f6b308d9fba0a2afc92e5a28e20cb",
+      "sha256": "3beef6534b02c3b011b741f957a7d9fb05a9ac0bba1fed53b2c71834e4ea6bc1"
+    },
+    {
+      "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/plan.py",
+      "usage": "input",
+      "git_blob": "48255d5454308c07635fae4e7eb4873b0bd2a4f8",
+      "sha256": "d9c8dc93762db4d3a449814aa51e2211460648694469854d89cb48cb04188cf3"
+    }
+  ]
+}

research/r437-source87-fibre-multiplicity/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "r437-carrier-integration",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "r437-carrier-integration",
+    "question": "Can the paid R437 two-window carrier improvement be admitted by the actual pooled compiler and physical caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/r437-two-window-carrier/README.md",
+      "research/r437-reverse-row-coefficient/README.md"
+    ],
+    "methods": [
+      "Close one compiler/request, caller or precision/stock implication for the pinned paid exchange.",
+      "Falsify that exact interface with an arbitrary-dirty-state or chronology counterexample."
+    ],
+    "acceptance_gate": "Pin the complete source and destination contracts, exact paid and scalar deltas, and all remaining assumptions. A local moment gain is not a physical or all-size supplier admission.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #4067 paid profile and open integration obligations; #4147 covers the reverse row coefficient. Three additional ADDs per call and all helpers remain charged. This is not a selected supplier.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Choose one unclaimed obligation: pooled compiler codebook/request alignment, actual physical caller, or precision/stock envelope using the already reported reverse coefficient. Pin the input and receiver, preserve dirty/source windows, and test one binding with a rejection control. Stop at unresolved dependencies; do not rederive the coefficient or quote the local moment as a completed bound.",
+    "bottleneck_link": "The exchange changes the paid profile; integration must establish that its gain survives the complete caller.",
+    "allowed_variations": [
+      "One compiler rebind, one actual caller boundary, or one precision/stock implication."
+    ],
+    "scope_change_triggers": [
+      "Ignoring added ADDs, retaining an obsolete reverse coefficient, or declaring global admission from the local histogram."
+    ],
+    "overlap_terms": [
+      "R437",
+      "two-window carrier",
+      "4067",
+      "4147",
+      "pooled compiler",
+      "request alignment",
+      "reverse row coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4067: source-bound two-window carrier with (2,2) to (1,3) paid exchange and fixed OQ4 host.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Pooled compiler/request rebind, physical caller and precision/stock admission.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4147: reverse row coefficient follow-up.",
+        "evidence": "research/r437-reverse-row-coefficient/README.md",
+        "remaining": "Use the exact coefficient in a caller-bound precision/stock proof rather than repeat the arithmetic.",
+        "status": "author-checked",
+        "source_commit": "72e7bb797adf82aeb525a399f56ab8adbab8e93c",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "At the pinned SOURCE87 rank-2 entry, certify the full-parent fibre count and show that this leaf-scan term is the same for arms C and D.",
+  "scope_change_reason": "The card asks for one unclaimed compiler, caller, or precision/stock obligation of the paid exchange. PR #4176 already regenerates the pooled compiler and connects the reverse coefficient to the 192/512 envelope. This package takes the first still-open integration question: the checked SOURCE87 entry at full parent spectator multiplicity. It does not rederive the reverse coefficient or rerun the compiler.",
+  "bottleneck_link": "The paid profile improvement can raise the bit supplier only if its gain survives the complete caller. Zeroing the SOURCE87 leaf-scan difference removes one unknown from that comparison. It does not admit the carrier: gather, parking, blank-return, and the other requests in the profile delta stay unpriced, and the selected result is still complex-bound.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the SOURCE87 fibre identity, the dimension classification, and the C-versus-D comparison for that entry. Do not price inter-fibre gather or search another carrier.",
+  "outcome": "partial",
+  "evidence": "PROOF.md plus verify.py. The integer model matches the published extent triple only at plan dimension 64, gives M = 9475 * 3^124 fibres, and reads the pinned compiler receipt for the shared chart and the nonzero profile delta.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "What is the fixed-tape gather, routing, parking, and blank-return bill that separates these M fibres?",
+      "why_it_matters": "The leaf-scan difference on SOURCE87 is zero. The integration's open question still names the separation bill as what prevents a global paid improvement.",
+      "first_step": "Price one spectator step of the pinned layout on the actual fixed-tape primitives, using the same source entry.",
+      "blocked_by": "This package does not execute a tape machine for the 3^124 gap."
+    },
+    {
+      "question": "What is the leaf-scan difference of the requests in the profile delta {1:+288, 2:-576, 3:+288}?",
+      "why_it_matters": "Those are the only request-count changes between C and D. SOURCE87 staying rank 2 does not make the sum over all requests equal.",
+      "first_step": "Read the plan coordinates of one changed rank-1 request and apply the same extent map.",
+      "blocked_by": "COMPILER-RESULT.json records SOURCE87 and the aggregate profile, not those other plan coordinates."
+    }
+  ]
+}

research/r437-source87-fibre-multiplicity/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/r437-carrier-integration/COMPILER-RESULT.json",
+    "research/r437-carrier-integration/physical.py",
+    "research/selected-bit-physical-caller/inputs/pr2753/layout.py",
+    "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/plan.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Extent identity at dimension 64, uniqueness on dimensions 1..64, fibre count M, shared SOURCE87 chart, profile delta, and rejection controls."
+    }
+  ]
+}