diff --git a/research/pr4610-endpoint-profile-check/.gitattributes b/research/pr4610-endpoint-profile-check/.gitattributes new file mode 100644 index 0000000000..e0d8b58e85 --- /dev/null +++ b/research/pr4610-endpoint-profile-check/.gitattributes @@ -0,0 +1 @@ +PR4610-ACTUAL-WORD.json.gz -text diff --git a/research/pr4610-endpoint-profile-check/PR4610-ACTUAL-WORD.json.gz b/research/pr4610-endpoint-profile-check/PR4610-ACTUAL-WORD.json.gz new file mode 100644 index 0000000000..79dad65b9c Binary files /dev/null and b/research/pr4610-endpoint-profile-check/PR4610-ACTUAL-WORD.json.gz differ diff --git a/research/pr4610-endpoint-profile-check/README.md b/research/pr4610-endpoint-profile-check/README.md new file mode 100644 index 0000000000..c79ad33501 --- /dev/null +++ b/research/pr4610-endpoint-profile-check/README.md @@ -0,0 +1,66 @@ +# Scoped check of #4610: endpoint frames preserved, profile arithmetic and moment positivity + +**Task:** independent-moment (independent check). **Base:** canonical main `f626db5c`. **No κ is claimed.** + +## The claim + +intqwq's #4610 (head `4b4c75bc`) claims a conditional κ of 37769/12500000 = 0.00302152. The construction: + +- substitutes 34 of PR4470's 72 independent warp generators with other invertible maps; +- relabels 422 scalar frames; +- keeps every scalar opcode and every external interface. + +Its paid list changes from Pold = 2237 H1 + 388 H2 + 494 H3 + 147 H4 + 36 H5 + 8 H8 to Pnew = 2201 H1 + 412 H2 + 506 H3 + 135 H4 + 36 H5 + 8 H8. + +## What is checked here + +Nothing is imported from #4610. Its emitted `ACTUAL-WORD.json.gz` is vendored with blob `79dad65b` and pinned by SHA256. Its canonical payload hash equals #4610's frozen value `4409d2d9…`. + +### 1. Endpoint frames + +This is the test #4596 failed (see #4604). For all 632 roles, the emitted word's **start and final frames equal PR4470's** as subspaces of F₂⁹, using PR4470's word from main's pinned constructor. The 112 ports, v = 112 and h = 9 are also unchanged, while the warp layer itself does change. So, unlike the span{511} quotient in #4596, this construction keeps every output chart. + +### 2. Profile arithmetic + +- **Profile.** The emitted word's local profile is exactly Pnew. +- **Difference.** Pold − Pnew = 12(3 H1 − 2 H2 − H3 + H4). +- **Totals.** Paid rank mass is unchanged at 5,327, with 12 fewer jobs per call. Over the 18-call controller that is 216 fewer paid calls, from 64,620 to 64,404. + +### 3. Moment positivity, with a written proof independent of #4610's intervals + +For 0 < a < 1, put x = 2^a ∈ (1, 2) and c = log₂ 3. Then + +```text +3 − 2·2^a − 3^a + 4^a = g(x) := (x − 1)² + 2 − x^c. +``` + +- **Convex:** g''(x) = 2 − c(c−1)x^{c−2} ≥ 2 − c(c−1) > 0, using x ≥ 1 and c < 2 (since 3 < 4). +- **Decreasing:** g'(2) = 2 − 3c/2 < 0, since c > 4/3 (because 27 > 16). With g convex, this gives g' < 0 on [1, 2]. +- **Conclusion:** g(2) = 0, so g(x) > 0 on (1, 2). + +The difference is therefore strictly positive for every 0 < t < 1, whichever of t or 1−t is the exponent. A 999-point grid is checked as a numerical sanity control. + +## Verify + +```text +python3 -B research/pr4610-endpoint-profile-check/verify.py +``` + +The check takes about 2 s and uses the standard library only. + +## Limitations + +**Not covered:** + +- the native Clifford and absolute-phase lowering of the 34 changed maps; +- the Lean certificates; +- the outer crossing interval (0.0030215551, 0.0030215552) and the resulting κ; +- whether substituting generators of the free-group identity is admissible under the supplier contract (a maintainer question). + +This package establishes only that the endpoints are preserved and that the claimed profile improvement is arithmetically and analytically sound. + +## Open next questions + +- **Native phase lowering.** Check it for the 34 changed G maps independently. First step: rebuild each K_G from the 9×9 binary G, using the transported-frame lemma's integer column formulas, and compare it with #4610's bound operators. + +Credit: intqwq (#4610), Cinna Davis (#4470), DaysSky and the #4535 lineage. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4610-endpoint-profile-check/SOURCES.json b/research/pr4610-endpoint-profile-check/SOURCES.json new file mode 100644 index 0000000000..a34ee9066e --- /dev/null +++ b/research/pr4610-endpoint-profile-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" + } + ] +} diff --git a/research/pr4610-endpoint-profile-check/TASK.json b/research/pr4610-endpoint-profile-check/TASK.json new file mode 100644 index 0000000000..29b9fb638a --- /dev/null +++ b/research/pr4610-endpoint-profile-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 scoped coverage of the newest kappa claim (#4610): endpoint preservation and paid-profile soundness.", + "budget_minutes": 60, + "stop_rule": "Stop at endpoint frames, profile arithmetic and moment positivity.", + "outcome": "completed", + "evidence": "Emitted ACTUAL-WORD (pinned, payload hash = #4610 freeze): all 632 start/final frames equal PR4470's, ports/v/h unchanged, warps changed; local profile = Pnew; Pold-Pnew = 12(3H1-2H2-H3+H4), rank mass 5,327 unchanged, 12 fewer jobs, 64,620 -> 64,404; written convexity proof of positivity on (0,1).", + "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 native phase lowering of the 34 changed maps.", + "why_it_matters": "Remaining unverified physical step of #4610.", + "first_step": "Rebuild K_G from each binary G via integer column formulas and compare.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4610-endpoint-profile-check/VERIFY.json b/research/pr4610-endpoint-profile-check/VERIFY.json new file mode 100644 index 0000000000..7593f97977 --- /dev/null +++ b/research/pr4610-endpoint-profile-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 #4610 word hash and payload; 632 start/final frames vs pinned PR4470 constructor; ports/v/h; local profile; profile arithmetic; moment positivity proof facts and grid." + } + ] +} diff --git a/research/pr4610-endpoint-profile-check/verify.py b/research/pr4610-endpoint-profile-check/verify.py new file mode 100644 index 0000000000..15a75a4752 --- /dev/null +++ b/research/pr4610-endpoint-profile-check/verify.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +"""Scoped independent check of PR #4610 (intqwq): conditional kappa 0.00302152 from changed native warp maps. + +#4610 (head 4b4c75bc) substitutes 34 of PR4470's 72 independent warp generators by other invertible maps and relabels +422 scalar frames, keeping every scalar opcode and external interface, and claims the paid list + Pnew = 2201 H1 + 412 H2 + 506 H3 + 135 H4 + 36 H5 + 8 H8 (Pold = 2237 H1 + 388 H2 + 494 H3 + 147 H4 + 36 H5 + 8 H8), + Pold - Pnew = 12(3 H1 - 2 H2 - H3 + H4) > 0 for every 0 < t < 1. +This verifier checks, independently of #4610's code (nothing imported from it): + 1. endpoint frames (the test #4596 failed, see #4604): the vendored emitted ACTUAL-WORD (sha256-pinned, its + canonical payload hash equal to #4610's frozen value) has, for all 632 roles, the same start and final frame + (as subspaces of F2^9) as PR4470's word from main's pinned constructor, and the same 112 ports, v and h; + 2. the emitted word's local profile is exactly Pnew; Pold - Pnew = 12(3,-2,-1,1) on (H1,H2,H3,H4); paid rank mass is + unchanged (5,327) with 12 fewer jobs per call; 18 calls give 216 fewer, 64,620 -> 64,404; + 3. 3 - 2*2^a - 3^a + 4^a > 0 for every 0 < a < 1 (so the difference is positive whichever of t, 1 - t is the + exponent): with x = 2^a in (1,2) and c = log2 3, it equals g(x) = (x-1)^2 + 2 - x^c; g'' >= 2 - c(c-1) > 0 because + c < 2 (3 < 4), and g'(2) = 2 - 3c/2 < 0 because c > 4/3 (27 > 16); so g is convex and strictly decreasing on + [1,2] with g(2) = 0. The integer facts are checked, and g is evaluated on a grid as a numerical sanity control. +Not covered: native Clifford/phase lowering, the Lean certificates, the outer crossing interval. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import gzip +import hashlib +import json +import math +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" +PAYLOAD_SHA256 = "4409d2d9328fffbd276bb03fb800f59a33ec3b2ab15f79a330a7af66e75110cc" +P_NEW = {1: 2201, 2: 412, 3: 506, 4: 135, 5: 36, 8: 8} +P_OLD = {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8} + + +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 pr4470_word(): + 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}))") + 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) + return json.loads(run.stdout)["c"] + + +def main(): + raw = WORD.read_bytes() + need(hashlib.sha256(raw).hexdigest() == WORD_SHA256, "vendored #4610 ACTUAL-WORD") + word = json.loads(gzip.decompress(raw)) + payload = json.dumps(word, sort_keys=True, separators=(",", ":")).encode() + need(hashlib.sha256(payload).hexdigest() == PAYLOAD_SHA256, "canonical payload equals #4610 freeze") + a = word["canonical"] + c = pr4470_word() + # 1. endpoint frames + need(len(a["final"]) == len(c["final"]) == 632 and len(a["start"]) == len(c["start"]) == 632, "632 roles") + final_same = sum(span(a["frames"][i]) == span(c["frames"][j]) for i, j in zip(a["final"], c["final"])) + start_same = sum(span(a["frames"][i]) == span(c["frames"][j]) for i, j in zip(a["start"], c["start"])) + need(final_same == 632 and start_same == 632, "every start and final frame equals PR4470's") + need(a["ports"] == c["ports"] and a["v"] == c["v"] == 112 and a["h"] == c["h"] == 9, "ports, v, h unchanged") + need(a["warps"] != c["warps"], "the warp layer itself did change") + # 2. profile arithmetic + need({int(k): v for k, v in a["local_profile"].items()} == P_NEW, "emitted local profile is Pnew") + diff = {r: P_OLD[r] - P_NEW[r] for r in P_OLD} + need(diff == {1: 36, 2: -24, 3: -12, 4: 12, 5: 0, 8: 0}, "Pold - Pnew = 12(3 H1 - 2 H2 - H3 + H4)") + mass = lambda p: sum(r * n for r, n in p.items()) + need(mass(P_OLD) == mass(P_NEW) == 5327 and sum(P_OLD.values()) - sum(P_NEW.values()) == 12, "mass and jobs") + need(64620 - 18 * 12 == 64404, "controller paid calls") + # 3. moment positivity: exact facts used by the convexity proof, then a numerical sanity grid + need(3 < 4 and 27 > 16, "1 < c = log2 3 < 2 and c > 4/3") + c_log = math.log2(3) + need(2 - c_log * (c_log - 1) > 1 and 2 - 1.5 * c_log < -0.3, "g'' > 0 and g'(2) < 0 (numerical margins)") + grid = [k / 1000 for k in range(1, 1000)] + need(all(3 - 2 * 2 ** s - 3 ** s + 4 ** s > 0 for s in grid), "grid sanity: 3 - 2*2^a - 3^a + 4^a > 0") + need(abs(3 - 2 * 2 - 3 + 4) == 0 and 3 - 2 - 1 + 1 == 1, "endpoint values 0 at a = 1 and 1 at a = 0") + print(json.dumps({"status": "PASS_PR4610_SCOPED_CHECK", + "endpoint_frames_equal_pr4470": {"start": start_same, "final": final_same}, + "ports_v_h_unchanged": True, "warps_changed": True, + "canonical_payload_hash_matches_freeze": True, + "local_profile": P_NEW, "paid_rank_mass": 5327, "jobs_removed_per_call": 12, + "moment_difference_positive_on_open_interval": True, + "not_covered": ["native phase lowering", "Lean certificates", "outer crossing interval"], + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())