diff --git a/research/pr4470-invoice-join/PROOF.md b/research/pr4470-invoice-join/PROOF.md new file mode 100644 index 0000000000..a0d7f718ad --- /dev/null +++ b/research/pr4470-invoice-join/PROOF.md @@ -0,0 +1,81 @@ +# Join and enclosure argument + +## 1. Charging model (taken from #4440 PROOF.md sections 1-2, not re-derived) + +Complex controller with p = 16 pairs and prefix a = 7, so there are 2p+1 = 33 local stages. +The thick stages are S = {0, 2p} ∪ {1, 3, ..., 2p-1}, which gives |S| = 18. The model has +112 ports and fresh block rank d = 8. Events are charged as follows: + +- `LOCAL(stage, pair, backward)`: one full native call. It charges one fresh copy of the local + helper targets and one copy of the local paid unit for that orientation. +- `QUERY_SHEAR(stage, ...)`: 112 paid rank-one jobs, one per port. No productive credit. +- `IDLE(pair, stages)`: both lines of the pair on every port. This is 2·112 paid jobs of rank + d·|stages|. +- `ADD`, `SIGNED_SWAP`: scalar bridges with no rank charge. They sit under the nonrecursive allowance + of #4470, which is not checked here. +- Diagonal output `(c, e_0, ..., e_32)`: c is ±1, the central Gaussian (rank 1). The term gives + 112 productive targets of rank 1 + d·|{s : e_s = 1}|. + +The verifier checks the structural conditions that make this model applicable to the +committed word: + +- one full call per thick stage; +- one query per thin stage; +- idle stages are distinct and thick; +- outputs have 0/1 exponents, support inside S, and c = ±1. + +The verifier does not prove that the word realizes the advertised operator. That is the +Laurent factorization of `research/pr4470-controller-replay`, and both packages pin the same +`CONTROLLER.json` bytes. + +## 2. Join and cross-bindings + +T is the sum of the main targets plus 18 helper copies. P is the sum of: + +- the idle charges; +- 112·15 rank-one queries; +- the forward unit, once per forward call; +- the backward unit, once per backward call. + +The units are read from #4504's committed `RESULT.json`, `profiles.new`. Both orientations are +required to carry the same paid unit with eight rank-8 center jobs. + +The #4440 closed form gives a second derivation that does not use the event word: + +- 2·112 targets of rank 1 + d(p+2); +- for j in 1..a and in 1..p-1-a: 2·112 targets of rank 1 + d(j+1) and 2·112 paid jobs of rank d(j+1); +- (p+2) units; +- 112(p-1) queries. + +The event-word join and the closed form agree exactly. Their common value equals: + +- `RESULT.json` targets/paid; +- `NATIVE.json.gz` helpers/paid, times the call counts; +- `CONTROLLER.json`'s embedded invoice after replacing 18 THREE-base units by 18 new units; +- #4478's literals `T` and `P`. + +## 3. Enclosure + +For integer k ≥ 1 and rational t ≥ 0, k^t = exp(t ln k). Decimal `ln` and `exp` are documented +as correctly rounded at the working precision (60 digits). Each returned value v is widened to +[v - |v|·10⁻²⁰, v + |v|·10⁻²⁰]. Rationals are converted to [floor, ceiling] decimal quotients. +Products of nonnegative intervals, sums and quotients are rounded outward with `ROUND_FLOOR` / +`ROUND_CEILING` contexts. exp is increasing, so exp evaluated at the interval endpoints encloses +the image. + +Then M_H(t) = Σ n_k k^t is enclosed for each histogram H. The surplus lower bound is +M_T,lo − M_P,hi, and the upper bound is M_T,hi − M_P,lo. The tails are enclosed from above by +using upper bounds in numerators and lower bounds in denominators: + +- α = M_P(t)/M_T(t); +- γ = M_P(t+1/5)/(20^{1/5} M_T(t)); +- δ = 21·|T|/(20^{C} M_T(t)), where t = 1 − C and C = 0.003020155. + +The exact rational facts (97/100)^128 < 1/16 and 1/(1 + 1024·10⁻⁹) + 4/2³² < 1 are checked in +`Fraction`. + +## 4. Sharpness + +The rank-one moment is 1^t = 1 for every t. The certified upper bounds of the raw surplus at +κ and at the tested saving are below 1. Adding any single rank-one paid job therefore makes +both surpluses negative, and the verifier asserts this bound. diff --git a/research/pr4470-invoice-join/README.md b/research/pr4470-invoice-join/README.md new file mode 100644 index 0000000000..f968ab9c49 --- /dev/null +++ b/research/pr4470-invoice-join/README.md @@ -0,0 +1,152 @@ +# Independent join of the selected #4470 p16 invoice to its moment bill + +**Independent verification; no new κ.** This covers the selected record, +[#4470](https://github.com/CrocSwap/integer-mult-bounds/pull/4470) (Cinna Davis / 1337isnot1337, +conditional κ = 60403/20000000 = 0.00302015). It joins two parts that were already independently +derived, the per-call local unit and the p16 controller word, into the complete target/paid histogram. +It then checks that histogram against the moment and tail inequalities at the selected κ, using a +different enclosure method. The verifier is separately written and imports no checker. + +Base `cef4b52f2a59009865bf8eabde1be3f159063703`, priority revision 7. +Claim: [#1166 comment 19137480](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19137480). + +## Coverage before this package + +| Piece of #4470's changed ledger | Independent coverage | +| --- | --- | +| Local unit: helpers `{4:28, 7:7, 8:47, 9:326}`, paid `{1:2237, 2:388, 3:494, 4:147, 5:36, 8:8}` | #4504 frame audit (Mihir Srivastava), both orientations | +| p16 Laurent factorization and main/idle/thin charges | `research/pr4470-controller-replay` (Ryanson Jonathan) | +| Changed transport recipes | `research/pr4470-coverage-join` (Clear1nsight) | +| Root, tails, compiler and outer rows **on a hard-coded histogram** | #4478 (Ryanson Jonathan), whose `T`/`P` literals are "as printed in #4470" | +| **Complete p16 histogram = controller bill + 18 local units** | author code only (`joint-helper-lattice/verify.py`) | +| **Moment/tail inequalities on a source-derived histogram** | author code only | + +The two bold rows are the gap. #4478 never reads `CONTROLLER.json` or the local unit. +`CONTROLLER.json`'s own `invoice` uses the older THREE-base unit (69,012 jobs). Only the +author's substitution step produced the 64,620-job histogram that everyone evaluates. + +## Result + +**A. Join (exact).** One pass over the 154 committed events gives the following. Full native calls sit +at exactly the 18 thick stages `{0, 32, 1, 3, …, 31}`: 2 forward and 16 backward. Paid query shears sit +at exactly the 15 thin stages. The 15 IDLE windows multiply only distinct thick stages. The 32 diagonal +outputs have central exponent ±1 and no thin-stage credit. The bill is charged as follows: + +- each full call gets #4504's unit for its own orientation, plus one fresh copy of the 408 helpers; +- each query shear gets 112 rank-one jobs; +- each IDLE window gets 2·112 jobs of rank 8·|stages|; +- each diagonal output gets 112 targets of rank 1 + 8·|stages|. + +The result is: + +```text +targets {4:504, 7:126, 8:846, 9:5868, 17..65 step 8: 448 each, 73:224, 145:224} 10,928 fields, mass 239,886 +paid {1:41946, 2:6984, 3:8892, 4:2646, 5:648, 8:144, 16..64 step 8: 448 each, 72:224} 64,620 jobs, mass 239,134 +``` + +The same histogram comes out of all six sources below, exactly: + +1. this event-word join; +2. the #4440 closed form (PROOF.md §2, with no event word); +3. `RESULT.json`; +4. `NATIVE.json.gz`'s unit, times the call counts; +5. `CONTROLLER.json`'s embedded invoice, with the THREE-base unit replaced by the new one; +6. #4478's `T`/`P` literals (read with `ast`, never executed). + +**B. Moment and tails (second method).** The verifier uses Python `decimal` at 60 digits with +directed rounding. It widens every correctly rounded `ln`/`exp` by 10⁻²⁰ relative, which is far +more than one ulp. This is a different method from the Fraction atanh/Taylor series used by #4470 +and #4478. Let `T_t − P_t` be the raw surplus, with `t = 1 − saving`. The results: + +| Check | Enclosure | Stated limit | +| --- | --- | --- | +| raw surplus at κ = 0.00302015 | ≥ 0.00395201766 | > 0 | +| raw surplus at tested 0.003020155 | ≥ 0.00271523544 | > 0 | +| root bracket (0.0030201659770, 0.0030201659771) | ≥ 3.86e-9 / ≤ −2.09e-8 | sign change | +| α = P_t/T_t | ≤ 0.999999988558808 | < 1 − 10⁻⁹ | +| γ = P_{t+1/5}/(20^{1/5} T_t) | ≤ 0.956176646498 | < 97/100 | +| δ = 21·10928/(20^{0.003020155} T_t) | ≤ 0.958284435309 | < 97/100 | + +These agree with #4470's and #4478's printed values. **No discrepancy was found.** + +**Sharpness (new observation).** The whole raw surplus at κ (0.00395) and at the tested saving +(0.00272) is **below the moment of one rank-one paid job** (1ᵗ = 1). The verifier asserts this. +Each of the following single-job edits flips the selected κ by itself: + +- one extra rank-one paid job; +- one rank-one job promoted to rank two; +- one rank-9 helper demoted to rank 8. + +The selected record is therefore correct only if the complete p16 invoice is exact at +single-job resolution. This is not a defect. It does mean an omitted charge of even one query, +copy or erase would invalidate κ = 0.00302015. + +## Controls + +The 15 controls below all reject, and the verifier fails if any one passes: + +- **Moment controls:** one extra rank-one job; 1→2 promotion; 9→8 helper demotion; κ moved to the + root's upper end; the #4447 local unit placed in the p16 word; the predecessor p17 invoice at κ. +- **Structural controls:** query shear dropped; query shear promoted to a full call; full call demoted + to a query; one IDLE stage removed; a diagonal output credited with a thin stage; central exponent 0. +- **Binding controls:** one backward-unit job shifted; one helper rank lowered; tampered pinned bytes. + +All 8 of 8 hand mutants of the verifier's sharp constants fail: + +- job count; α limit; port count; κ; thin charge; idle line count; γ limit; and the root upper end + moved below the root. + +## Not covered + +This package does not cover: + +- the native word, phases or helper boundaries (#4504, the coverage join and the maintainer review cover these); +- the Laurent factorization (pr4470-controller-replay covers this); +- the compiler, BIT admission, the outer ledger rows and their parameters (#4478 covers these from printed parameters); +- the physical query/owned-stream protocol. + +The cost model is taken as stated in #4440 PROOF.md §1–2 and is not re-derived: + +- 112 ports; +- fresh block rank 8; +- one unit per full call; +- a query costs one rank-one job per port; +- idle costs 2·112 jobs of rank 8·|stages|; +- a main output has rank 1 + 8·|stages|. + +The decimal enclosure assumes Python's documented correct rounding of `Decimal.ln`/`exp`, with +10²⁰-ulp slack. This is a finite certificate for one fixed histogram. It is not a theorem about +the multiplication algorithm and not a new κ. + +## Reproduce + +```sh +python3 scripts/research_package.py --package research/pr4470-invoice-join --check-only +python3.12 -B scripts/research_package.py --package research/pr4470-invoice-join +python3.12 -O -B research/pr4470-invoice-join/verify.py +python3.12 -I -W error -B research/pr4470-invoice-join/verify.py +``` + +The verifier prints `PASS_PR4470_INVOICE_JOIN` in under a second, using only the standard library. +`PROOF.md` states the charging rules and the enclosure argument. + +## Open next questions + +1. **Single-job completeness of the p16 invoice.** The surplus at κ is below one rank-one job, so is + every paid operation of a thin query shear and an IDLE window charged exactly once? + *First step:* enumerate one query shear's per-port copy/query/add/erase steps from #4440's protocol. + Match each step to a histogram entry or to an explicit nonrecursive allowance. +2. **Stage-zero unit.** All 18 full calls, including stage 0 (multiplier F9·Q⁻¹), are charged the same + #4504 unit, following #4440/#4470. *First step:* compare the stage-zero call's frame audit with the + generic unit. + +Structured versions are in `TASK.json`. + +## Credit + +- Construction and claim: Cinna Davis / 1337isnot1337 (#4470, #4440, #4441, #4447). zxv supplied the native/controller lineage. +- Local unit audit: Mihir Srivastava (#4504). Arithmetic audit and controller replay: Ryanson Jonathan (#4478, pr4470-controller-replay). Coverage join: Clear1nsight. +- Maintainer review: docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md. + +Prepared by JoyboyBrian with substantial assistance from Anthropic Claude (Claude Code, Opus 5.5). +This is not independent human or formal review. Apache-2.0. diff --git a/research/pr4470-invoice-join/SOURCES.json b/research/pr4470-invoice-join/SOURCES.json new file mode 100644 index 0000000000..4dd22d0001 --- /dev/null +++ b/research/pr4470-invoice-join/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + }, + { + "path": "research/joint-helper-lattice/NATIVE.json.gz", + "usage": "input", + "git_blob": "0910f74138decf498e7fc445cc2daff4390169d6", + "sha256": "74582cce642c80f0235be7fcbce3716174666326ac6a1d46d02a62a75d7be4c6" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/missing-join-frame/RESULT.json", + "usage": "input", + "git_blob": "e653fb4358ded67ff1539151f4b670ad9a242fb1", + "sha256": "25f2cbcde988847ff86f44e804982069863ec99ff68097f16e9bb7a1a17c4cd0" + }, + { + "path": "research/pr4470-arithmetic-check/verify.py", + "usage": "input", + "git_blob": "629964628fdf5d5695cfd56e0c7bdd69beea5010", + "sha256": "eefdc2a1b6ca98d04ecd543428231d2a6ca48090477068d76d5038ea3bd5a09d" + }, + { + "path": "research/pr4470-controller-replay/SOURCES.json", + "usage": "input", + "git_blob": "3df53e9984de185eae263858196da6ecba3e38ca", + "sha256": "5d00952f3c969027a04ebcf912d18cc32644e885e39361b00c3d367c21b2dc44" + }, + { + "path": "research/pr4470-frame-audit/RESULT.json", + "usage": "input", + "git_blob": "423d1bbe38023d34419082492bac38b29a80850c", + "sha256": "9eae5428e0d083a80c4771439b888f8e559624754be71bb80c2a610ff54c10b7" + }, + { + "path": "research/pr4470-frame-audit/SOURCES.json", + "usage": "input", + "git_blob": "9124bb10fe889a583982b0f5228776c779f092bf", + "sha256": "0b2b3bebb675855bb87d2cf6318fcc45c46d2c3f23064a9e765847991bf4ce5f" + } + ] +} diff --git a/research/pr4470-invoice-join/TASK.json b/research/pr4470-invoice-join/TASK.json new file mode 100644 index 0000000000..d58fc628d0 --- /dev/null +++ b/research/pr4470-invoice-join/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "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": "Independent source-bound join of the selected #4470 p16 complete invoice: CONTROLLER.json event word and diagonal plus the #4504 per-orientation local unit, bound to RESULT.json, NATIVE.json.gz, the embedded controller invoice and #4478's hard-coded histogram; second-method (decimal, directed rounding) enclosure of the raw surplus at the selected kappa and tested saving, the root bracket and the three completion tails.", + "scope_change_reason": "The card's starting examples (#4088/#4091/#4067) predate the selected record. The selected change is #4470. Its local unit (#4504), controller Laurent word (pr4470-controller-replay) and arithmetic on a hard-coded histogram (#4478) are independently covered; no non-author code joined the two derived parts into the histogram that #4478 evaluates.", + "bottleneck_link": "Independent pricing of the selected record: the raw surplus at kappa is below one rank-one job, so the frontier depends on the complete histogram being exact at single-job resolution.", + "budget_minutes": 150, + "stop_rule": "Stop at the complete p16 histogram and its moment/tail inequalities at kappa and the tested saving. No native, Laurent, compiler or outer-theorem replay.", + "outcome": "completed", + "evidence": "verify.py prints PASS_PR4470_INVOICE_JOIN: 18 full calls (2 forward, 16 backward), 15 query shears; 10,928 fields, 64,620 jobs, masses 239,886/239,134 agree across the event-word join, the #4440 closed form, RESULT.json, NATIVE.json.gz, the embedded controller invoice and #4478's literals. Raw surplus lower bounds 0.0039520 at kappa and 0.0027152 at tested; alpha < 0.999999988558809, gamma < 0.956176646498, delta < 0.958284435310. 15 controls reject; 8 of 8 verifier mutants fail.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)", + "open_questions": [ + { + "question": "Is every rank-one paid job of the p16 invoice physically present, with no uncharged operation omitted, at single-job resolution?", + "why_it_matters": "The raw surplus at kappa is 0.00395 of one rank-one job and the alpha headroom is about 1e-8 against about 4e-6 per job: one missing charge anywhere (copy, query, owned-stream erase, center) would invalidate the selected kappa.", + "first_step": "Enumerate the per-port operations of one thin query shear and one IDLE window from the #4440 owned-stream protocol and match each to a charged histogram entry or an explicit nonrecursive allowance.", + "blocked_by": "Requires the physical query/owned-stream contract, an inherited premise outside this ledger join." + }, + { + "question": "Is the uniform per-call unit correct for the stage-zero full call, whose multiplier is the nine-axis F9 Q^-1 rather than a fresh eight-axis D_s?", + "why_it_matters": "This join charges the same #4504 unit at all 18 thick stages, following #4440/#4470; a stage-zero-specific unit would change the histogram.", + "first_step": "Locate the stage-zero native call in the #4470 word and compare its frame audit with the generic unit.", + "blocked_by": "None; the stage-zero commutation audits cover operators, not the per-call bill." + } + ] +} diff --git a/research/pr4470-invoice-join/VERIFY.json b/research/pr4470-invoice-join/VERIFY.json new file mode 100644 index 0000000000..15f5d8c0c1 --- /dev/null +++ b/research/pr4470-invoice-join/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/joint-helper-lattice/CONTROLLER.json", + "research/joint-helper-lattice/NATIVE.json.gz", + "research/joint-helper-lattice/RESULT.json", + "research/missing-join-frame/RESULT.json", + "research/pr4470-arithmetic-check/verify.py", + "research/pr4470-controller-replay/SOURCES.json", + "research/pr4470-frame-audit/RESULT.json", + "research/pr4470-frame-audit/SOURCES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source-pinned join of #4470's complete p16 histogram from CONTROLLER.json events/diagonal and #4504's per-orientation local unit; equality with the #4440 closed form, RESULT.json, NATIVE.json.gz, the embedded controller invoice and #4478's hard-coded T/P (10,928 fields, 64,620 jobs, masses 239,886/239,134). Decimal directed-rounding enclosure: positive raw surplus at kappa 60403/20000000 and tested 0.003020155, root bracket, alpha/gamma/delta below 1-1e-9, 97/100, 97/100; surplus below one rank-one job. Fifteen rejection controls (one extra or shifted job, wrong unit, predecessor invoice, dropped/promoted/demoted calls, idle and diagonal edits, tampered bytes)." + } + ] +} diff --git a/research/pr4470-invoice-join/verify.py b/research/pr4470-invoice-join/verify.py new file mode 100644 index 0000000000..07d6a49483 --- /dev/null +++ b/research/pr4470-invoice-join/verify.py @@ -0,0 +1,381 @@ +#!/usr/bin/env python3 +"""Independent join of the selected #4470 p16 invoice to its independently derived parts. + +Separately written; imports no checker. It (A) rebuilds the complete p16 target/paid +histogram from the committed CONTROLLER.json event word and the per-orientation local +profile derived by the #4504 frame audit, with a closed-form third derivation from the +#4440 controller formula, and binds it to RESULT.json, NATIVE.json.gz, the embedded +controller invoice and #4478's hard-coded histogram; (B) encloses the raw moment surplus +and the three completion tails with decimal arithmetic under directed rounding (a +different method from the Fraction series used by #4470 and #4478); (C) runs semantic +rejection controls. JoyboyBrian with substantial Claude Code assistance. Apache-2.0. +""" +import ast +import copy +import decimal +import gzip +import hashlib +import json +import sys +from collections import Counter +from decimal import Decimal as D +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +JOINT = 'research/joint-helper-lattice/' + +# Model constants of the #4440 complex controller (PROOF.md section 2), not read from code: +# 112 ports, fresh block rank 8, p = 16 pairs, prefix a = 7, 2p+1 = 33 local stages. +PORTS, BLOCK, PAIRS, PREFIX = 112, 8, 16, 7 +STAGES = 2 * PAIRS + 1 +THICK = frozenset({0, 2 * PAIRS, *range(1, 2 * PAIRS, 2)}) +# THREE-base unit embedded in CONTROLLER.json's generic invoice (#4440 PROOF.md section 1). +THREE_HELPERS = {5: 28, 6: 18, 7: 56, 8: 93, 9: 213} +THREE_PAID = {1: 2487, 2: 713, 3: 224, 4: 102, 5: 20, 8: 8} +# Values stated in docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md. +REVIEW = {'kappa': Q(60403, 20000000), 'tested': Q(3020155, 10 ** 9), 'cutoff': 20, + 'floor': 21, 'offset': Q(1, 5), 'root': (Q(30201659770, 10 ** 13), Q(30201659771, 10 ** 13)), + 'fields': 10928, 'paid_jobs': 64620, 'target_mass': 239886, 'paid_mass': 239134} +LIMITS = {'alpha': 1 - Q(1, 10 ** 9), 'gamma': Q(97, 100), 'delta': Q(97, 100)} + +PREC = 60 # working digits +SLACK = 40 # every ln/exp value is widened by 10^-(PREC-SLACK) relative, far beyond 1 ulp + + +class Reject(Exception): + pass + + +def need(ok, why): + if not ok: + raise Reject(why) + + +# ---------------------------------------------------------------- source binding + +def blob(data): + return hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() + + +def load_inputs(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + data = {} + for row in pins['files']: + if row['usage'] != 'input': + continue + rel = Path(row['path']) + need(not rel.is_absolute() and '..' not in rel.parts, 'canonical input path') + raw = (ROOT / rel).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'sha256 pin: ' + row['path']) + need(blob(raw) == row['git_blob'], 'git blob pin: ' + row['path']) + data[row['path']] = raw + return data + + +def as_json(raw, gz=False): + return json.loads(gzip.decompress(raw) if gz else raw) + + +def hist(d): + return {int(k): int(v) for k, v in d.items()} + + +def literal_dict(source, name): + """Module-level `name = {...}` literal from a Python file, read as data (never executed).""" + found = [n.value for n in ast.parse(source).body if isinstance(n, ast.Assign) + and any(isinstance(t, ast.Name) and t.id == name for t in n.targets)] + need(len(found) == 1, 'one literal ' + name) + return hist(ast.literal_eval(found[0])) + + +# ---------------------------------------------------------------- A. invoice join + +def controller_charges(ctrl): + """Walk the emitted word once; return per-orientation full calls and the controller-only bill.""" + need((ctrl['kind'], ctrl['pairs'], ctrl['prefix_pairs'], ctrl['ambient_rank']) + == ('complex', PAIRS, PREFIX, 1 + BLOCK * len(THICK)), 'controller parameters') + full = {'forward': [], 'backward': []} + thin, idle_paid, main = [], Counter(), Counter() + for ev in ctrl['physical_events']: + op = ev[0] + if op == 'LOCAL': + _, stage, pair, backward = ev + need(stage in THICK and 0 <= pair < PAIRS and isinstance(backward, bool), 'full call at a thick stage') + full['backward' if backward else 'forward'].append(stage) + elif op == 'QUERY_SHEAR': + _, stage, pair, backward = ev + need(0 <= stage < STAGES and stage not in THICK and 0 <= pair < PAIRS, 'query shear at a thin stage') + thin.append(stage) + elif op == 'IDLE': + _, pair, stages = ev + need(0 <= pair < PAIRS and stages and len(set(stages)) == len(stages) and set(stages) <= THICK, + 'idle multiplies only distinct thick stages') + idle_paid[BLOCK * len(stages)] += 2 * PORTS # both lines of the pair, every port + elif op in ('ADD', 'SIGNED_SWAP', 'SWAP'): + pass # scalar bridge: no rank charge + else: + raise Reject('unknown event ' + str(op)) + calls = sorted(full['forward'] + full['backward']) + need(calls == sorted(THICK), 'exactly one full native call per thick stage') + need(sorted(thin) == sorted(set(range(STAGES)) - THICK), 'exactly one paid query shear per thin stage') + need(len(ctrl['diagonal']) == 2 * PAIRS, 'one diagonal output per line') + for term in ctrl['diagonal']: + need(len(term) == 1 + STAGES and term[0] in (-1, 1), 'central Gaussian exponent is +-1') + need(all(x in (0, 1) for x in term[1:]), 'stage exponents are 0/1') + support = {s for s in range(STAGES) if term[1 + s]} + need(support <= THICK, 'no main output is credited for a thin stage') + main[1 + BLOCK * len(support)] += PORTS + return full, len(thin), main, idle_paid + + +def join(ctrl, frame): + """Complete p16 histogram: controller bill + one fresh local unit per full call.""" + full, thin, main, idle_paid = controller_charges(ctrl) + new = frame['profiles']['new'] + helpers = hist(new['helpers']) + targets, paid = Counter(main), Counter(idle_paid) + paid[1] += PORTS * thin + for orientation, stages in full.items(): + unit = hist(new[orientation]['paid']) + need(new[orientation]['owned_center_jobs'] == unit.get(8, 0) == 8, 'eight rank-8 owned center jobs charged') + for _ in stages: + targets.update(helpers) + paid.update(unit) + return {'targets': dict(targets), 'paid': dict(paid), 'main': dict(main), 'idle': dict(idle_paid), + 'full_forward': len(full['forward']), 'full_backward': len(full['backward']), 'thin': thin, + 'helpers': helpers, 'unit_paid': {o: hist(new[o]['paid']) for o in full}} + + +def formula(helpers, unit): + """#4440 PROOF.md section 2 closed form, with no reference to the event word.""" + p, a, d, v = PAIRS, PREFIX, BLOCK, PORTS + targets, paid = Counter({1 + d * (p + 2): 2 * v}), Counter() + for j in list(range(1, a + 1)) + list(range(1, p - a)): + targets[1 + d * (j + 1)] += 2 * v + paid[d * (j + 1)] += 2 * v + for _ in range(p + 2): + targets.update(helpers) + paid.update(unit) + paid[1] += v * (p - 1) + return dict(targets), dict(paid) + + +def bind(inp): + """All cross-bindings of the joined histogram against committed sources.""" + ctrl = as_json(inp[JOINT + 'CONTROLLER.json']) + frame = as_json(inp['research/pr4470-frame-audit/RESULT.json']) + result = as_json(inp[JOINT + 'RESULT.json']) + native = as_json(inp[JOINT + 'NATIVE.json.gz'], gz=True) + j = join(ctrl, frame) + T, P = j['targets'], j['paid'] + need(j['unit_paid']['forward'] == j['unit_paid']['backward'], 'both orientations carry one local paid profile') + unit = j['unit_paid']['forward'] + need(formula(j['helpers'], unit) == (T, P), 'event-word join equals the #4440 closed form') + need(sum(T.values()) == REVIEW['fields'] and sum(P.values()) == REVIEW['paid_jobs'], 'field and job counts') + need(sum(r * n for r, n in T.items()) == REVIEW['target_mass'], 'target rank mass') + need(sum(r * n for r, n in P.items()) == REVIEW['paid_mass'], 'paid rank mass') + need((hist(result['targets']), hist(result['paid'])) == (T, P), 'RESULT.json histogram') + need((result['full_calls'], result['query_shears']) == (j['full_forward'] + j['full_backward'], j['thin']), + 'RESULT.json call counts') + need((hist(result['local_helpers']), hist(result['local_paid'])) == (j['helpers'], unit), 'RESULT.json local unit') + need((hist(native['helpers']), hist(native['paid'])) == (j['helpers'], unit), 'NATIVE.json.gz receipt') + src = inp['research/pr4470-arithmetic-check/verify.py'].decode() + need((literal_dict(src, 'T'), literal_dict(src, 'P')) == (T, P), '#4478 evaluated exactly this histogram') + inv = ctrl['invoice'] + need(hist(inv['main']) == j['main'], 'embedded controller main targets') + calls = j['full_forward'] + j['full_backward'] + embedded = Counter(hist(inv['paid'])) + embedded.subtract({r: calls * n for r, n in THREE_PAID.items()}) + embedded.update({r: calls * n for r, n in unit.items()}) + need(+embedded == Counter(P), 'embedded THREE-base invoice with the new unit substituted') + need((inv['productive_fields'], inv['rank_surplus']) == (REVIEW['fields'], REVIEW['target_mass'] - REVIEW['paid_mass']), + 'embedded field count and surplus') + old = Counter(hist(inv['paid'])) + need(sum(old.values()) == inv['paid_calls'], 'embedded THREE-base paid count') + sel = as_json(inp['certificates/selected-result.json']) + need(Q(sel['kappa']) == REVIEW['kappa'] == Q(result['kappa']), 'selected kappa') + st = result['strictification'] + need((Q(st['tested']), st['cutoff'], st['floor'], Q(st['tail_offset']), st['power']) + == (REVIEW['tested'], REVIEW['cutoff'], REVIEW['floor'], REVIEW['offset'], 1024), 'tail parameters') + pred = as_json(inp['research/missing-join-frame/RESULT.json']) + return j, (hist(pred['targets']), hist(pred['paid'])), frame + + +# ---------------------------------------------------------------- B. decimal enclosures + +CTX = decimal.Context(prec=PREC, Emax=10 ** 6, Emin=-10 ** 6, traps=[decimal.InvalidOperation, decimal.DivisionByZero]) +FLOOR = CTX.copy() +FLOOR.rounding = decimal.ROUND_FLOOR +CEIL = CTX.copy() +CEIL.rounding = decimal.ROUND_CEILING +REL = D(10) ** -(PREC - SLACK) + + +def dec(x): + """Rational -> enclosing decimal interval.""" + x = Q(x) + return FLOOR.divide(D(x.numerator), D(x.denominator)), CEIL.divide(D(x.numerator), D(x.denominator)) + + +def widen(v): + e = CEIL.multiply(abs(v), REL) + return FLOOR.subtract(v, e), CEIL.add(v, e) + + +def ln_iv(k): + return widen(CTX.ln(D(k))) if k != 1 else (D(0), D(0)) + + +def mul_pos(a, b): + need(a[0] >= 0 and b[0] >= 0, 'nonnegative interval product') + return FLOOR.multiply(a[0], b[0]), CEIL.multiply(a[1], b[1]) + + +def pow_iv(k, t): + """k^t for integer k >= 1 and rational t >= 0: exp(t ln k), exp monotone.""" + x = mul_pos(dec(t), ln_iv(k)) + return widen(CTX.exp(x[0]))[0], widen(CTX.exp(x[1]))[1] + + +def moment(h, t): + lo = hi = D(0) + for k, n in h.items(): + p = pow_iv(k, t) + lo, hi = FLOOR.add(lo, FLOOR.multiply(D(n), p[0])), CEIL.add(hi, CEIL.multiply(D(n), p[1])) + return lo, hi + + +def surplus(T, P, saving): + """Enclosure of T_t - P_t at t = 1 - saving.""" + t = 1 - Q(saving) + a, b = moment(T, t), moment(P, t) + return FLOOR.subtract(a[0], b[1]), CEIL.subtract(a[1], b[0]) + + +def tails(T, P, tested, u, c, b): + t = 1 - Q(tested) + target = moment(T, t) + alpha = CEIL.divide(moment(P, t)[1], target[0]) + gamma = CEIL.divide(moment(P, t + u)[1], FLOOR.multiply(pow_iv(c, u)[0], target[0])) + delta = CEIL.divide(D(b * sum(T.values())), FLOOR.multiply(pow_iv(c, Q(tested))[0], target[0])) + return {'alpha': alpha, 'gamma': gamma, 'delta': delta} + + +def moment_checks(T, P, kappa=REVIEW['kappa']): + out = {'kappa': surplus(T, P, kappa), 'tested': surplus(T, P, REVIEW['tested']), + 'root_low': surplus(T, P, REVIEW['root'][0]), 'root_high': surplus(T, P, REVIEW['root'][1])} + need(out['kappa'][0] > 0, 'positive raw surplus at the selected kappa') + need(out['tested'][0] > 0, 'positive raw surplus at the tested saving') + need(out['root_low'][0] > 0 and out['root_high'][1] < 0, 'raw root inside the stated bracket') + tl = tails(T, P, REVIEW['tested'], REVIEW['offset'], REVIEW['cutoff'], REVIEW['floor']) + for name, value in tl.items(): + need(value < dec(LIMITS[name])[0], name + ' below its stated limit') + need(Q(97, 100) ** 128 < Q(1, 16), 'decay block (97/100)^128 < 1/16') + need(1 / (1 + 1024 * Q(1, 10 ** 9)) + Q(4, 2 ** 32) < 1, 'normalized paid bound below one') + return out, tl + + +# ---------------------------------------------------------------- C. controls + +def rejects(fn): + try: + fn() + except Reject as e: + return str(e) + raise Reject('control was not rejected') + + +def controls(inp, j, pred, frame): + T, P = j['targets'], j['paid'] + ctrl = as_json(inp[JOINT + 'CONTROLLER.json']) + out = {} + + def bumped(h, src, dst, n=1): + h = Counter(h) + h[src] -= n + h[dst] += n + return dict(+h) + + out['one_extra_rank1_paid_job'] = rejects(lambda: moment_checks(T, dict(Counter(P) + Counter({1: 1})))) + out['one_paid_rank1_job_promoted_to_rank2'] = rejects(lambda: moment_checks(T, bumped(P, 1, 2))) + out['one_productive_rank9_helper_demoted_to_rank8'] = rejects(lambda: moment_checks(bumped(T, 9, 8), P)) + out['kappa_at_root_upper_end'] = rejects(lambda: moment_checks(T, P, REVIEW['root'][1])) + out['predecessor_p17_invoice_at_selected_kappa'] = rejects(lambda: need(surplus(*pred, REVIEW['kappa'])[0] > 0, 'predecessor surplus')) + old = copy.deepcopy(frame) + old['profiles']['new'] = old['profiles']['old'] + oj = join(ctrl, old) + out['pr4447_local_unit_in_p16'] = rejects(lambda: moment_checks(oj['targets'], oj['paid'])) + + def mutate(edit): + bad = copy.deepcopy(inp) + c = as_json(bad[JOINT + 'CONTROLLER.json']) + edit(c) + bad[JOINT + 'CONTROLLER.json'] = json.dumps(c).encode() + return lambda: bind(bad) + + def first(c, op): + return next(i for i, e in enumerate(c['physical_events']) if e[0] == op) + + out['query_shear_dropped'] = rejects(mutate(lambda c: c['physical_events'].pop(first(c, 'QUERY_SHEAR')))) + out['query_shear_promoted_to_full_call'] = rejects(mutate(lambda c: c['physical_events'][first(c, 'QUERY_SHEAR')].__setitem__(0, 'LOCAL'))) + out['full_call_demoted_to_query'] = rejects(mutate(lambda c: c['physical_events'][first(c, 'LOCAL')].__setitem__(0, 'QUERY_SHEAR'))) + out['idle_stage_removed'] = rejects(mutate(lambda c: c['physical_events'][first(c, 'IDLE')][2].pop())) + out['main_output_credited_thin_stage'] = rejects(mutate(lambda c: c['diagonal'][0].__setitem__(1 + 2, 1))) + out['central_exponent_zero'] = rejects(mutate(lambda c: c['diagonal'][0].__setitem__(0, 0))) + + def frame_edit(edit): + bad = copy.deepcopy(inp) + f = as_json(bad['research/pr4470-frame-audit/RESULT.json']) + edit(f['profiles']['new']) + bad['research/pr4470-frame-audit/RESULT.json'] = json.dumps(f).encode() + return lambda: bind(bad) + + def shift_backward(n): + p = n['backward']['paid'] + p['1'] -= 1 + p['2'] += 1 + out['backward_unit_one_job_shifted'] = rejects(frame_edit(shift_backward)) + out['helper_unit_one_rank_lowered'] = rejects(frame_edit(lambda n: n['helpers'].update({'9': 325, '8': 48}))) + out['tampered_pinned_bytes'] = rejects(lambda: need(hashlib.sha256(inp[JOINT + 'CONTROLLER.json'] + b' ').hexdigest() + == hashlib.sha256(inp[JOINT + 'CONTROLLER.json']).hexdigest(), 'sha256 pin')) + return out + + +def show(x, digits=15): + return format(x, '.%dg' % digits) + + +def main(): + inp = load_inputs() + j, pred, frame = bind(inp) + T, P = j['targets'], j['paid'] + margins, tl = moment_checks(T, P) + # Sharpness: the whole raw surplus at kappa and at the tested saving is below one rank-one job (1^t = 1). + need(margins['kappa'][1] < 1 and margins['tested'][1] < 1, 'raw surplus below one rank-one paid job') + ctl = controls(inp, j, pred, frame) + print(json.dumps({ + 'status': 'PASS_PR4470_INVOICE_JOIN', + 'join': {'full_calls': {'forward': j['full_forward'], 'backward': j['full_backward']}, + 'query_shears': j['thin'], 'targets': dict(sorted(T.items())), 'paid': dict(sorted(P.items())), + 'productive_fields': sum(T.values()), 'paid_jobs': sum(P.values()), + 'rank_masses': [sum(r * n for r, n in T.items()), sum(r * n for r, n in P.items())]}, + 'bindings': ['CONTROLLER.json events and diagonal', '#4504 RESULT.json per-orientation unit', + '#4440 closed form', 'RESULT.json', 'NATIVE.json.gz', 'CONTROLLER.json embedded invoice', + '#4478 hard-coded T and P', 'selected kappa and tail parameters'], + 'raw_surplus_lower': {k: show(v[0]) for k, v in margins.items() if k != 'root_high'}, + 'raw_surplus_upper_at_root_high': show(margins['root_high'][1]), + 'sharpness': 'raw surplus at kappa and at the tested saving is below 1 = the moment of one rank-one paid job', + 'tails_upper': {k: show(v) for k, v in tl.items()}, + 'enclosure': 'decimal, %d digits, directed rounding, ln/exp widened by 10^-%d relative' % (PREC, PREC - SLACK), + 'rejected_controls': ctl, + 'new_kappa_claimed': False}, indent=1)) + + +if __name__ == '__main__': + try: + main() + except Reject as e: + print('FAIL_PR4470_INVOICE_JOIN: ' + str(e)) + sys.exit(1)