Record that the #4091 ceiling still bounds the 1090-call fill

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.

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.

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"
+    }
+  ]
+}