Independent verification: derive PR540's pending ranges [15,22) and [1,29) from PR442's schedule (no new kappa)

research/pr540-pending-range-derivation/README.md

@@ -0,0 +1,93 @@
+# Deriving PR540's pending ranges from PR442's schedule
+
+**Independent source-binding check for an open Lean PR. No new κ; the selected record is unchanged.**
+
+[PR540](https://github.com/CrocSwap/integer-mult-bounds/pull/540) (cheesegrader, head
+`acc1917034d10f464271ab115fda314fd4eee7a3`) formalizes one literal PR442 bit invocation (stage 2,
+replica 0, pair 0, forward). Its `PhysicalSourceConnection.pendingTag` supplies the pending
+coordinates by hand: child 1 owns axes `[15,22)` and child 2 owns `[1,29)`. Its README states that
+"Neither Lean nor the source-extraction check binds these ranges to the source schedule." Lean's
+`tag_pending_contains` only shows that the ranges *contain* the hosted target masks. The extractor
+`generate_ownership_data.py` hard-codes the bases 15 and 1. The
+[handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166) lists this as a next task.
+
+## Result
+
+`verify.py` derives both ranges from PR442's hosted bit template and PR434's geometry. It is
+standard-library code that imports nothing from PR434, PR442 or PR540. **Both ranges are exactly the
+derived pending sets.**
+
+| Child (template `idx`) | Pair | Level advance | Window stages | Derived pending axes | PR540 range | Hosted width used by the stage-2 call |
+|---|---:|---|---|---|---|---:|
+| 1 | 1 | 1 → 2 | {2} | `[15,22)` = exterior block E₂ | `[15,22)` | 7 of 7 |
+| 2 | 2 | −1 → 3 | {0,1,2,3} | `[1,29)` = q⊥ ⊕ E₁ ⊕ E₂ ⊕ E₃ | `[1,29)` | 28 of 28 |
+
+The derivation has five steps.
+
+1. **Binding.** The hosted template's uncompressed SHA256 equals `bit_template_sha256` in PR442's
+   [`EXPECTED.json`](../idle-axis-hosting/EXPECTED.json) on main. The geometry's hash equals the
+   template's `geometry_sha256`. The two vendored inputs in `inputs/` are byte-identical to PR540's
+   `research/lean-multi-host-source/inputs/` files with the same names.
+2. **Coordinates.** All 120 ports' stage-s routes give one common exterior block layout:
+   E_s = `[8+7(s−1), 8+7s)`. The blocks partition axes 8..63. For every port, `[q/2 | A_q]` is
+   checked to be an exactly orthogonal 8×8 matrix. This is the `B_port ⊕ I₅₆` chart in which axis 0
+   is span(q) and axes 1..7 are q⊥.
+3. **Levels.** The level model follows PR386's geometry (ρ_(s,q) sends (P_q, E_s) to (I₈, E_(s−1))):
+   L₋₁ = span(q) = {0} and L_ℓ = Q⁸ ⊕ E₁ ⊕ … ⊕ E_ℓ = `[0, 8+7ℓ)` in chart axes. The rank of every
+   idle event in the schedule (all 10, including the rank-0 terminal child) equals dim L_b − dim L_a.
+4. **Windows.** The windows are recomputed from the schedule with the PR442 rule: local invocations
+   strictly after the last local or bridge touch of the pair. Stage 2 lies in both windows, and the
+   host pairs differ from the active pair 0.
+5. **Routes.** Each of the 747 hosted routes `(child, off, w)` of the selected call maps to
+   `pending[off:off+w]`. This equals PR540's `base+off .. base+off+w` for every route. Each
+   PR540 range equals the full derived pending set, not just a superset of its targets.
+
+Six mutations are rejected:
+
+- child 1 placed on the previous level's block `[8,15)`;
+- child 2 shifted to include the q axis;
+- the two children's ranges swapped;
+- L₋₁ = {} (rank mismatch);
+- a route offset moved past the pending rank;
+- stage 2 removed from child 1's window.
+
+## Limits
+
+- This is a Python derivation, not a kernel proof. It closes the stated gap as **external evidence**.
+  Moving the derivation into Lean remains open.
+- The idle ranks fix only the *dimensions* of the level spaces. Identifying L₋₁ with span(q), rather
+  than another line, uses PR386's route identity, which this package does not re-prove. A wrong
+  choice of line would break the q⊥ chart; that chart is checked.
+- Within one child, PR442 requires only disjoint width-w subsets of its pending set. The ascending
+  axis order that maps `off` to axes is the shared convention of PR540's extractor and this check;
+  the source does not fix it.
+- Only the selected invocation is checked. This says nothing about other calls, the cover sweep,
+  costs or κ.
+
+## Reproduce
+
+```sh
+python3 -I -B research/pr540-pending-range-derivation/verify.py   # ~0.5 s, prints PASS_…
+python3 scripts/research_package.py --package research/pr540-pending-range-derivation
+```
+
+`verify.py --write` regenerates `RESULT.json`. Without that flag, the script requires the existing file to
+match byte for byte.
+
+## Open next questions
+
+- **Can `pendingTag` be defined from the schedule inside Lean?** This would turn the hand-supplied
+  ranges into a theorem. A first step is to encode the 10 idle events and the level map
+  `L_ℓ = [0, 8+7ℓ)`, then prove `pendingTag t = L_b \ L_a` by `decide`. The blocker is that the
+  level model must be stated as a definition and linked to the route identities in Lean.
+- **Does the same derivation hold for a second selected call?** That would test whether the
+  convention generalises before PR540 is extended. A first step is to run `derive` with another
+  `SELECTED` (for example, stage 3 on pair 1, whose children have different windows). This is not
+  blocked, but it is outside this session.
+
+## Credit
+
+The construction and hosting rule are PR434/PR442 (`research/e8-early-reset-kernel`,
+`research/idle-axis-hosting`). The bit geometry is PR386. The Lean formalization and the
+identification of this gap are cheesegrader's PR540. Prepared by Douglas Colkitt with substantial
+Claude (Anthropic) assistance. Apache-2.0.

