From a0dab1be029af75ef635a10eb9c905014dc54a31 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 23 Oct 2026 13:41:36 +0000 Subject: [PATCH] Record that the #4091 ceiling still bounds the 1090-call fill The THREE/FOUR words, owner capacities and stock coefficient of the pooled ceiling match the later mixed fill. The 1090-call root stays strictly below that ceiling and strictly above the 1080 literal root. No new kappa. Co-authored-by: unpaidmoon --- .../PROOF.md | 101 ++++++++ .../README.md | 116 +++++++++ .../SOURCES.json | 120 +++++++++ .../TASK.json | 106 ++++++++ .../VERIFY.json | 36 +++ .../verify.py | 238 ++++++++++++++++++ 6 files changed, 717 insertions(+) create mode 100644 research/staged-fourth-ceiling-equivalence/PROOF.md create mode 100644 research/staged-fourth-ceiling-equivalence/README.md create mode 100644 research/staged-fourth-ceiling-equivalence/SOURCES.json create mode 100644 research/staged-fourth-ceiling-equivalence/TASK.json create mode 100644 research/staged-fourth-ceiling-equivalence/VERIFY.json create mode 100644 research/staged-fourth-ceiling-equivalence/verify.py diff --git a/research/staged-fourth-ceiling-equivalence/PROOF.md b/research/staged-fourth-ceiling-equivalence/PROOF.md new file mode 100644 index 0000000000..1bae4c406d --- /dev/null +++ b/research/staged-fourth-ceiling-equivalence/PROOF.md @@ -0,0 +1,101 @@ +# Equivalence of the pooled ceiling with the 1,090-call fill + +The #4091 certificate in `research/staged-fourth-mixture-ceiling` is pinned to +PR #4088 head `76088d49e3ed4142a958659aa996b0ca4da5e88e`. Its unique pooled +optimum uses 1,080 fourth-entry calls. The later literal fill in +`research/staged544-mixed-fourth-entry` uses 1,090. This note checks the three +quantities the ceiling needs before that number can be read against the later +fill: the local words, the bin capacities, and the stock coefficient. + +## Words + +The four gzip exports + +```text +THREE-base.json.gz +THREE-extra.json.gz +FOUR-base.json.gz +FOUR-extra.json.gz +``` + +are byte-identical in the two packages. Their gzip SHA-256 values are the +ceiling's `source_sha256` pins, and the SHA-256 values of the decompressed +JSON are the later package's `INPUTS.json` pins. Both THREE orientations have +local profile + +```text +L3 = 2487 H1 + 713 H2 + 224 H3 + 102 H4 + 20 H5 + 8 H8 +``` + +and width inventory `{5:28, 6:18, 7:56, 8:93, 9:213}`. Both FOUR orientations +have + +```text +L4 = L3 + 2 H1 + 3 H3 - 3 H4 +``` + +and width inventory `{5:28, 6:18, 7:57, 8:92, 9:213}`. Helper 601 is recorded +at entrance `[45]` in THREE and `[127, 45]` in FOUR. The local rank mass falls +by exactly one from L3 to L4. + +## Capacity + +`owner/TEMPLATE.json.gz` and `owner/ORDER.json` are byte-identical. The +template has 2,016 child rows, 18 on each of 112 ports, with ranks + +```text +{8:672, 16:448, 32:448, 48:448}. +``` + +Multiplying by the 360 replicas gives the ceiling's bin counts + +```text +{8:241920, 16:161280, 32:161280, 48:161280}, +``` + +725,760 bins and total capacity 17,418,240. + +## Stock + +Both proofs use the comparison stock `(896*360)*73 = 23,546,880` and the paid +rank-mass identity `65088*360 = 23,431,680`. Rebuilding the recorded profiles +from the words and the recorded idle histograms gives that mass for both: + +```text +2160 L3 + 1080 L4 + (22788 H3 + 1620 H5 + 138492 H48) +2150 L3 + 1090 L4 + (22783 H3 + 1625 H5 + 138492 H48). +``` + +The first identity is the ceiling's recorded complete profile. The second is +the later fill's recorded profile. The ten extra fourth calls lower the local +rank mass by ten, and the later idle rank mass is ten higher. The total does +not move. + +## What the selector change does to the root + +The ceiling's literal-minus-ideal histogram still contains one rank-16 term +and two rank-32 terms. The 1,090-call idle support is only ranks 3, 5 and 48. +The two recorded roots, as reduced comparisons of the pinned rational +endpoints, satisfy + +```text +1080 literal upper < 1090 lower < 1090 upper < pooled ceiling lower. +``` + +The separations are + +```text +1090 lower - 1080 literal upper = 810594906779329 / 10^24, +pooled ceiling lower - 1090 upper = 1140318244487201 / 10^24. +``` + +The shared words, capacities and stock coefficient make the pooled ceiling the +correct optimistic cap for this two-word invoice, including a 1,090-call +mixture. The 1,090 root does not exceed it. The headroom `1.951e-9` measured +from the 1,080 literal fill is a different gap: the later fill has already +moved part of the way from that literal root toward the ceiling. + +No pattern of the 841-bin program is replayed here, and no claim is made that +the 1,090 idle histogram is a feasible point of that program beyond the +recorded capacity and rank-mass identities. The ordinary/outer four-provider +rebind is not run. diff --git a/research/staged-fourth-ceiling-equivalence/README.md b/research/staged-fourth-ceiling-equivalence/README.md new file mode 100644 index 0000000000..4cda76bb9e --- /dev/null +++ b/research/staged-fourth-ceiling-equivalence/README.md @@ -0,0 +1,116 @@ +# The #4091 pooled ceiling still bounds the 1,090-call fill + +**Audit of a fixed two-word invoice. No new κ.** The selected record remains +`60403/20000000 = 0.00302015`. + +The pooled ceiling in +[research/staged-fourth-mixture-ceiling](../staged-fourth-mixture-ceiling/README.md) +is pinned to PR #4088 head `76088d49e3ed4142a958659aa996b0ca4da5e88e` and its +unique optimum uses 1,080 fourth-entry calls. The later literal fill in +[research/staged544-mixed-fourth-entry](../staged544-mixed-fourth-entry/README.md) +uses 1,090 of the same 3,240 calls. This package checks the three quantities +that ceiling needs before it can be read against the later fill: the local +words, the bin capacities, and the stock coefficient. + +## Result + +The four gzip word exports are byte-identical. Their gzip SHA-256 values are +the ceiling `source_sha256` pins. The SHA-256 values of the decompressed JSON +are the later package's `INPUTS.json` pins. Both THREE orientations have + +```text +L3 = 2487 H1 + 713 H2 + 224 H3 + 102 H4 + 20 H5 + 8 H8 +``` + +and widths `{5:28, 6:18, 7:56, 8:93, 9:213}`. Both FOUR orientations have +`L4 = L3 + 2 H1 + 3 H3 - 3 H4` and widths `{5:28, 6:18, 7:57, 8:92, 9:213}`. +Helper 601 is recorded at entrance `[45]` in THREE and `[127, 45]` in FOUR. +Local rank mass falls by exactly one. + +`owner/TEMPLATE.json.gz` and `owner/ORDER.json` are byte-identical. The +template has 2,016 child rows, 18 on each of 112 ports, with ranks +`{8:672, 16:448, 32:448, 48:448}`. Times 360 replicas this is the ceiling bin +count `{8:241920, 16:161280, 32:161280, 48:161280}`: 725,760 bins and total +capacity 17,418,240. + +Both proofs use the comparison stock `(896*360)*73 = 23,546,880` and the paid +mass `65088*360 = 23,431,680`. Rebuilding the recorded profiles from the words +and the recorded idle histograms gives that mass for both: + +```text +2160 L3 + 1080 L4 + (22788 H3 + 1620 H5 + 138492 H48) +2150 L3 + 1090 L4 + (22783 H3 + 1625 H5 + 138492 H48) +``` + +The ten extra fourth calls lower the local rank mass by ten, and the later +idle rank mass is ten higher. The total stays put. + +The recorded roots satisfy + +```text +1080 literal upper < 1090 lower < 1090 upper < pooled ceiling lower. +``` + +The separations are exact: + +```text +1090 lower − 1080 literal upper = 810594906779329 / 10^24 +pooled ceiling lower − 1090 upper = 1140318244487201 / 10^24 +``` + +The shared words, capacities and stock coefficient make the pooled ceiling the +optimistic cap for this two-word invoice at 1,090 calls as well. The later +root stays under it. The headroom `1.951e-9` measured from the 1,080 literal +fill is a different gap: the later fill has already moved part of the way from +that literal root toward the ceiling. The ceiling's literal-minus-ideal +histogram still contains one rank-16 term and two rank-32 terms. The 1,090-call +idle support is ranks 3, 5 and 48. + +The argument is in [PROOF.md](PROOF.md). The checker reads the pinned bytes +and rebuilds both mixtures. It does not import either predecessor verifier. + +## Scope + +Task card `independent-moment`, priority revision 7, base +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. Scope status is **refined**: the +card's first step asks for this equivalence before the #4091 ceiling is applied +to the later fill. + +This comparison stops at the three identities and the two root separations. +It does not replay the 841-pattern linear program, so it does not show that +the 1,090 idle histogram is a feasible point of that program beyond the +recorded capacity and rank-mass identities. The ordinary/outer four-provider +rebind is left to +[research/staged544-mixed-idle-rebind](../staged544-mixed-idle-rebind/README.md). + +## Reproduce + +From the repository root, Python 3.12 standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/staged-fourth-ceiling-equivalence --check-only +python3.12 -B scripts/research_package.py --package research/staged-fourth-ceiling-equivalence +``` + +The direct checker is `python3.12 -B research/staged-fourth-ceiling-equivalence/verify.py`. +It prints `PASS_STAGED_FOURTH_CEILING_EQUIVALENCE`. Live inputs are the sixteen +predecessor files listed in [VERIFY.json](VERIFY.json). Pins are in +[SOURCES.json](SOURCES.json). + +## Open next questions + +1. Does the 1,090-call idle `{3:22783, 5:1625, 48:138492}` correspond to a + feasible pattern vector of the 841-pattern program? Express the idle delta + from the certified eight-pattern witness as a combination of tight patterns. + Pattern enumeration is not replayed here. +2. Can the pinned ordinary rebind take four provider ids, recompute this idle, + and still pass the outer release? That is open question 1 of + `research/staged544-mixed-idle-rebind`. Equivalence does not run it. + +Structured fields are in [TASK.json](TASK.json). + +## Credit + +Credit Cinna Davis and PR #4088 for the later fill, and Ross Richardson and +PR #4091 for the pooled ceiling. Prepared by unpaidmoon with substantial Cursor +Grok assistance. New work is Apache-2.0. diff --git a/research/staged-fourth-ceiling-equivalence/SOURCES.json b/research/staged-fourth-ceiling-equivalence/SOURCES.json new file mode 100644 index 0000000000..43da34aa70 --- /dev/null +++ b/research/staged-fourth-ceiling-equivalence/SOURCES.json @@ -0,0 +1,120 @@ +{ + "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/staged-fourth-mixture-ceiling/PROOF.md", + "usage": "input", + "git_blob": "c67a80c8727ee45e2ba61de28bbaca8bb6d45e2a", + "sha256": "fc9a073b2c334e8e413062157569653e8bb52db81d72d68621287f6810090f40" + }, + { + "path": "research/staged-fourth-mixture-ceiling/RESULT.json", + "usage": "input", + "git_blob": "2803d5c42b5d49ea72bd9bb006ffb4a9eec6a316", + "sha256": "53849028b12f7d9b726ac7576eeb64dc9a1a51bb2890edbb15aa83d1e39fae5f" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-base.json.gz", + "usage": "input", + "git_blob": "65957e5ca322049d985f23fdc0bd8da07ffa4c2a", + "sha256": "aecaddba48fdff6353a6511c3623346b05aa607e30103fb016604a2b1025ce95" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-extra.json.gz", + "usage": "input", + "git_blob": "1f3239c30e9343cf4e34b4371fcbeebb94a19011", + "sha256": "615093190aa5479034bb8acdd8925d7a910e082b84dec7df84b459b62421235a" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-base.json.gz", + "usage": "input", + "git_blob": "137793e275870db2161048405017b83dcc1824ee", + "sha256": "df31495cff95a1e512da398f52841c6b5ade29067869b3d68b89d756a5641112" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-extra.json.gz", + "usage": "input", + "git_blob": "7cce921b20dc0504cea954ab3297c5b55a9468dc", + "sha256": "9a28f7ef91938c0866e408eb06e03eb5f8e727a00b44eb936ddd5ed48704bd4c" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/owner/ORDER.json", + "usage": "input", + "git_blob": "58d4b4c34170788a825d4c4e595fe45e28ef3fd2", + "sha256": "743e74b538432e2b2045e754b0de9c18f36fc5039fdb8eb542177a898ec78e44" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/owner/TEMPLATE.json.gz", + "usage": "input", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + }, + { + "path": "research/staged544-mixed-fourth-entry/INPUTS.json", + "usage": "input", + "git_blob": "5898f7e11f827baa4122fa17d4aa251b990efff6", + "sha256": "43ab5cd305ec23dbc63accaffb0dca8bdf201130bff89f5e807d919c5118fc98" + }, + { + "path": "research/staged544-mixed-fourth-entry/PROOF.md", + "usage": "input", + "git_blob": "9c665b0442774b8c84116f51c3261d50dd5f8d2c", + "sha256": "3aa03a9ba64422474890c137d2b10ef830464712830fd469fe1b0e9538b24ebb" + }, + { + "path": "research/staged544-mixed-fourth-entry/RESULT.json", + "usage": "input", + "git_blob": "1174e25e2ef8f8bc9a0815c43ba5d64c8af08349", + "sha256": "6346ee768637aa9a1891d1d61d800d640235420b320fb7e659d1bf664ec42b3d" + }, + { + "path": "research/staged544-mixed-fourth-entry/inputs/FOUR-base.json.gz", + "usage": "input", + "git_blob": "65957e5ca322049d985f23fdc0bd8da07ffa4c2a", + "sha256": "aecaddba48fdff6353a6511c3623346b05aa607e30103fb016604a2b1025ce95" + }, + { + "path": "research/staged544-mixed-fourth-entry/inputs/FOUR-extra.json.gz", + "usage": "input", + "git_blob": "1f3239c30e9343cf4e34b4371fcbeebb94a19011", + "sha256": "615093190aa5479034bb8acdd8925d7a910e082b84dec7df84b459b62421235a" + }, + { + "path": "research/staged544-mixed-fourth-entry/inputs/THREE-base.json.gz", + "usage": "input", + "git_blob": "137793e275870db2161048405017b83dcc1824ee", + "sha256": "df31495cff95a1e512da398f52841c6b5ade29067869b3d68b89d756a5641112" + }, + { + "path": "research/staged544-mixed-fourth-entry/inputs/THREE-extra.json.gz", + "usage": "input", + "git_blob": "7cce921b20dc0504cea954ab3297c5b55a9468dc", + "sha256": "9a28f7ef91938c0866e408eb06e03eb5f8e727a00b44eb936ddd5ed48704bd4c" + }, + { + "path": "research/staged544-mixed-fourth-entry/owner/ORDER.json", + "usage": "input", + "git_blob": "58d4b4c34170788a825d4c4e595fe45e28ef3fd2", + "sha256": "743e74b538432e2b2045e754b0de9c18f36fc5039fdb8eb542177a898ec78e44" + }, + { + "path": "research/staged544-mixed-fourth-entry/owner/TEMPLATE.json.gz", + "usage": "input", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + } + ] +} diff --git a/research/staged-fourth-ceiling-equivalence/TASK.json b/research/staged-fourth-ceiling-equivalence/TASK.json new file mode 100644 index 0000000000..260669a945 --- /dev/null +++ b/research/staged-fourth-ceiling-equivalence/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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": "refined", + "actual_scope": "Compare the byte-level THREE/FOUR words, template capacities and stock coefficient of staged-fourth-mixture-ceiling with staged544-mixed-fourth-entry, and place the recorded 1090-call root against the pooled ceiling and the 1080-call literal root.", + "scope_change_reason": "The card asks whether a mixture-ceiling claim has independent source-bound coverage of its changed ledger. Its first step names this comparison: #4091 pins an earlier #4088 head, so word, capacity and stock equivalence have to be checked before that ceiling is applied to the later 1090-call fill. This package does that comparison. It does not search residual exchanges or rerun four-provider admission.", + "bottleneck_link": "The selected frontier stays at 60403/20000000. A higher conditional endpoint still has to pass the pooled two-word invoice. Equivalence shows that the #4091 ceiling remains a valid cap for the later fill's words, capacities and stock, while the 1.951e-9 headroom of the 1080-call literal is a different gap from the 1090-call root.", + "budget_minutes": 60, + "stop_rule": "Stop after the word, capacity and stock identities, the two exact root separations, and the three failure controls. Do not replay the 841-pattern linear program, the native stages, or the ordinary/outer release.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/staged-fourth-ceiling-equivalence. The four word gzip files and the owner template and order are byte-identical. Both rebuilt profiles have paid mass 65088*360. The 1090-call root sits strictly above the 1080 literal upper by 810594906779329/10^24 and strictly below the pooled ceiling lower by 1140318244487201/10^24. Three semantic controls reject a shifted profile, the 1080 idle on the 1090 selector, and a truncated word.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does the 1090-call idle histogram {3:22783, 5:1625, 48:138492} correspond to a feasible pattern vector of the 841-pattern pooled program?", + "why_it_matters": "Word, capacity and stock equivalence make the pooled ceiling a valid optimistic cap for this invoice. Feasibility would say whether that idle is an attainable point of the same relaxation, which is a stronger statement than the root comparison.", + "first_step": "Express the idle delta from the certified eight-pattern witness at x=1080 as an integer combination of tight patterns, then check capacity and the width-5 through width-9 helper totals.", + "blocked_by": "This package does not replay the 841-pattern enumeration." + }, + { + "question": "Can the pinned ordinary rebind be extended to four provider ids so the mixed idle is recomputed and the full outer release still passes?", + "why_it_matters": "That remains the admission gate for the 1090-call endpoint. Equivalence of the ceiling model does not admit the fill.", + "first_step": "Follow open question 1 of research/staged544-mixed-idle-rebind: add the two fourth-entry provider ids, stamp each call's width vector, recompute idle from the literal bins, and rerun the existing admission controls.", + "blocked_by": "The full release needs the reconstructed source closure, native cache and outer wheels. This session stops at the equivalence." + } + ] +} diff --git a/research/staged-fourth-ceiling-equivalence/VERIFY.json b/research/staged-fourth-ceiling-equivalence/VERIFY.json new file mode 100644 index 0000000000..bea830f514 --- /dev/null +++ b/research/staged-fourth-ceiling-equivalence/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/staged-fourth-mixture-ceiling/PROOF.md", + "research/staged-fourth-mixture-ceiling/RESULT.json", + "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-base.json.gz", + "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-extra.json.gz", + "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-base.json.gz", + "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-extra.json.gz", + "research/staged-fourth-mixture-ceiling/source4088/owner/ORDER.json", + "research/staged-fourth-mixture-ceiling/source4088/owner/TEMPLATE.json.gz", + "research/staged544-mixed-fourth-entry/INPUTS.json", + "research/staged544-mixed-fourth-entry/PROOF.md", + "research/staged544-mixed-fourth-entry/RESULT.json", + "research/staged544-mixed-fourth-entry/inputs/FOUR-base.json.gz", + "research/staged544-mixed-fourth-entry/inputs/FOUR-extra.json.gz", + "research/staged544-mixed-fourth-entry/inputs/THREE-base.json.gz", + "research/staged544-mixed-fourth-entry/inputs/THREE-extra.json.gz", + "research/staged544-mixed-fourth-entry/owner/ORDER.json", + "research/staged544-mixed-fourth-entry/owner/TEMPLATE.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Byte identity of the four THREE/FOUR words and of the owner template and order, with gzip pins matched to the ceiling source_sha256 and decompressed pins matched to the later INPUTS.json. Template ranks times 360 equal the recorded bin counts. Both word orientations, helper-601 entrances, and the local rank-mass drop of 1. Rebuilt 1080 and 1090 mixtures equal the recorded profiles and both have paid mass 65088*360. Stock sentences (896*360)*73 and 65088*360. The 1090 root is strictly above the 1080 literal upper by 810594906779329/10^24 and strictly below the pooled ceiling lower by 1140318244487201/10^24. Three controls reject a rank-1 profile shift, the 1080 idle on the 1090 selector, and a truncated THREE-base word." + } + ] +} diff --git a/research/staged-fourth-ceiling-equivalence/verify.py b/research/staged-fourth-ceiling-equivalence/verify.py new file mode 100644 index 0000000000..5f23b1bd19 --- /dev/null +++ b/research/staged-fourth-ceiling-equivalence/verify.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Word, capacity and stock equivalence of the #4091 ceiling and the 1090-call fill. + +This checker does not import either predecessor verifier. It reads the pinned +word bytes, owner template and recorded profiles, rebuilds both mixtures, and +rejects a shifted profile, a swapped idle histogram and a one-byte word change. +""" +import collections +import gzip +import hashlib +import json +import math +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +CEILING = ROOT / "research/staged-fourth-mixture-ceiling" +LATER = ROOT / "research/staged544-mixed-fourth-entry" +WORDS = ( + "THREE-base.json.gz", + "THREE-extra.json.gz", + "FOUR-base.json.gz", + "FOUR-extra.json.gz", +) +TEMPLATE_RANKS = {8: 672, 16: 448, 32: 448, 48: 448} +THREE_WIDTHS = {5: 28, 6: 18, 7: 56, 8: 93, 9: 213} +FOUR_WIDTHS = {5: 28, 6: 18, 7: 57, 8: 92, 9: 213} +WORD_DELTA = {1: 2, 3: 3, 4: -3} +CEILING_IDLE = {3: 22788, 5: 1620, 48: 138492} +LATER_IDLE = {3: 22783, 5: 1625, 48: 138492} +PAID_MASS = 65088 * 360 +STOCK = 896 * 360 * 73 + + +class CheckFailure(Exception): + pass + + +def demand(condition, message): + if not condition: + raise CheckFailure(message) + + +def sha256(data): + return hashlib.sha256(data).hexdigest() + + +def load_json(path): + return json.loads(path.read_text(encoding="utf-8")) + + +def integers(mapping): + return {int(key): int(value) for key, value in mapping.items()} + + +def fraction(text): + numerator, denominator = str(text).split("/") + return int(numerator), int(denominator) + + +def rank_mass(profile): + return sum(rank * count for rank, count in profile.items()) + + +def mix(third, fourth, third_calls, fourth_calls, idle): + total = collections.Counter() + for profile, scale in ((third, third_calls), (fourth, fourth_calls), (idle, 1)): + for rank, count in profile.items(): + total[rank] += scale * count + return {rank: count for rank, count in total.items() if count} + + +def word_report(path): + payload = json.loads(gzip.decompress(path.read_bytes())) + report = payload["report"] + return ( + integers(report["local_profile"]), + integers(report["width_inventory"]), + [int(item) for item in payload["start_extra"]["601"]], + ) + + +def difference(left, right): + keys = set(left) | set(right) + return { + key: left.get(key, 0) - right.get(key, 0) + for key in keys + if left.get(key, 0) != right.get(key, 0) + } + + +def below(left, right): + left_n, left_d = left + right_n, right_d = right + return left_n * right_d < right_n * left_d + + +def separation(higher, lower): + high_n, high_d = higher + low_n, low_d = lower + numerator = high_n * low_d - low_n * high_d + denominator = high_d * low_d + demand(numerator > 0 and denominator > 0, "nonpositive root separation") + divisor = math.gcd(numerator, denominator) + return numerator // divisor, denominator // divisor + + +def audit(): + ceiling = load_json(CEILING / "RESULT.json") + later = load_json(LATER / "RESULT.json") + plain_pins = load_json(LATER / "INPUTS.json")["canonical_sha256"] + gzip_pins = ceiling["source_sha256"] + + for name in WORDS: + ceiling_bytes = (CEILING / "source4088/inputs" / name).read_bytes() + later_bytes = (LATER / "inputs" / name).read_bytes() + demand(ceiling_bytes == later_bytes, "word bytes differ: " + name) + demand(sha256(ceiling_bytes) == gzip_pins["inputs/" + name], "gzip pin: " + name) + demand(sha256(gzip.decompress(ceiling_bytes)) == plain_pins[name], "plain pin: " + name) + + for ceiling_rel, later_rel in ( + ("source4088/owner/TEMPLATE.json.gz", "owner/TEMPLATE.json.gz"), + ("source4088/owner/ORDER.json", "owner/ORDER.json"), + ): + demand( + (CEILING / ceiling_rel).read_bytes() == (LATER / later_rel).read_bytes(), + "owner bytes differ: " + ceiling_rel, + ) + template_bytes = (CEILING / "source4088/owner/TEMPLATE.json.gz").read_bytes() + demand( + sha256(template_bytes) == gzip_pins["owner/TEMPLATE.json.gz"], + "template pin", + ) + children = json.loads(gzip.decompress(template_bytes))["idle_children"] + ranks = collections.Counter(int(child["rank"]) for child in children) + demand(len(children) == 2016, "template row count") + demand(dict(ranks) == TEMPLATE_RANKS, "template ranks " + str(dict(ranks))) + ports = collections.Counter(int(child["port"]) for child in children) + demand(len(ports) == 112 and set(ports.values()) == {18}, "port slot count") + bins = {capacity: count * 360 for capacity, count in ranks.items()} + demand(integers(ceiling["bin_counts"]) == bins, "recorded bin counts") + demand(sum(bins.values()) == 725760, "total bins") + demand(sum(capacity * count for capacity, count in bins.items()) == 17418240, "total capacity") + + profiles = {} + widths = {} + entrances = {} + for name in WORDS: + profiles[name], widths[name], entrances[name] = word_report(LATER / "inputs" / name) + third = profiles["THREE-base.json.gz"] + fourth = profiles["FOUR-base.json.gz"] + demand(profiles["THREE-extra.json.gz"] == third, "THREE orientations differ") + demand(profiles["FOUR-extra.json.gz"] == fourth, "FOUR orientations differ") + demand(widths["THREE-base.json.gz"] == widths["THREE-extra.json.gz"] == THREE_WIDTHS, "THREE widths") + demand(widths["FOUR-base.json.gz"] == widths["FOUR-extra.json.gz"] == FOUR_WIDTHS, "FOUR widths") + demand(difference(fourth, third) == WORD_DELTA, "local-word delta") + demand(entrances["THREE-base.json.gz"] == entrances["THREE-extra.json.gz"] == [45], "THREE entrance") + demand(entrances["FOUR-base.json.gz"] == entrances["FOUR-extra.json.gz"] == [127, 45], "FOUR entrance") + demand(rank_mass(fourth) - rank_mass(third) == -1, "local rank-mass delta") + + ceiling_idle = integers(ceiling["idle"]) + later_idle = integers(later["idle"]) + demand(ceiling["calls"] == 3240 and later["calls"] == 3240, "call count") + demand(ceiling["optimum_fourth_calls"] == 1080, "pooled optimum") + demand(later["fourth_calls"] == 1090, "later selector") + demand(ceiling_idle == CEILING_IDLE, "ceiling idle") + demand(later_idle == LATER_IDLE, "later idle") + ceiling_profile = integers(ceiling["complete_profile"]) + later_profile = integers(later["profile"]) + demand(mix(third, fourth, 2160, 1080, ceiling_idle) == ceiling_profile, "ceiling mixture") + demand(mix(third, fourth, 2150, 1090, later_idle) == later_profile, "later mixture") + demand(rank_mass(ceiling_profile) == PAID_MASS, "ceiling paid mass") + demand(rank_mass(later_profile) == PAID_MASS, "later paid mass") + demand(rank_mass(later_idle) - rank_mass(ceiling_idle) == 10, "idle mass shift") + + ceiling_proof = (CEILING / "PROOF.md").read_text(encoding="utf-8") + later_proof = (LATER / "PROOF.md").read_text(encoding="utf-8") + demand("(896*360)*73=23546880" in ceiling_proof.replace(" ", ""), "ceiling stock sentence") + demand("(896*360)73^(1-k)" in later_proof.replace(" ", ""), "later stock sentence") + demand("65088*360" in ceiling_proof and "65088*360" in later_proof, "paid-mass sentence") + demand(STOCK == 23546880, "stock arithmetic") + + literal_minus_ideal = integers(ceiling["literal_minus_ideal"]) + demand(literal_minus_ideal[16] == 1 and literal_minus_ideal[32] == 2, "1080 residual terms") + demand(16 not in later_idle and 32 not in later_idle, "1090 idle support") + + ceiling_lower = fraction(ceiling["root_bracket"][0]) + later_upper = fraction(later["root_upper"]) + later_lower = fraction(later["root_lower"]) + literal_upper = fraction(ceiling["literal_root_bracket"][1]) + demand(below(later_upper, ceiling_lower), "1090 root is not below the ceiling") + demand(below(literal_upper, later_lower), "1090 root is not above the 1080 literal") + above_literal = separation(later_lower, literal_upper) + below_ceiling = separation(ceiling_lower, later_upper) + demand(above_literal == (810594906779329, 10**24), "literal separation") + demand(below_ceiling == (1140318244487201, 10**24), "ceiling separation") + + # Semantic controls. Each one changes a real identity the audit just used. + shifted = dict(later_profile) + shifted[1] += 1 + demand(shifted != mix(third, fourth, 2150, 1090, later_idle), "shifted profile was accepted") + demand( + mix(third, fourth, 2150, 1090, ceiling_idle) != later_profile, + "1080 idle was accepted as the 1090 fill", + ) + mutated = (LATER / "inputs/THREE-base.json.gz").read_bytes()[:-1] + demand(sha256(mutated) != sha256((CEILING / "source4088/inputs/THREE-base.json.gz").read_bytes()), + "truncated word still matched") + + return { + "paid_mass": PAID_MASS, + "stock": STOCK, + "bins": 725760, + "capacity": 17418240, + "above_literal": above_literal, + "below_ceiling": below_ceiling, + } + + +def main(): + try: + result = audit() + except CheckFailure as exc: + raise SystemExit("FAIL_STAGED_FOURTH_CEILING_EQUIVALENCE " + str(exc)) from exc + above_n, above_d = result["above_literal"] + below_n, below_d = result["below_ceiling"] + print( + "PASS_STAGED_FOURTH_CEILING_EQUIVALENCE" + " words=identical capacities=identical" + f" stock={result['stock']} bins={result['bins']} capacity={result['capacity']}" + f" paid_mass={result['paid_mass']} fourth=1080->1090" + f" above_literal={above_n}/{above_d}" + f" below_ceiling={below_n}/{below_d}" + " controls=3 no_new_kappa=true" + ) + + +if __name__ == "__main__": + main()