diff --git a/research/qq16-consumer-budget-independent/PREDECESSORS.json b/research/qq16-consumer-budget-independent/PREDECESSORS.json new file mode 100644 index 0000000000..ecac65f581 --- /dev/null +++ b/research/qq16-consumer-budget-independent/PREDECESSORS.json @@ -0,0 +1,53 @@ +{ + "audited_pr": 3908, + "head": "0d8880e38ed7c88d70eec6a48e5aa829d0fb22f3", + "author": "1337isnot1337", + "archive_sha256": "9ccaf27da52f96a5701d8d7f9e9934a64f8bbc15f0aa12bd45c7168785d6966d", + "files": [ + { + "path": "research/qq16-consumer-cap-audit/PR3181-README.md.gz", + "sha256": "c9ebe8149ff8cc0dc4f67bc52fd6bef822ba99a8a803bbddba0eb99c032cedde", + "git_blob": "14779caff5262387a6fb42e284f94524b8c66550" + }, + { + "path": "research/qq16-consumer-cap-audit/README.md", + "sha256": "b62dfba1a486ee0e28d799abe0c95f0a72e1942fd9ddcf2ed51c0ead780f579e", + "git_blob": "d4606ff57f84566b1fd586dd02a192d66d9da895" + }, + { + "path": "research/qq16-consumer-cap-audit/SOURCES.json", + "sha256": "d48c7151a4553351d4f9de58eaa39f5660591fb3a84edc4aee3978bdefec2323", + "git_blob": "a7d38c77808c4f43c43db4c948af1d3a623f3f44" + }, + { + "path": "research/qq16-consumer-cap-audit/TARGET.json", + "sha256": "b11729b374a14775c754ff561f52ab48562a4c12ea1e5303e3829ec15cebf1c3", + "git_blob": "750e72bdb5709a9b41993c12948729374faac38c" + }, + { + "path": "research/qq16-consumer-cap-audit/TASK.json", + "sha256": "1c9c1ca540312c72ff27ffbfbb17e3306e4195da7f9ff254c508ada1efb3cc07", + "git_blob": "c869052a9e86d9314442c64c1213476fa7d6a867" + }, + { + "path": "research/qq16-consumer-cap-audit/VERIFY.json", + "sha256": "021f6f76b07a0c96cbc6d870bdd8a44de61b0dc9d726b483731fe0417ab79544", + "git_blob": "37caf50e7cbcec733ddfde93f6a3a55b4096f91e" + }, + { + "path": "research/qq16-consumer-cap-audit/verify.py", + "sha256": "30ce90d9d0a8d6bda4341ebfc26a2dbcd0fbf60170e50a010ccbad4ce54274a9", + "git_blob": "dd6c8b9f123e85da984edfc847bb40469d0cc555" + } + ], + "caller_pr": 3932, + "caller_head": "12c324c576821f78070627c5eeb684d03704e20e", + "credit": [ + "Ali Romman and QQ16/native lineage", + "Douglas Colkitt and coverage-ceiling lineage", + "ywz65 PR2707", + "dcharb78 PR3181", + "Nick Petalas producer/decoder numerical lineage", + "Chris R / Clear1nsight with substantial OpenAI assistance" + ] +} diff --git a/research/qq16-consumer-budget-independent/PROOF.md b/research/qq16-consumer-budget-independent/PROOF.md new file mode 100644 index 0000000000..c25fa4e29c --- /dev/null +++ b/research/qq16-consumer-budget-independent/PROOF.md @@ -0,0 +1,254 @@ +# A caller-bound audit of the QQ16 consumer budget + +Chris R / Clear1nsight, with substantial OpenAI assistance. Apache-2.0. +This is an ordinary scoped proof and executable rational certificate, not +human review, proof-kernel verification or supplier admission. + +## 1. Audited claim and independent source binding + +The audited PR3908 head is +`0d8880e38ed7c88d70eec6a48e5aa829d0fb22f3`, by 1337isnot1337. +It checks the consumer-budget branch of dcharb78's PR3181, not its +dynamic-range, adjoint or grid theorems. The canonical baseline is +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. + +The original seven-file package is retained byte-for-byte in +`vendor/PR3908.tar.gz`, with per-file Git blob/SHA256 identities in +PREDECESSORS.json. Its original attribution and limitations are retained. +The regression suite authenticates and replays that exact executable in a +temporary source export. The independent calculation imports neither that +executable nor `ceiling.py`. + +Unlike a check of reported profile dictionaries alone, the new checker +expands the literal `programs.F_0` and `programs.B_1_2` in the pinned +`research/joint-query/certificate.json.gz`. `retained_core` expands the named +core word; `cover_sweep` and `private_sweep` contribute their ordered bodies. +Each instruction is counted once per full-cover invocation, not multiplied +by the number of cover owners. This matches the per-call native invoice. +`climb` supplies its literal rank; `native_line` supplies its recipe rank. + +The resulting event counts are 26,099 and 27,019. Their positive child +profiles are: + +| Program | Rank 1 | Rank 2 | Rank 3 | Rank 4 | Rank 5 | Rank mass | +|---|---:|---:|---:|---:|---:|---:| +| F0 | 2,420 | 418 | 432 | 142 | 82 | 5,530 | +| B_1_2 | 2,436 | 418 | 432 | 142 | 82 | 5,546 | +| Pair average | 2,428 | 418 | 432 | 142 | 82 | 5,538 | + +The same independent census checks all 37 native cases: each of the nine F +cases has the F0 profile and each of the 28 B cases has the B_1_2 profile. +This is a count check, not 37 complete operator-correctness replays. + +They agree with CONSERVED-QQ16.json, whose payload hash also binds the exact +decompressed certificate. Independently counting the literal #2707 WORD.json +gives 3,823 instructions, including 336 signed rank-one lines and no stage +children. The source proof lowers each signed line using one positive +rank-one child and explicit monomial wrappers. Its functional equivalence +and physical realization are inherited, not re-proved by this census. + +The per-call profile with this decoder is therefore +`{1:2596,2:418,3:432,4:142,5:82}`, of mass 5,706. PR3181 additionally reports +eight rank-eight children per call. The main obstruction below drops all of +them, so their origin or necessity is not a premise of that obstruction. +The tables explicitly labelled as retaining rank eight condition on that +additional reported profile component. + +## 2. Applicability to the audited first F0 caller + +The first positive child in the same literal F0 expansion is zero-based +event 9894: + +```text +["climb","A",546,0,4,1] +``` + +Event 9895 is `L546 -= L561` in frame 4. The canonical JSON hash of the +preceding 9,894 events is +`15115954461f2cb93e2266822d82bfac1ab8de7d460ff78fcf594d21c61d2b53`, +exactly the prefix audited in PR3932, head +`12c324c576821f78070627c5eeb684d03704e20e`. +Thus our caller is inside the F0 program counted here. It is not a new +producer profile to which an unrelated histogram has been assigned. + +The implication remains conditional: if this F0 and B_1_2 are used with the +unchanged #2707 decoder and their listed paid recursive ranks, and the +centre-64 coverage/halving law is retained, the budget fails at the selected +target. Correct encoding or a faster implementation of a scalar/axis +operation does not by itself delete those recursive charges. + +Conversely, PR3884's six-tape operation is a local bit-tape implementation, +and PR3932 is an arithmetic caller audit. Neither supplies the complete +recursive invoice. A proof that direct implementation actually *replaces* +a listed recursive tariff, with all-depth costs and the complete consumer +charged, would change this model and must be assessed separately. This +obstruction does not prohibit that possibility or every physical caller. + +Changing only F/B frequencies cannot fix the screen if the decoder charge +remains 168 rank-one children per call: the most favorable all-F mixture, +still waiving rank eight, has moment in +`[1.000090397821,1.000090398426]`. All B substitutions increase it. +This does not establish the actual decoder frequency in a new global +schedule. Different reuse/frequencies must be proved and priced; the +pair-level audit is not an admission of an outer schedule. + +## 3. The conditional moment lower bound + +Fix `m=73`, `w=896/9`, `R=51`, one unpaid coordinate per family and centre +charge `c`. The inherited coverage law fixes total paid rank mass + +```text +T(c) = 72w + c. +``` + +At c=64 this is 7,232. For local profile n_r, let L=sum r*n_r and +I=T(c)-L. The outer halving guard `2R^2100009/100000. Every admissible idle packing in this fixed +model has moment above one before additional physical costs. Since the +moment is increasing in a, this model cannot support the selected saving +or a larger one. No claim about an exact cap root is needed. + +## 4. Independent exact interval construction + +PR3908 uses a positive atanh/log expansion and one-sided exponential sums. +This checker instead encloses logarithms by integration. On [1,y], +1<=y<=2, the function f(t)=1/t is convex. For a uniform partition into +1,024 panels, the composite midpoint sum is a lower bound for its integral +and the composite trapezoid sum is an upper bound. Every evaluation and +sum is rational. Reduce x>=1 by powers of two and use +`ln(x)=k*ln(2)+ln(x/2^k)`; add the corresponding enclosures. + +For 0<=l<=u<=1/2, the degree-six exponential polynomial at l is a lower +bound. At u, the first omitted term is t7=u^7/7!. All later term ratios +are at most u/8, so + +```text +exp(u) <= sum_{j=0}^6 u^j/j! + t7/(1-u/8). +``` + +All used a*ln(73/r) intervals lie in this domain; the code checks it. +Every interval is rounded outward to the dyadic grid 2^-80. Positive +coefficients, mass and division by w preserve enclosure. The decimal +endpoints in RESULT.json are rational outward bounds at 10^-12, not +floating-point calculations. Full JSON equality checks every reported +field and distinguishes booleans from integers. + +The retained PR3908 replay reproduces its output lower bound +1.000097677879937. Its centre-free lower bound being below one is only a +scope control, not evidence of a feasible supplier. Our new upper bounds +below one certify passing *relaxations*, also not supplier admission. + +## 5. Exact decoder and centre tradeoffs + +Keep the producer average fixed and let d be the total number of additional +rank-one decoder children across the two-call pair. Per-call decoder cost +is d/2. Since each added rank-one child displaces one unit of rank-51 idle +mass, G increases linearly in d with positive coefficient + +```text +[b_a(1)-b_a(51)/51] / (2w). +``` + +This allows exact integer thresholds without a search for a root: + +| Centre charge per call | Eight rank-eight children | Last integer d passing relaxation | First d excluded | +|---|---|---:|---:| +| 64 | Dropped favorably | 121 | 122 | +| 64 | Retained | 61 | 62 | +| 63 (hypothetical changed law) | Retained | 363 | 364 | + +Odd d is permitted as a fractional per-call average; an even, equal split +would restrict the passing ceilings to 120, 60 and 362. This generalization +does not affect PR3908's actual even d=336. + +Thus a decoder-only replacement under centre-64 must remove at least 215 +of 336 calls even when all rank-eight work is waived, or at least 275 with +that work retained. Merely removing two 112-call groups leaves d=112 and +still fails the retained-rank-eight test. These are budget requirements, +not decoder lower bounds or constructions. + +For the unchanged d=336 with rank eight retained, a hypothetical c=63 gives + +```text +0.999987387153 <= G <= 0.999987387763. +``` + +Its available additional normalized moment is between 0.000012612237 and +0.000012612847. Any complete replacement must fit strictly inside its +actual remaining allowance. In the very special case where the only +additional work is rank-one local children displacing idle mass, at most +27 additional children per pair pass this relaxation; 28 are excluded. +This is not a conversion rate for tape actions or physical overhead. + +## 6. Research decision and limits + +Pause expansion of the unchanged F0/B_1_2 + #2707 centre-64 recipe **as a +route to the selected target**. Its optimistic bound already fails. +Retain the Gaussian/caller results as useful local interface contributions. +Do not infer a global QQ16 or multiplication impossibility statement. + +The next budget-admissible research question is a *changed consumer +endpoint or native operator-specific identity*: can one identify real +eliminated centre work, corresponding to at least one average mass unit +per call in the aggregate coverage ledger, while retaining the required +final output and avoiding repayment beyond the allowance above? +One unit per call means two over this pair; a smaller saving can be +assessed by the same affine c-dependence. No such identity is supplied. + +The first test must specify the actual downstream F17-native demand map, +the producer output rows it reads, chronological owner/frame interval, +arbitrary dirty state and return/restoration requirements. Compose that +map with the literal decoder before proposing cancellation. A final-output +quotient or identity specific to the fixed native operators is a declared +changed premise; relabelling selected independent demands or storing the +same first transcript is not one. + +Relevant adjacent restrictions are PR2391's native first-transcript +counterexample, PR2461's owner-local repair floor, PR3120's selected +copied-demand rank floor and pending PR3873's uniform scalar-oracle and +selected coverage audits. We inspected their stated scopes, not re-proved +those theorems here; none is silently asserted for a new QQ16 endpoint. +Any proposed escape must name its difference from those contracts. + +If no named consumer supplies the saving, stop at this handoff. If the +changed contract passes its complete budget, the next implementation slice +is the already identified L546 child-plus-ADD with actual tape intervals, +entry grid/range, monomials, movement/address/control and eventual return +charged. Local bit counts cannot be inserted into this recursive moment +without a justified transfer. Unknown costs remain unknown. + +The complete native/bridge algebra, decoder correctness, global coverage +realization, huge all-depth payload execution, physical hosting/routing, +precision/restoration admission, F17 consumer and selected full cold replay +remain inherited or unrun. No frontier record is changed. diff --git a/research/qq16-consumer-budget-independent/README.md b/research/qq16-consumer-budget-independent/README.md new file mode 100644 index 0000000000..3a9db642cc --- /dev/null +++ b/research/qq16-consumer-budget-independent/README.md @@ -0,0 +1,140 @@ +# Independent QQ16 consumer-budget audit and caller applicability + +The obstruction in [PR3908](https://github.com/CrocSwap/integer-mult-bounds/pull/3908) +is confirmed for its stated equal F0/B_1_2 pair, #2707 decoder and centre-64 +coverage model. Even after favorably dropping all eight reported rank-eight +children, the exact optimistic moment at the selected saving lies in + +```text +[1.000097677678, 1.000097678284] > 1. +``` + +This package independently expands the raw producer programs and decoder +word, binds the first F0 caller audited in PR3932, and uses rational +midpoint/trapezoid logarithm bounds instead of the predecessor's atanh +method. It supplies quantitative changed-contract thresholds to guide the +next research decision. It does not implement a supplier or change kappa. + +## Source and caller binding + +Canonical base `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, revision 6. +Audited PR3908 head `0d8880e38ed7c88d70eec6a48e5aa829d0fb22f3`. +The seven original package files are retained unchanged in +`vendor/PR3908.tar.gz` for an actual offline predecessor replay, with exact +hashes and credit in PREDECESSORS.json. No predecessor executable is imported +by the independent checker; `ceiling.py` is used only by that retained replay. + +The literal profiles are F0 `{1:2420,2:418,3:432,4:142,5:82}` and B_1_2 +`{1:2436,2:418,3:432,4:142,5:82}`. The literal decoder word contains 336 +rank-one lines across the pair. Its functional/native proof is inherited. +All external executable inputs have base-commit Git blob/SHA256 pins and +explicit replay invalidation in SOURCES.json and VERIFY.json. +The count check also covers all nine F and 28 B native cases. With the +decoder rate fixed at 168 per call, even the cheaper all-F profile remains +above one; F/B reweighting alone does not remove the obstruction. A different +global decoder rate is an unproved changed premise, not excluded here. + +F0 event 9894 is `['climb','A',546,0,4,1]`, followed by +`L546 -= L561` in frame 4. The complete preceding-event hash agrees with +[PR3932](https://github.com/CrocSwap/integer-mult-bounds/pull/3932), head +`12c324c576821f78070627c5eeb684d03704e20e`. Thus the local caller belongs +to the profile screened here. Physical admission and the full outer +schedule are separate. Changed call weights, decoder reuse, coverage or +actual replacement of a recursive tariff require a new complete invoice. +Faster scalar/axis tape work alone supplies none of those changes. + +## Decision and quantified alternatives + +Pause the unchanged recipe as a route to the selected target. Retain its +local numerical and tape components as useful interface results. The +following are certified *optimistic screens*, not implemented alternatives: + +| Assumed model | Largest integer decoder rank-one count per pair passing relaxation | Next count already excluded | +|---|---:|---:| +| Centre 64, eight rank-eight children waived | 121 | 122 | +| Centre 64, eight rank-eight children retained | 61 | 62 | +| Hypothetical centre 63, eight rank-eight children retained | 363 | 364 | + +The existing decoder has 336. A decoder-only revision must therefore remove +at least 215 calls in the first case or 275 in the second. These are necessary +budget targets, not lower bounds on all decoders. Odd totals allow fractional +per-call averages; an equal integer split restricts the limits to 120/60/362. + +Keeping all 336 calls and the reported rank-eight children, a hypothetical +one-unit centre reduction per call gives an optimistic moment in +`[0.999987387153,0.999987387763]`. Its additional normalized-cost allowance +is only about `0.0000126126`. Under the special unchanged-coverage accounting +where extra rank-one calls displace idle mass, 27 extra calls per pair still +pass; 28 fail. This is not a tariff for tape actions. + +The next useful question is whether an actual F17-native consumer or an +identity specific to the fixed native operators can remove the required +work without repaying it elsewhere. Simply setting centre=63 is not such +a construction. Neither this package nor PR3908 supplies that consumer. + +## Reproduce and verification boundary + +```sh +python3 -I -Werror -B research/qq16-consumer-budget-independent/verify.py +python3 -I -O -Werror -B research/qq16-consumer-budget-independent/test_verify.py +python3 -B scripts/research_package.py --package research/qq16-consumer-budget-independent +``` + +Expected: `PASS_QQ16_CONSUMER_BUDGET_INDEPENDENT no_new_kappa`, eleven +behavioral groups and `PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed`. +RESULT.json contains the complete rational enclosure receipt; PROOF.md +derives the bounds and scope; actual environments, execution and unrun +obligations are recorded in VERIFICATION.json. No network or unmerged Git +object is needed by the standalone scripts once declared base inputs are +provided. The source archive permits exact predecessor replay offline. + +The review checks PR3908's atanh positivity, exponential truncation, +rank-mass relaxation and selected-exponent implication. It also reproduces +the predecessor registered replay and its source-history preflight on a +full-history checkout. The independent implementation uses integral bounds +and a positive geometric exponential tail; all proof arithmetic is rational. +Controls cover omitted decoder work, illegal rank 52, threshold repayment, +source and receipt corruption, changed caller wire and deleted literal line. + +No full F0/B1 algebraic correctness replay, inherited native/bridge proof, +decoder operator replay, huge payload execution, selected cold replay, +Lean, full physical invoice, human review or supplier admission is claimed. + +## Open next questions + +**One named changed consumer contract.** Pin a downstream F17-native demand +map and compose it with the literal decoder. Identify the specific output +combination or fixed-native identity that removes real centre operations, +with its owner/frame chronology, arbitrary dirty state and required return. +Then derive the changed aggregate coverage identity and complete moment. +The narrow target here is one average centre mass unit per call, with all +replacement charges inside the certified allowance; broader changes need +their own screen. Stop if no actual demand or eliminated work is exhibited. + +This must distinguish the proposed contract from the selected first-transcript +counterexample (#2391), owner-local repair bound (#2461), copied-demand rank +floor (#3120) and pending uniform-oracle/selected-coverage audit (#3873). +Their scopes were inspected as adjacent evidence, not independently verified +here or automatically transferred to a new QQ16 endpoint. + +Only after a changed complete budget survives should this stream expand the +physical child-plus-ADD connection from #3932: actual tape windows and heads, +entry grid/range, both monomials, movement/address/control, adjacent ADD and +eventual restoration. A proof that direct bit implementation replaces a +recursive charge is another changed hypothesis and needs an all-depth cost +transfer. Unknown costs remain unknown. TASK.json records the family decision. + +## Credit + +1337isnot1337's #3908 exact obstruction; dcharb78's #3181 profile/cost-screen +branch; ywz65's #2707 decoder; Ali Romman and the conserved QQ16/native +lineage; Douglas Colkitt's selected coverage-ceiling model; Sagar Thakrar +and the coverage identity lineage; Nick Petalas's producer/decoder numerical +work; the retained native, supplier and source notices. This contribution +adds a different rational enclosure, literal count/caller binding and budget +thresholds, not the original obstruction or decoder theorem. + +Chris R / Clear1nsight, with substantial OpenAI assistance. Apache-2.0. +Independent software/mathematical checking is distinct from independent +human review or formal-kernel acceptance. Existing frozen sources, shared +verifiers, selected frontier and other contributions are unchanged. diff --git a/research/qq16-consumer-budget-independent/RESULT.json b/research/qq16-consumer-budget-independent/RESULT.json new file mode 100644 index 0000000000..8705db00a3 --- /dev/null +++ b/research/qq16-consumer-budget-independent/RESULT.json @@ -0,0 +1,138 @@ +{ + "caller": { + "child": [ + "climb", + "A", + 546, + 0, + 4, + 1 + ], + "event": 9894, + "next": [ + "scalar", + [ + "add", + [ + "L", + 546 + ], + [ + "L", + 561 + ], + -1, + 1 + ], + 4 + ], + "prefix_sha256": "15115954461f2cb93e2266822d82bfac1ab8de7d460ff78fcf594d21c61d2b53" + }, + "centre63_decoder_pair_threshold": { + "excluded": { + "decimal_lower": "1.000000126903", + "decimal_upper": "1.000000127515", + "lower": "1000000126903/1000000000000", + "upper": "200000025503/200000000000" + }, + "first_excluded": 364, + "last_pass": 363, + "passing": { + "decimal_lower": "0.999999671912", + "decimal_upper": "0.999999672524", + "lower": "124999958989/125000000000", + "upper": "249999918131/250000000000" + } + }, + "centre63_normalized_extra_cost_allowance": { + "decimal_lower": "0.000012612237", + "decimal_upper": "0.000012612847", + "lower": "12612237/1000000000000", + "upper": "12612847/1000000000000" + }, + "changed_centre63_full_profile": { + "decimal_lower": "0.999987387153", + "decimal_upper": "0.999987387763", + "lower": "999987387153/1000000000000", + "upper": "999987387763/1000000000000" + }, + "decoder_pair_children": 336, + "decoder_thresholds": [ + { + "excluded": { + "decimal_lower": "1.000000309592", + "decimal_upper": "1.000000310185", + "lower": "125000038699/125000000000", + "upper": "200000062037/200000000000" + }, + "first_integer_pair_count_excluded": 122, + "largest_integer_pair_count_passing_relaxation": 121, + "passing": { + "decimal_lower": "0.999999854601", + "decimal_upper": "0.999999855194", + "lower": "999999854601/1000000000000", + "upper": "499999927597/500000000000" + }, + "retains_eight_rank8": false + }, + { + "excluded": { + "decimal_lower": "1.000000400155", + "decimal_upper": "1.000000400749", + "lower": "200000080031/200000000000", + "upper": "1000000400749/1000000000000" + }, + "first_integer_pair_count_excluded": 62, + "largest_integer_pair_count_passing_relaxation": 61, + "passing": { + "decimal_lower": "0.999999945164", + "decimal_upper": "0.999999945758", + "lower": "249999986291/250000000000", + "upper": "499999972879/500000000000" + }, + "retains_eight_rank8": true + } + ], + "f_only_lower_envelope_with_168_decoder_per_call": { + "decimal_lower": "1.000090397821", + "decimal_upper": "1.000090398426", + "lower": "1000090397821/1000000000000", + "upper": "500045199213/500000000000" + }, + "minimal_profile_centre64": { + "decimal_lower": "1.000097677678", + "decimal_upper": "1.000097678284", + "lower": "500048838839/500000000000", + "upper": "250024419571/250000000000" + }, + "native_cases_profile_checked": 37, + "producer_events": { + "B_1_2": 27019, + "F_0": 26099 + }, + "producer_profiles": { + "B_1_2": { + "1": 2436, + "2": 418, + "3": 432, + "4": 142, + "5": 82 + }, + "F_0": { + "1": 2420, + "2": 418, + "3": 432, + "4": 142, + "5": 82 + } + }, + "reported_rank8_profile_centre64": { + "decimal_lower": "1.000125067705", + "decimal_upper": "1.000125068315", + "lower": "200025013541/200000000000", + "upper": "200025013663/200000000000" + }, + "scope": "Conditional fixed-profile coverage obstruction and optimistic changed-contract budget only; no physical supplier admission.", + "selected_a": "836330098538459/499163669901461541", + "status": "PASS_QQ16_CONSUMER_BUDGET_INDEPENDENT no_new_kappa" +} diff --git a/research/qq16-consumer-budget-independent/SOURCES.json b/research/qq16-consumer-budget-independent/SOURCES.json new file mode 100644 index 0000000000..2e0f50d876 --- /dev/null +++ b/research/qq16-consumer-budget-independent/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.json", + "usage": "input", + "git_blob": "7a155a27dcf7f1ccd48e40d57a2c5d2724016e9b", + "sha256": "b91eb8599c403db55c889bb225a1cd93f46fdb83eb339f101d18843d52b1c920" + }, + { + "path": "research/qq16-line-normalized-decoder/WORD.json", + "usage": "input", + "git_blob": "e45320dcb07ef2dc89622e9ca68adfe826a6e9dd", + "sha256": "5623b9cd62635d47f84e78135d817cfddec7ae31c154c565bf6e16cf5ed75475" + }, + { + "path": "research/qq16-line-normalized-decoder/RESULT.json", + "usage": "input", + "git_blob": "ba4167dbf133cff51513bb832802c290edcdffea", + "sha256": "58df4ad68e2ff335ee58fa4336a449d0f73f3366d840574e5e30b50f507c358d" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/qq16-consumer-budget-independent/TASK.json b/research/qq16-consumer-budget-independent/TASK.json new file mode 100644 index 0000000000..9cfeb95397 --- /dev/null +++ b/research/qq16-consumer-budget-independent/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "joint-query-controller", + "question": "Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md", + "research/qq16-producer-defect-transfer/README.md" + ], + "methods": [ + "Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.", + "Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer" + ] + }, + "scope_status": "refined", + "actual_scope": "Independent audit of PR3908 fixed-profile consumer obstruction; literal F0 caller and decoder count binding; exact rational decoder/centre tradeoff and changed-contract handoff.", + "scope_change_reason": "Explicit user continuation after PR3932, using a different logarithm enclosure and actual literal counts rather than another precision calculation or kernel optimization.", + "bottleneck_link": "Determine whether the local first F0 caller can belong to a supplier meeting the selected target, and identify the changed consumer obligation needed before expansion.", + "budget_minutes": 60, + "stop_rule": "Stop after independently verified obstruction/applicability and budget thresholds; pause unchanged-recipe target expansion. Do not build an unpriced centre-free supplier or change the selected frontier.", + "outcome": "completed", + "evidence": "Independent exact midpoint/trapezoid logarithm intervals, rational exponential tails, raw literal profile/decoder census, identical first-caller prefix, retained exact predecessor replay and behavioral controls. Execution receipt in VERIFICATION.json.", + "author": "Chris R / Clear1nsight", + "ai_assistance": "Substantial OpenAI assistance; no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can a named F17-native downstream demand or fixed-native identity remove real centre work while the changed complete bill fits the certified allowance?", + "why_it_matters": "The unchanged F0/B1 plus #2707 recipe fails before physical costs; a hypothetical one-unit centre reduction per call leaves only about 1.2612e-5 of normalized moment.", + "first_step": "Pin one actual downstream demand map and compose it with the literal decoder; specify owner/frame chronology, dirty restoration and genuinely eliminated operations. Price the resulting changed profile before further tape implementation.", + "blocked_by": "No such consumer or changed coverage identity is provided; known selected transcript/demand and uniform-oracle restrictions cannot be bypassed by relabelling." + } + ], + "family_decision": { + "decision": "pause unchanged target recipe; narrow next research to a changed consumer contract", + "proved": "Conditional centre-64 obstruction at selected target even with rank-eight children waived; exact decoder thresholds; source applicability to first F0 caller.", + "constructively_upper_bounded": "Two-sided optimistic moments only; centre63 plus existing profile passes the relaxation with small allowance.", + "unknown": "Actual F17 consumer and changed coverage identity; legal eliminated work; paid transfer from tape actions to recursive tariff; all-depth ownership, routing, restoration, precision and complete supplier costs.", + "next_test": "Pin one actual downstream demand map and compose it with the literal decoder; specify owner/frame chronology, dirty restoration and genuinely eliminated operations. Price the resulting changed profile before further tape implementation.", + "reopen_trigger": "A concrete changed endpoint/native identity or genuinely replaced recursive tariff with a favorable complete invoice." + }, + "coordination": { + "canonical_investigation": "https://github.com/CrocSwap/integer-mult-bounds/pull/3908#issuecomment-6260505775", + "entry_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "entry_checked_utc": "2026-10-19T05:35:00Z", + "priority_revision": 6, + "overlap_limit": "find_overlap remote refresh unavailable: gh absent. Targeted live PR bodies, QQ16 Discussion index, #2727 and first-caller handoff checked; no exhaustive novelty claim.", + "related_scopes_inspected": [ + 2391, + 2461, + 3120, + 3873, + 3908, + 3932 + ], + "freshness": "Canonical main, instruction/priorities/catalogue/selected/family changes checked: unchanged. Recheck live heads/overlap immediately before publication.", + "checkpoint_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "checkpoint_checked_utc": "2026-10-19T05:52:08.239512+00:00" + } +} diff --git a/research/qq16-consumer-budget-independent/VERIFICATION.json b/research/qq16-consumer-budget-independent/VERIFICATION.json new file mode 100644 index 0000000000..0229e55907 --- /dev/null +++ b/research/qq16-consumer-budget-independent/VERIFICATION.json @@ -0,0 +1,82 @@ +{ + "recorded_utc": "2026-10-19T05:52:38.562754+00:00", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.39", + "export": { + "git_free": true, + "regular_copied_files": 18, + "unchanged_after_successful_replays": true, + "normal_and_optimized_receipt_mutants_rejected": true, + "commands": [ + { + "script": "verify.py", + "isolated": true, + "optimized": false, + "warnings_as_errors": true, + "bytecode_writes": false, + "exit_code": 0, + "seconds": 1.229, + "stdout_sha256": "4f4d203ab38df939dab2a1e4f056f2e9de1ca5fbf7227a961ddeb57c8ca85b24", + "stderr": "" + }, + { + "script": "verify.py", + "isolated": true, + "optimized": true, + "warnings_as_errors": true, + "bytecode_writes": false, + "exit_code": 0, + "seconds": 1.321, + "stdout_sha256": "4f4d203ab38df939dab2a1e4f056f2e9de1ca5fbf7227a961ddeb57c8ca85b24", + "stderr": "" + }, + { + "script": "test_verify.py", + "isolated": true, + "optimized": false, + "warnings_as_errors": true, + "bytecode_writes": false, + "exit_code": 0, + "seconds": 9.889, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "stderr": "...........\n----------------------------------------------------------------------\nRan 11 tests in 9.699s\n\nOK\n" + }, + { + "script": "test_verify.py", + "isolated": true, + "optimized": true, + "warnings_as_errors": true, + "bytecode_writes": false, + "exit_code": 0, + "seconds": 13.626, + "stdout_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "stderr": "...........\n----------------------------------------------------------------------\nRan 11 tests in 12.653s\n\nOK\n" + } + ] + }, + "scientific_file_sha256": { + "PREDECESSORS.json": "6f46104ccdcad56ef1025b1a7eae63c1814c6183f80260d35812e67b75165cb3", + "PROOF.md": "a90a1d77b717908b64b25509f6a57c5d63b5ba8cf5539519e393258caa163f9c", + "README.md": "5fa713475152249d052a3dff418e423c8aeed26ad95a170afc056fa2e60ded50", + "RESULT.json": "4f4d203ab38df939dab2a1e4f056f2e9de1ca5fbf7227a961ddeb57c8ca85b24", + "SOURCES.json": "1bdbd986f6814713dea567c6ae80ec808d21883c60521a0fae3f78a976ba0a65", + "TASK.json": "90c2928314832bbcb2fe7112d5c7abf4f406c3fbcb749c5626f5e853d1e22e48", + "VERIFY.json": "aa7f6e385bf3ff9aea622ae30269ea8479d9c0019f8159995a9d30ced1dd866f", + "test_verify.py": "9e0eaf41d1398416770e96be30970fe0aab633b4b25fbe185df55d89f71d155f", + "vendor/PR3908.tar.gz": "9ccaf27da52f96a5701d8d7f9e9934a64f8bbc15f0aa12bd45c7168785d6966d", + "verify.py": "e12f3d810a6f659e4b2453d251e323aa5e2c4693c4b28a9cec611796cc2dd94a" + }, + "predecessor_registered_replay": { + "status": "passed locally", + "head": "0d8880e38ed7c88d70eec6a48e5aa829d0fb22f3", + "committed_byte_and_source_history_preflight": "PASS; 12 files; base20ecf2891d80b5acf18d980b2164fb44ea7faa90 ancestor" + }, + "new_registered_replay": "Passed locally on CPython3.12.3; metadata/pins and warning-strict compilation passed. Exact-head publication preflight and hosted CI recorded separately.", + "limitations": [ + "No inherited full native/bridge/decoder algebra replay", + "No full selected cold replay or all-depth payload allocation", + "No physical consumer, complete recursive supplier or new selected kappa", + "No independent human or proof-kernel review", + "No Ruff run for this package" + ] +} diff --git a/research/qq16-consumer-budget-independent/VERIFY.json b/research/qq16-consumer-budget-independent/VERIFY.json new file mode 100644 index 0000000000..088accd486 --- /dev/null +++ b/research/qq16-consumer-budget-independent/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/complex-local-word-ceiling/RESULT.json", + "research/complex-local-word-ceiling/ceiling.py", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.json", + "research/qq16-line-normalized-decoder/WORD.json", + "research/qq16-line-normalized-decoder/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticated raw F0/B1 and decoder counts; caller/prefix applicability; independent rational quadrature moment enclosures and decoder/centre thresholds; complete RESULT equality." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Eleven behavioral groups: quadrature/tails, idle mass relaxation, omitted decoder, thresholds/repayment, source/JSON/domain controls, semantic mutants and byte-authenticated exact PR3908 replay in temporary export." + } + ] +} diff --git a/research/qq16-consumer-budget-independent/test_verify.py b/research/qq16-consumer-budget-independent/test_verify.py new file mode 100644 index 0000000000..c8f2fe9240 --- /dev/null +++ b/research/qq16-consumer-budget-independent/test_verify.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Behavioral controls; no network, Git objects or predecessor imports needed.""" +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha1, sha256 +import gzip +import io +import json +from pathlib import Path +import runpy +import subprocess +import sys +import tarfile +import tempfile +import unittest +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +V = runpy.run_path(str(HERE / 'verify.py')) +ROOT = V['ROOT'] +BASE = {1:2428, 2:418, 3:432, 4:142, 5:82} +A = Q(836330098538459, 499163669901461541) + + +class Audit(unittest.TestCase): + def test_01_complete_receipt(self): + self.assertEqual(V['canonical'](V['calculate']()), + V['canonical'](V['decode']((HERE / 'RESULT.json').read_bytes()))) + + def test_02_log_integral_enclosures(self): + self.assertEqual(V['integral_log'](Q(1)), (0, 0)) + lo, hi = V['logarithm'](Q(2)) + known = Q(693147180559945309417, 10**21) + self.assertLess(lo, known) + self.assertGreater(hi, known + Q(1, 10**21)) + for y in [Q(9,8), Q(73,51), Q(2)]: + coarse = V['integral_log'](y, 16) + fine = V['integral_log'](y, 128) + self.assertLessEqual(coarse[0], fine[0]) + self.assertLessEqual(fine[1], coarse[1]) + self.assertGreaterEqual(fine[0], 1 - 1/y) + self.assertLessEqual(fine[1], y-1) + with self.assertRaisesRegex(ValueError, 'domain'): + V['logarithm'](Q(1,2)) + + def test_03_exp_tail_and_rounding(self): + self.assertEqual(V['exponential'](Q(0), Q(0)), (1,1)) + lo, hi = V['exponential'](Q(1,2), Q(1,2), 12) + # Independently bounded e^(1/2), from squaring a known e enclosure. + self.assertLess(lo*lo, Q(2718281828459045235361, 10**21)) + self.assertGreater(hi*hi, Q(2718281828459045235362, 10**21)) + self.assertLess(hi-lo, Q(1,10**12)) + self.assertEqual(V['outward'](Q(1,3),Q(2,3))[0] <= Q(1,3), True) + self.assertEqual(V['outward'](Q(1,3),Q(2,3))[1] >= Q(2,3), True) + with self.assertRaisesRegex(ValueError, 'domain'): + V['exponential'](Q(0), Q(1)) + + def test_04_idle_mass_relaxation(self): + for r in [1,2,3,4,5,8,17,34,50]: + lo, hi = V['cost'](r,A) + rlo, rhi = V['cost'](51,A) + self.assertGreater(lo/r, rhi/51) + zlo, zhi = V['cost'](r,Q(0)) + self.assertLessEqual(zlo, Q(r,73)) + self.assertGreaterEqual(zhi, Q(r,73)) + with self.assertRaisesRegex(ValueError, 'halving'): + V['moment'](BASE,336,64,False,A,52) + + def test_05_omitted_decoder_changes_decision(self): + self.assertLess(V['moment'](BASE,0,64,True,A)[1],1) + self.assertGreater(V['moment'](BASE,336,64,False,A)[0],1) + # Even deleting two whole groups of 112 leaves 112, above the full threshold. + self.assertGreater(V['moment'](BASE,112,64,True,A)[0],1) + + def test_06_thresholds_and_repayment(self): + for rank8,last in [(False,121),(True,61)]: + self.assertLess(V['moment'](BASE,last,64,rank8,A)[1],1) + self.assertGreater(V['moment'](BASE,last+1,64,rank8,A)[0],1) + self.assertLess(V['moment'](BASE,363,63,True,A)[1],1) + self.assertGreater(V['moment'](BASE,364,63,True,A)[0],1) + self.assertGreater(V['moment'](BASE,336,64,True,A)[0],1) + + def test_07_negative_and_excess_budget(self): + with self.assertRaisesRegex(ValueError, 'negative budget'): + V['moment'](BASE,-1,64,True,A) + with self.assertRaisesRegex(ValueError, 'negative idle'): + V['moment'](BASE,10000,64,True,A) + + def test_08_literal_omissions(self): + c = V['decode'](gzip.decompress(V['pinned']('research/joint-query/certificate.json.gz'))) + original = V['profile'](c,V['expand'](c,'F_0')) + altered = deepcopy(c) + altered['programs']['F_0'] = [e for e in altered['programs']['F_0'] if e[0] != 'private_sweep'] + self.assertNotEqual(V['profile'](altered,V['expand'](altered,'F_0')), original) + changed = deepcopy(c) + next(e for e in changed['core_words']['forward'] if e[0]=='climb')[5] = 2 + self.assertNotEqual(V['profile'](changed,V['expand'](changed,'F_0')), original) + changed['programs']['F_0'].append(['unknown']) + with self.assertRaisesRegex(ValueError, 'unknown event'): + V['expand'](changed,'F_0') + + def test_09_source_and_manifest_controls(self): + manifest = V['decode']((HERE/'SOURCES.json').read_bytes()) + path = 'certificates/selected-result.json' + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + (root/path).parent.mkdir(parents=True) + (root/path).write_bytes((ROOT/path).read_bytes()+b' ') + with self.assertRaisesRegex(ValueError,'SHA256'): + V['pinned'](path,root,manifest) + (root/path).write_bytes((ROOT/path).read_bytes()) + duplicate = deepcopy(manifest) + duplicate['files'].append(deepcopy(duplicate['files'][0])) + with self.assertRaisesRegex(ValueError,'unique input'): + V['pinned'](path,root,duplicate) + manifest['files'][0]['git_blob'] = '0'*40 + with self.assertRaisesRegex(ValueError,'Git blob'): + V['pinned'](path,root,manifest) + with self.assertRaisesRegex(ValueError,'duplicate JSON'): + V['decode']('{"a":1,"a":2}') + self.assertNotEqual(V['canonical']({'a':1}),V['canonical']({'a':True})) + + def test_10_retained_original_replay(self): + meta = V['decode']((HERE/'PREDECESSORS.json').read_bytes()) + archive = (HERE/'vendor/PR3908.tar.gz').read_bytes() + self.assertEqual(sha256(archive).hexdigest(),meta['archive_sha256']) + expected = {r['path']:r for r in meta['files']} + self.assertEqual(len(expected),7) + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + with tarfile.open(fileobj=io.BytesIO(archive), mode='r:gz') as t: + members=t.getmembers() + self.assertEqual(len(members),7) + self.assertEqual({m.name for m in members},set(expected)) + for member in members: + self.assertTrue(member.isfile()) + self.assertNotIn('..',Path(member.name).parts) + self.assertFalse(Path(member.name).is_absolute()) + b=t.extractfile(member).read() + self.assertEqual(sha256(b).hexdigest(),expected[member.name]['sha256']) + self.assertEqual(sha1(b'blob '+str(len(b)).encode()+b'\0'+b).hexdigest(),expected[member.name]['git_blob']) + dest=root/member.name;dest.parent.mkdir(parents=True,exist_ok=True);dest.write_bytes(b) + manifest=V['decode']((HERE/'SOURCES.json').read_bytes()) + for row in manifest['files']: + if row['usage']=='input': + dest=root/row['path'];dest.parent.mkdir(parents=True,exist_ok=True) + dest.write_bytes(V['pinned'](row['path'])) + result=subprocess.run([sys.executable,'-I','-O','-Werror','-B', + str(root/'research/qq16-consumer-cap-audit/verify.py')], + cwd=root,check=True,capture_output=True,text=True,timeout=60) + answer=json.loads(result.stdout) + self.assertEqual(answer['status'],'PASS_QQ16_CONSUMER_CAP_BELOW_SELECTED no_new_kappa') + self.assertEqual(answer['display_decimal'],'1.000097677879937') + # This predecessor output is a lower bound, not a feasibility proof. + self.assertGreater(Q(answer['display_decimal']), Q(100009,100000)) + + def test_11_rebound_semantic_mutants(self): + """Rebind hashes deliberately: semantic checks must also reject.""" + original=V['pinned'] + cp='research/joint-query/certificate.json.gz' + rp='research/joint-query/evidence/CONSERVED-QQ16.json' + packet=V['decode'](gzip.decompress(original(cp))) + reported=V['decode'](original(rp)) + # Wire mutation preserves every rank/count, but changes caller applicability. + next(e for e in packet['core_words']['forward'] if e[0]=='climb')[2]=547 + payload=V['canonical'](packet) + reported['payload_sha256']=sha256(payload).hexdigest() + replacements={cp:gzip.compress(payload,mtime=0),rp:V['canonical'](reported)} + def load(path,*args,**kwargs): + return replacements.get(path) if path in replacements else original(path,*args,**kwargs) + with patch.dict(V['calculate'].__globals__,{'pinned':load}): + with self.assertRaisesRegex(ValueError,'first F0 caller'): + V['calculate']() + # A deleted line cannot acquire the original invoice through a new hash. + dp='research/qq16-line-normalized-decoder/WORD.json' + word=V['decode'](original(dp));word.remove(next(e for e in word if e[0]=='line')) + replacements.clear();replacements[dp]=V['canonical'](word) + with patch.dict(V['calculate'].__globals__,{'pinned':load}): + with self.assertRaisesRegex(ValueError,'literal decoder inventory'): + V['calculate']() + + +if __name__=='__main__': + unittest.main() diff --git a/research/qq16-consumer-budget-independent/vendor/PR3908.tar.gz b/research/qq16-consumer-budget-independent/vendor/PR3908.tar.gz new file mode 100644 index 0000000000..a83a4024b8 Binary files /dev/null and b/research/qq16-consumer-budget-independent/vendor/PR3908.tar.gz differ diff --git a/research/qq16-consumer-budget-independent/verify.py b/research/qq16-consumer-budget-independent/verify.py new file mode 100644 index 0000000000..dd53a9472d --- /dev/null +++ b/research/qq16-consumer-budget-independent/verify.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Independent QQ16 profile/caller and rational quadrature budget audit. + +Chris R / Clear1nsight, with substantial OpenAI assistance. Apache-2.0. +No predecessor executable is imported. See PROOF.md for the interval argument. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from hashlib import sha1, sha256 +import gzip +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +M, W, R = 73, Q(896, 9), 51 +GRID = 1 << 80 + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, 'duplicate JSON key') + out[key] = value + return out + + +def decode(raw): + return json.loads(raw, object_pairs_hook=unique) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def pinned(path, root=ROOT, manifest=None): + if manifest is None: + manifest = decode((HERE / 'SOURCES.json').read_bytes()) + rows = [row for row in manifest['files'] if row['path'] == path and row['usage'] == 'input'] + need(len(rows) == 1, 'unique input pin: ' + path) + raw = (root / path).read_bytes() + row = rows[0] + need(sha256(raw).hexdigest() == row['sha256'], 'source SHA256: ' + path) + need(sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == row['git_blob'], + 'source Git blob: ' + path) + return raw + + +def outward(lo, hi): + return Q((lo.numerator * GRID) // lo.denominator, GRID), Q(-((-hi.numerator * GRID) // hi.denominator), GRID) + + +@lru_cache(None) +def integral_log(y, panels=1024): + """Midpoint lower / trapezoid upper for integral_1^y 1/t dt.""" + y = Q(y) + need(1 <= y <= 2 and type(panels) is int and panels > 0, 'quadrature domain') + if y == 1: + return Q(0), Q(0) + h = (y - 1) / panels + lo = h * sum(1 / (1 + (Q(j) + Q(1, 2)) * h) for j in range(panels)) + hi = h * ((1 + 1 / y) / 2 + sum(1 / (1 + j * h) for j in range(1, panels))) + return outward(lo, hi) + + +@lru_cache(None) +def logarithm(x): + x = Q(x) + need(x >= 1, 'logarithm domain') + powers = 0 + while x > 2: + x /= 2 + powers += 1 + lo, hi = integral_log(x) + two_lo, two_hi = integral_log(Q(2)) + return outward(lo + powers * two_lo, hi + powers * two_hi) + + +def exponential(lo, hi, degree=6): + need(0 <= lo <= hi <= Q(1, 2), 'exponential domain') + need(type(degree) is int and degree >= 1, 'exponential degree') + lsum = usum = lterm = uterm = Q(1) + for j in range(1, degree + 1): + lterm *= lo / j + uterm *= hi / j + lsum += lterm + usum += uterm + first = uterm * hi / (degree + 1) + tail = first / (1 - hi / (degree + 2)) + return outward(lsum, usum + tail) + + +@lru_cache(None) +def cost(rank, a): + need(type(rank) is int and 0 < rank < M and a >= 0, 'child domain') + lo, hi = logarithm(Q(M, rank)) + lo, hi = exponential(a * lo, a * hi) + return outward(Q(rank, M) * lo, Q(rank, M) * hi) + + +def expand(packet, name): + events = [] + + def visit(sequence): + for event in sequence: + tag = event[0] + if tag == 'retained_core': + need(event[1] in ('forward', 'backward'), 'core orientation') + visit(packet['core_words'][event[1]]) + elif tag in ('private_sweep', 'cover_sweep'): + visit(event[2]) + else: + need(tag in ('scalar', 'climb', 'adapter', 'residual_adapter', + 'phase', 'native_line', 'cover_map'), 'unknown event') + events.append(event) + + visit(packet['programs'][name]) + return events + + +def profile(packet, events): + out = Counter() + for event in events: + if event[0] == 'climb': + rank = event[5] + elif event[0] == 'native_line': + record = packet['native_line_recipes'][event[2]] + rank = record['rank'] + need(record['recipe']['rank'] == rank, 'wrapper recipe rank') + else: + continue + need(type(rank) is int and 0 < rank < M, 'literal child rank') + out[rank] += 1 + return dict(sorted(out.items())) + + +def moment(base, decoder_pair, centre, rank8, a, idle_rank=R): + need(all(type(r) is int and 0 < r < M and Q(n) >= 0 for r,n in base.items()), 'local profile domain') + need(2 * idle_rank**2 < M**2 and idle_rank >= max(base), 'halving / relaxation rank') + need(Q(decoder_pair) >= 0 and Q(centre) >= 0, 'negative budget charge') + local = {r: Q(n) for r, n in base.items()} + local[1] += Q(decoder_pair, 2) + if rank8: + local[8] = Q(8) + total = (M - 1) * W + centre + paid = sum(r * n for r, n in local.items()) + idle = total - paid + need(idle >= 0, 'negative idle mass') + lo = hi = Q(0) + for rank, number in local.items(): + clo, chi = cost(rank, a) + lo += number * clo + hi += number * chi + clo, chi = cost(idle_rank, a) + return outward((lo + idle / idle_rank * clo) / W, + (hi + idle / idle_rank * chi) / W) + + +def decimal_interval(pair, digits=12): + scale = 10**digits + lo, hi = pair + l = lo.numerator * scale // lo.denominator + u = -((-hi.numerator * scale) // hi.denominator) + return {'lower': str(Q(l, scale)), 'upper': str(Q(u, scale)), + 'decimal_lower': f'{l // scale}.{l % scale:0{digits}d}', + 'decimal_upper': f'{u // scale}.{u % scale:0{digits}d}'} + + +def calculate(root=ROOT, manifest=None): + def source(path): + return pinned(path, root, manifest) + + # Also authenticated for the retained predecessor replay in test_verify.py. + source('research/complex-local-word-ceiling/ceiling.py') + selected = decode(source('certificates/selected-result.json')) + kappa = Q(selected['kappa']) + need(kappa == Q(836330098538459, 500000000000000000), 'selected target') + a = kappa / (1 - kappa) + model = decode(source('research/complex-local-word-ceiling/RESULT.json'))['model'] + need((model['m'], Q(model['live_families_per_call']), model['centre_per_call'], + model['idle_rank_cap']) == (M, W, 64, R), 'coverage model') + payload = gzip.decompress(source('research/joint-query/certificate.json.gz')) + packet = decode(payload) + reported = decode(source('research/joint-query/evidence/CONSERVED-QQ16.json')) + need(sha256(payload).hexdigest() == reported['payload_sha256'], 'producer payload binding') + profiles, event_counts = {}, {} + for name, side in [('F_0', 'F'), ('B_1_2', 'B')]: + events = expand(packet, name) + profiles[name] = profile(packet, events) + event_counts[name] = len(events) + need(profiles[name] == {int(r): n for r, n in reported['invoices'][side]['native_profile'].items()}, + 'literal / reported producer profile') + need(sum(r * n for r, n in profiles[name].items()) == reported['invoices'][side]['native_mass'], + 'literal producer mass') + need(event_counts == {'F_0': 26099, 'B_1_2': 27019}, 'literal event counts') + need(len(packet['programs']) == 37, 'complete native case inventory') + for name in packet['programs']: + expected = profiles['F_0'] if name.startswith('F_') else profiles['B_1_2'] + need(name.startswith(('F_', 'B_')) and profile(packet, expand(packet, name)) == expected, + 'native case profile: ' + name) + f = expand(packet, 'F_0') + cut = next(j for j, e in enumerate(f) if e[0] in ('climb', 'native_line')) + need((cut, f[cut], f[cut+1]) == + (9894, ['climb', 'A', 546, 0, 4, 1], ['scalar', ['add', ['L', 546], ['L', 561], -1, 1], 4]), + 'first F0 caller and consumer') + need(sha256(canonical(f[:cut])).hexdigest() == + '15115954461f2cb93e2266822d82bfac1ab8de7d460ff78fcf594d21c61d2b53', + 'first F0 prefix binding') + decoder_word = decode(source('research/qq16-line-normalized-decoder/WORD.json')) + dc = Counter(event[0] for event in decoder_word) + need(dc == {'add': 2704, 'map': 464, 'line': 336, 'clear': 312, 'begin': 3, 'end': 3, 'checkpoint': 1}, + 'literal decoder inventory') + need(all(len(e) == 4 and e[3] in (-1, 1) for e in decoder_word if e[0] == 'line'), + 'decoder signed line syntax') + decoder = decode(source('research/qq16-line-normalized-decoder/RESULT.json')) + need(decoder['invoice']['rank_one_children'] == dc['line'] and decoder['invoice']['rank_eight_children'] == 0, + 'literal / reported decoder count') + base = {r: Q(profiles['F_0'].get(r, 0) + profiles['B_1_2'].get(r, 0), 2) + for r in set(profiles['F_0']) | set(profiles['B_1_2'])} + need(base == {1:2428, 2:418, 3:432, 4:142, 5:82}, 'pair average') + relaxed = moment(base, dc['line'], 64, False, a) + full = moment(base, dc['line'], 64, True, a) + centre63 = moment(base, dc['line'], 63, True, a) + f_only = moment(profiles['F_0'], dc['line'], 64, False, a) + need(relaxed[0] > Q(100009, 100000) and full[0] > relaxed[1], 'independent obstruction') + need(f_only[0] > Q(100009, 100000), 'F/B reweighting with fixed decoder rate') + need(centre63[1] < 1, 'changed-centre optimistic opening') + rows = [] + for rank8, last_pass, first_fail in [(False, 121, 122), (True, 61, 62)]: + passing = moment(base, last_pass, 64, rank8, a) + failing = moment(base, first_fail, 64, rank8, a) + need(passing[1] < 1 < failing[0], 'decoder threshold bracket') + rows.append({'retains_eight_rank8':rank8, 'largest_integer_pair_count_passing_relaxation':last_pass, + 'first_integer_pair_count_excluded':first_fail, + 'passing':decimal_interval(passing), 'excluded':decimal_interval(failing)}) + p363, p364 = moment(base,363,63,True,a), moment(base,364,63,True,a) + need(p363[1] < 1 < p364[0], 'centre63 repayment threshold') + return {'status':'PASS_QQ16_CONSUMER_BUDGET_INDEPENDENT no_new_kappa', + 'selected_a':str(a), 'producer_profiles':{k:{str(r):n for r,n in p.items()} for k,p in profiles.items()}, + 'producer_events':event_counts, 'decoder_pair_children':dc['line'], + 'native_cases_profile_checked':37, + 'f_only_lower_envelope_with_168_decoder_per_call':decimal_interval(f_only), + 'caller':{'event':cut,'child':f[cut],'next':f[cut+1], + 'prefix_sha256':sha256(canonical(f[:cut])).hexdigest()}, + 'minimal_profile_centre64':decimal_interval(relaxed), + 'reported_rank8_profile_centre64':decimal_interval(full), + 'changed_centre63_full_profile':decimal_interval(centre63), + 'centre63_normalized_extra_cost_allowance':decimal_interval((1-centre63[1],1-centre63[0])), + 'decoder_thresholds':rows, + 'centre63_decoder_pair_threshold':{'last_pass':363,'first_excluded':364, + 'passing':decimal_interval(p363),'excluded':decimal_interval(p364)}, + 'scope':'Conditional fixed-profile coverage obstruction and optimistic changed-contract budget only; no physical supplier admission.'} + + +def main(): + actual = calculate() + expected = decode((HERE / 'RESULT.json').read_bytes()) + need(canonical(actual) == canonical(expected), 'complete RESULT mismatch') + print(json.dumps(actual, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main()