research/pr540-pending-range-derivation/RESULT.json

@@ -0,0 +1,100 @@
+{
+ "controls": {
+  "child1_previous_level_block": "rejected: route ['hosted', 1, 0, 7]: derived [15, 16, 17, 18, 19, 20, 21] != Lean [8, 9, 10, 11, 12, 13, 14]",
+  "child2_includes_q_axis": "rejected: route ['hosted', 2, 16, 8]: derived [17, 18, 19, 20, 21, 22, 23, 24] != Lean [16, 17, 18, 19, 20, 21, 22, 23]",
+  "children_swapped": "rejected: route ['hosted', 2, 16, 8]: derived [17, 18, 19, 20, 21, 22, 23, 24] != Lean [31, 32, 33, 34, 35, 36, 37, 38]",
+  "level_minus_one_empty": "rejected: idle 0 rank 14 != dim difference",
+  "route_offset_past_rank": "rejected: route ['hosted', 1, 1, 7] exceeds pending rank",
+  "stage2_outside_window": "rejected: stage 2 outside window of child 1"
+ },
+ "exterior_blocks": {
+  "1": [
+   8,
+   15
+  ],
+  "2": [
+   15,
+   22
+  ],
+  "3": [
+   22,
+   29
+  ],
+  "4": [
+   29,
+   36
+  ],
+  "5": [
+   36,
+   43
+  ],
+  "6": [
+   43,
+   50
+  ],
+  "7": [
+   50,
+   57
+  ],
+  "8": [
+   57,
+   64
+  ]
+ },
+ "hosted_children": {
+  "1": {
+   "derived_pending_axes": [
+    15,
+    22
+   ],
+   "hosted_axes_used": 7,
+   "lean_range": [
+    15,
+    22
+   ],
+   "levels": [
+    1,
+    2
+   ],
+   "pair": 1,
+   "pending_rank": 7,
+   "window_stages": [
+    2
+   ]
+  },
+  "2": {
+   "derived_pending_axes": [
+    1,
+    29
+   ],
+   "hosted_axes_used": 28,
+   "lean_range": [
+    1,
+    29
+   ],
+   "levels": [
+    -1,
+    3
+   ],
+   "pair": 2,
+   "pending_rank": 28,
+   "window_stages": [
+    0,
+    1,
+    2,
+    3
+   ]
+  }
+ },
+ "hosted_routes": 747,
+ "idle_ranks_checked": 10,
+ "ports_checked": 120,
+ "scope": "Python derivation from the source schedule and geometry. Not kernel checked. The level model L_-1=span(q), L_l=Q^8+E_1..E_l is PR386 geometry, checked here against every idle rank and route; the ascending order of pending axes within a child is the shared offset convention.",
+ "selected_call": {
+  "orientation": "forward",
+  "pair": 0,
+  "replica": 0,
+  "stage": 2
+ },
+ "status": "PASS_PR540_PENDING_RANGES_DERIVED_FROM_PR442_SCHEDULE"
+}

