Navigation repair: route R439 H2/K work through the retained semantic-D evidence (no new kappa)

docs/research/bottleneck-brief.md

@@ -49,9 +49,14 @@ There are three central opportunities:
 | Supplier interface lemma | Admit a promising word excluded by today's contract | One exact replacement implication, including dirty inputs and its implementation cost |
 
 For example, [the helper-star package](../../research/r439-bsection-stars-seed01/README.md)
-reduces scalar additions but keeps its paid profile and carries an H2/K interface
-gap. A useful next question is whether one changed helper operation has a valid
-replacement interface. Another addition-count reduction alone does not answer it.
+reduces scalar additions while failing the original H2/K syntax. The retained
+[semantic-D evidence map](../../research/r439-semantic-d-navigation/README.md)
+links the replacement lemma (#1194), its application to the changed-A word
+(#1311), and that word's complete finite nine-stage hosted invoice (#1806).
+For the exact 10,652-ADD word, the remaining step is supplier-admission review
+under the inherited physical/all-size premises; its paid profile is unchanged.
+For a different helper operation, first identify which hypothesis or boundary
+the existing contract does not cover.
 
 The historical 71-record heterogeneous-owner catalogue excludes the selected k8
 provider. The [source-bound applicability receipt](../../research/selected-k8-catalogue-scope/README.md)

docs/research/research-glossary.md

@@ -19,7 +19,7 @@ and contracts govern a proof; historical packages may use different conventions.
 | Owner / bank | A physical allocation used to host logical helper families. Compatibility, capacity and timing must be established; reuse is not free by declaration. |
 | Hosting | Realizing logical calls and frames on actual data/streams with the promised layout and access costs. |
 | H1–H5 | Named hypotheses of the selected bit scalar-interface lemma, covering gate directions, frames, ordering and cleanup. They are not five universal laws for all networks. See the [checker’s interface description](../../research/e8-bit-p111-tuned/code/xcheck_p.py). |
-| H2/K gap | A candidate can pass some finite identities yet fail an inherited restriction on D-stage gates or the required D/K correspondence. It needs a new implication, not a disabled check. |
+| H2/K gap | A failure of the original D-stage gate restriction or literal D/K comparison. Fixed R439 words already have a [semantic replacement and finite hosted follow-up](../../research/r439-semantic-d-navigation/README.md); a different word still needs the full boundary and continuation contract. The original syntactic flags can remain false. |
 | All-size / uniform | Correctness for the algorithm's whole permitted parameter range, rather than only the finite address sizes tested. |
 | Cold replay | Reconstruct and check the relevant construction from its pinned inputs, under its declared environment and coverage. |
 | Scoped obstruction | An exclusion with explicit hypotheses. Changing a hypothesis may escape it; increasing search size inside an excluded class does not. |

research/r439-semantic-d-navigation/README.md

@@ -0,0 +1,134 @@
+# R439 semantic D: the retained lemma, bridge and hosted invoice
+
+The R439 helper-mixing handoff has progressed beyond its historical H2/K
+syntax failure. PR1194 supplies a replacement scalar contract, PR1311 checks
+its application to PR1122's changed-A word, and PR1806 completes that exact
+word's finite nine-stage hosted invoice. The remaining adoption decision must
+account for the inherited physical and all-size premises. At the pinned base,
+the selected bit supplier is still PR589 and the paid profile is unchanged.
+
+This is a **navigation and evidence-binding result**, scoped to those records
+and their PR1062 predecessor. It repairs the next-step pointer in the
+[bottleneck brief](../../docs/research/bottleneck-brief.md) and the
+[glossary](../../docs/research/research-glossary.md). It contributes no new
+contract proof, circuit, native execution, hosted construction or exponent.
+Historical package text and receipts remain preserved.
+
+Base: `c676548106012571fefa1dce0ec16f1bcfe11dce`.
+The [local task card](TASK.json) records chooser nonce
+`d2435983b76fd86391c83bd4a80e7e79`, consolidation / `scope-navigation`, priority
+revision 3. The claim is in [discussion #1796](https://github.com/CrocSwap/integer-mult-bounds/discussions/1796#discussioncomment-18930573).
+
+## Read the evidence at the right layer
+
+| Layer and exact object | Retained evidence | What it establishes; boundary |
+|---|---|---|
+| Original syntax on PR1062's 11,500-ADD B/star word | Sagar Thakrar's [PR1062 package](../r439-bsection-stars-seed01/README.md), [certificate](../r439-bsection-stars-seed01/CERTIFICATE.json) | Literal `H2_D_frame0_targets_from_helpers` and `K_equals_D` are false. Other inherited flags pass. Those two false flags describe the original checker. |
+| Replacement scalar contract on that PR1062 word | woklerx's [PR1194 proof](../r439-semantic-d-contract-seed10/PROOF.md), [receipt](../r439-semantic-d-contract-seed10/RESULT.json) | The zero-frame D boundary is `(x,y,h) -> (x,y+Nh,h)` on arbitrary dirt, with `N=K`. A proof-only original-D splice satisfies the old chronological interface. Common-frame realization and the continuation's conditions remain premises. |
+| Different A and cleanup in the 10,652-ADD word | Gareth Davidson's [PR1122 composition](../r439-abc-star-composition/README.md) and Arham Tahir's [PR1311 bridge](../r439-abc-semantic-bridge/README.md) | PR1122 supplies the circuit and native 5/9/11-stage evidence. PR1311 checks all 661 dirty columns and the **changed continuation**, including raw J/V/K and the original-D splice. Equality of D alone would not check that changed continuation. |
+| Finite nine-stage hosted execution and full invoice for exactly PR1122 | Matthieu Pascal's [PR1806 package](../r439-abc-hosted-invoice/README.md), [receipt](../r439-abc-hosted-invoice/RESULT.json) | Fresh native 5/9-stage evidence, 126,432 helper occurrences, zero banks, 3,911,328 emitted instructions and 904,896 paid children. Precision uses 176/390 bits and is charged at 192/512. This completes the finite hosted-invoice handoff left in PR1311. |
+| Selected supplier and outer result at this base | [Selected record](../../certificates/selected-result.json), [selected assembly](../community-frontier1094-audit/ASSEMBLY.json) | The assembly's `bit_supplier` is PR589 at `a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46`. Incorporating the preceding research packages does not select PR1122. The bit saving is unchanged and the complex side binds. |
+
+The exact retained heads, locations and contributor handles are reproduced in
+[RESULT.json](RESULT.json) from the reviewed disposition records. The records
+for [#1194](../../docs/research/community-efficient300-review.md),
+[#1311](../../docs/research/community-efficient400-review.md) and
+[#1806](../../docs/research/community-efficient800-review.md) explicitly retain
+these scopes. This map is not a review of every later helper-mixing word.
+
+## Which hypotheses still matter?
+
+PR1194's D contract requires source-free additions at the common zero frame,
+no COPY/ERASE, recursive child, allocation or frame-change event inside D,
+complete restoration of dirty helper and target bases, and its retained H1
+restriction on target feedback. The continuation still needs H1/H3/H4/H5 and
+the separately checked raw `J=I`. The chronological argument substitutes only
+the equal-value, equal-frame prefix before an identical continuation; its
+virtual D is not executed or charged.
+
+Thus the original syntactic failures and the successful replacement contract
+can coexist. Likewise PR1311's stored `hosted_admission: false` records **that
+package's scope**. PR1806 subsequently supplies the missing finite hosted
+invoice for the identical candidate. It explicitly leaves acceptance of the
+replacement interface and inherited physical/all-size premises separate.
+Neither record is made false by the later work.
+
+A proposal that changes the frame, reads sources, permits target feedback or
+changes the continuation must identify the corresponding missing implication.
+PR1194 alone does not certify such a proposal. A scalar addition saving also
+does not improve the recursive moment: the local rank mass remains 5,129,
+and PR1806 retains PR589's complete bit profile and saving.
+
+## Reproduce this navigation check
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -I -B scripts/research_package.py --package research/r439-semantic-d-navigation --check-only
+python3 -I -B scripts/research_package.py --package research/r439-semantic-d-navigation
+```
+
+Expected replay output:
+
+```text
+PASS_R439_SEMANTIC_D_NAVIGATION chain=5 controls=8 selected_bit=589 no_new_kappa
+PASS_REGISTERED_RESEARCH_PACKAGE research/r439-semantic-d-navigation outcome=completed
+```
+
+The check binds fourteen inputs by SHA256, checks five exact retained heads
+and credits, compares the 111 semantic compensation rows and the old/virtual
+interface flags, and binds the hosted receipt to the PR1311 receipt and actual
+PR1122 candidate bytes. It recounts 10,652 literal ADDs, checks the recorded
+local/hosted profile relationships and precision charges, and follows the
+selected record to its PR589 supplier. Immutable gzip inputs retain their exact
+source hashes; this check does not compare regenerated gzip containers.
+
+Eight controls mutate evidence **after** source admission: wrong word, wrong
+bridge receipt, semantic/syntactic H2 confusion, an incomplete virtual bridge,
+a changed local profile, an understated hosted invoice, a reduced precision
+charge and an unadopted word labeled selected. All must fail at the named
+relationship. Normal replay is read-only; `verify.py --write` regenerates only
+this package's receipt.
+
+For this contribution, the following existing local verifiers were also run
+successfully on CPython 3.12.3:
+
+```sh
+python3 -I -O -B research/r439-semantic-d-contract-seed10/verify.py
+python3 -I -B research/r439-abc-semantic-bridge/verify.py
+```
+
+They report `PASS_SEMANTIC_D_CONTRACT` (661 columns, seven controls) and
+`PASS_R439_ABC_SEMANTIC_BRIDGE` (661 columns, nine negative controls). Their
+mathematical implementations and results belong to the cited predecessors.
+They are separate from the lightweight registered navigation check.
+
+Native execution, the hosted emitter/auditor, exact moment enclosure and the
+selected full cold replay were **not rerun here**. The full PR1806 reproduction
+command and environment are in its linked README. This map checks the binding
+of its retained evidence, not the correctness of every producer or a complete
+multiplication theorem. No new complex packing-cap or kappa claim is made.
+
+## Open next questions
+
+For an authorized supplier-admission review, does the exact PR1122 word satisfy
+the maintained semantic-interface policy and all inherited physical/all-size
+obligations? Start with PR1194's chronological proof, PR1311's changed-A bridge
+and PR1806's complete bound invoice, then enumerate the remaining admission
+requirements. The blocker is acceptance and fulfillment of those requirements,
+not another derivation of the same scalar lemma or missing finite nine-stage
+invoice. Its unchanged paid profile supplies no exponent improvement.
+[TASK.json](TASK.json) records this same question and stopping boundary.
+
+## Credit
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+New material is under the repository's Apache-2.0 license.
+
+The mathematical and implementation results belong to **Sagar Thakrar**
+(PR1062), **Gareth Davidson / bitplane** (PR1122), **woklerx** (PR1194),
+**Arham Tahir** (PR1311), and **Matthieu Pascal / mtpsl** (PR1806). Their lineage
+includes **Sricharan Vagvala** (PR967 helper stars), **Aaron Wang** (PR1015),
+**Ross Richardson** (PR923), **DreamingOfClouds** (PR589/510), **eumemic**
+(PR555/543), **Zhihao Chen** (PR425), and the retained exporter, native,
+hosting and moment contributors. Their source notices remain unchanged.

research/r439-semantic-d-navigation/RESULT.json

@@ -0,0 +1,74 @@
+{
+  "kind": "source-bound navigation evidence, not a new supplier replay",
+  "retained_chain": [
+    {
+      "pr": 1062,
+      "head": "cd016e5dcd5ba28dafa3f3b4eeef003a38e6a11b",
+      "author": "thakrarsagar",
+      "package": "research/r439-bsection-stars-seed01"
+    },
+    {
+      "pr": 1122,
+      "head": "a2551e70fce0cc34348f50f1a94e7cc4c80bbcbf",
+      "author": "bitplane",
+      "package": "research/r439-abc-star-composition"
+    },
+    {
+      "pr": 1194,
+      "head": "2e39c98238f543d988f9efc1b076590a4b780dca",
+      "author": "woklerx",
+      "package": "research/r439-semantic-d-contract-seed10"
+    },
+    {
+      "pr": 1311,
+      "head": "a2875c1834b9c9ef42a84eda4890d5462cc98fa5",
+      "author": "Arham-Tahir64",
+      "package": "research/r439-abc-semantic-bridge"
+    },
+    {
+      "pr": 1806,
+      "head": "48153115a150af98a9c94adb34cab180dcd226e5",
+      "author": "mtpsl",
+      "package": "research/r439-abc-hosted-invoice"
+    }
+  ],
+  "candidate_sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066",
+  "semantic_compensation_rows": 111,
+  "syntactic_failures": [
+    "H2_D_frame0_targets_from_helpers",
+    "K_equals_D"
+  ],
+  "virtual_bridge_all_flags": true,
+  "local_ADDs": {
+    "PR1062": 11500,
+    "PR1122": 10652
+  },
+  "unchanged_local_rank_mass": 5129,
+  "hosted_helpers": 126432,
+  "hosted_banks": 0,
+  "hosted_instructions": 3911328,
+  "hosted_paid_children": 904896,
+  "precision_used_and_charged": [
+    [
+      176,
+      192
+    ],
+    [
+      390,
+      512
+    ]
+  ],
+  "selected_bit_pr": 589,
+  "bit_saving": "1733427039589844234749/1000000000000000000000000",
+  "new_kappa": false,
+  "controls_rejected": [
+    "wrong hosted word",
+    "wrong bridge receipt",
+    "literal H2 confused with semantic H2",
+    "incomplete virtual bridge",
+    "changed local profile",
+    "understated invoice profile",
+    "lowered precision charge",
+    "unadopted word called selected"
+  ]
+}

research/r439-semantic-d-navigation/SOURCES.json

@@ -0,0 +1,96 @@
+{
+  "schema_version": 1,
+  "base_commit": "c676548106012571fefa1dce0ec16f1bcfe11dce",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    },
+    {
+      "path": "research/community-batch1099-audit/DISPOSITIONS.json",
+      "usage": "input",
+      "git_blob": "63791463b469f8c517f4c007ccabc3c4b92f3736",
+      "sha256": "81f584c1f802266cd02acd2513572b8ae012da577403f9c46620dd4094ce0a41"
+    },
+    {
+      "path": "research/community-efficient300-audit/DISPOSITIONS.json",
+      "usage": "input",
+      "git_blob": "46a71b59086d163d8aa4312aeb369b5e31a9eef3",
+      "sha256": "b5b1232b5f3580f41947cca4437c7f5726c01daf50a0ad2b9aff8d80db3c5a64"
+    },
+    {
+      "path": "research/community-efficient400-audit/DISPOSITIONS.json",
+      "usage": "input",
+      "git_blob": "74cb62a1697800532c7b6b35287efcd0bbe02fc7",
+      "sha256": "3d6c4ddb87902503a043b8609fd8fdafaa7bdef416cb977f73271542d458b147"
+    },
+    {
+      "path": "research/community-efficient800-audit/DISPOSITIONS.json",
+      "usage": "input",
+      "git_blob": "b1ffec4df832a93780283b7e6f660bb27a2afa78",
+      "sha256": "d97825a16961faa81b42c0a2007bef86c39572172f229a8a903a45664a1c6247"
+    },
+    {
+      "path": "research/community-frontier1094-audit/ASSEMBLY.json",
+      "usage": "input",
+      "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0",
+      "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045"
+    },
+    {
+      "path": "research/r439-abc-hosted-invoice/README.md",
+      "usage": "input",
+      "git_blob": "9a289d1090f9d6881dc3e71252e9092b64c2a7dd",
+      "sha256": "fa70300a234c6a1d80c3bdd1acab79f1a15da4ff459b2384f7222046b01a56d5"
+    },
+    {
+      "path": "research/r439-abc-hosted-invoice/RESULT.json",
+      "usage": "input",
+      "git_blob": "75fc85424f6f62e248a295483bf157de79724daa",
+      "sha256": "6df8eda1973bfed47b055017057947d8d81b4654de30efbc562a6d1c210c3b94"
+    },
+    {
+      "path": "research/r439-abc-semantic-bridge/RESULT.json",
+      "usage": "input",
+      "git_blob": "c99ce921c94237bac60c6e4d52cfd362c4d34d08",
+      "sha256": "2cb4c886d02714a103e5e59ab1aaca7501c41845c5224a7a4f054d62a68a336d"
+    },
+    {
+      "path": "research/r439-abc-semantic-bridge/inputs/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "0ab597fefd68bfefecc85d631b172d174bdaeb70",
+      "sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066"
+    },
+    {
+      "path": "research/r439-abc-star-composition/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "0ab597fefd68bfefecc85d631b172d174bdaeb70",
+      "sha256": "2b09a7a3851cdf2a7f19350d1555cf75788d001c9507a37e459cd931881ee066"
+    },
+    {
+      "path": "research/r439-bsection-stars-seed01/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "2cff2738f7869abb58b95cc7eec533c46c4a591a",
+      "sha256": "252cf7c4981be1c9dcfb7654d917d51a0303a21eee036988b74f9ef436f9c287"
+    },
+    {
+      "path": "research/r439-semantic-d-contract-seed10/PROOF.md",
+      "usage": "input",
+      "git_blob": "2707fdb0d2f34c1c6c4ea41c2a68e44904a3e4fd",
+      "sha256": "dfbca8c61a92fdf0db8af450dc4466849da37fc296e28b67f357e196e87327db"
+    },
+    {
+      "path": "research/r439-semantic-d-contract-seed10/RESULT.json",
+      "usage": "input",
+      "git_blob": "88e2eb701156e8361787b54951ec2df1097cacf1",
+      "sha256": "64eaffd2493c8eb19d624f8cdd9158f4e4c91b8af5f7160076af002dd1bf50fb"
+    }
+  ]
+}