research/pr540-pending-range-derivation/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    },
+    {
+      "path": "research/idle-axis-hosting/EXPECTED.json",
+      "usage": "input",
+      "git_blob": "1b0811df29bc2eabdabb51219e9b2382da9a48f6",
+      "sha256": "ed83c1bf1ca2d01eaab5149a34520806a07ef375dfa9e3ed69d123f4be4c9960"
+    }
+  ]
+}

research/pr540-pending-range-derivation/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 2,
+  "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Audit one theorem-to-source binding of open PR540: derive its hand-supplied pendingTag ranges [15,22) and [1,29) from PR442's bit schedule and PR434 geometry, instead of formalizing a new lemma.",
+  "scope_change_reason": "The card allows narrowing to one theorem-to-certificate binding. PR540's README and the handoff thread name this exact unbound premise.",
+  "bottleneck_link": "Side result for the conditional gap, not kappa: it removes one hand-supplied premise from the only literal Lean invocation of the hosting interface by tying it to the source schedule as external evidence.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the single selected invocation; do not extend to other calls or attempt the Lean port in this session.",
+  "outcome": "completed",
+  "evidence": "RESULT.json: both PR540 ranges equal the derived pending sets for all 747 hosted routes; 6/6 mutations rejected",
+  "author": "Douglas Colkitt",
+  "ai_assistance": "Substantial: Claude (Anthropic, Claude Code) selected the task, wrote verify.py and drafted the README; the author reviewed the result.",
+  "open_questions": [
+    {
+      "question": "Can pendingTag be defined from the schedule inside Lean?",
+      "why_it_matters": "It turns a hand-supplied premise of PR540 into a kernel-checked theorem.",
+      "first_step": "Encode the 10 idle events and L_l=[0,8+7l); prove pendingTag t = L_b minus L_a by decide.",
+      "blocked_by": "The level model must be stated in Lean and linked to the route identities."
+    },
+    {
+      "question": "Does the derivation hold for a second selected call?",
+      "why_it_matters": "It tests whether the convention generalises before PR540 is extended.",
+      "first_step": "Run derive() with another SELECTED, e.g. stage 3 on pair 1.",
+      "blocked_by": "Nothing; out of this session's budget."
+    }
+  ]
+}

research/pr540-pending-range-derivation/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/idle-axis-hosting/EXPECTED.json",
+    "research/pr540-pending-range-derivation/inputs/geometry.json.gz",
+    "research/pr540-pending-range-derivation/inputs/hosted-template.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Pins and PR442/geometry binding; derived pending sets equal PR540 ranges for all 747 routes; RESULT.json byte match; six rejection controls"
+    }
+  ]
+}