From 3c182afc7c5597170caf60e8dd14a6d910e6b01e Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Thu, 22 Oct 2026 09:30:42 -0500 Subject: [PATCH 1/5] Prove an all-mask all-p ceiling for the paired-path thinning moment --- .../FROZEN-SOURCE.json | 10 + .../PROOF.md | 190 ++++++++++++++ .../README.md | 51 ++++ .../RESULT.json | 219 ++++++++++++++++ .../SOURCES.json | 36 +++ .../TASK.json | 66 +++++ .../VERIFY.json | 22 ++ .../inputs/PR4610-ARITHMETIC.json | 241 ++++++++++++++++++ .../verify.py | 208 +++++++++++++++ 9 files changed, 1043 insertions(+) create mode 100644 research/controller-thinning-global-ceiling/FROZEN-SOURCE.json create mode 100644 research/controller-thinning-global-ceiling/PROOF.md create mode 100644 research/controller-thinning-global-ceiling/README.md create mode 100644 research/controller-thinning-global-ceiling/RESULT.json create mode 100644 research/controller-thinning-global-ceiling/SOURCES.json create mode 100644 research/controller-thinning-global-ceiling/TASK.json create mode 100644 research/controller-thinning-global-ceiling/VERIFY.json create mode 100644 research/controller-thinning-global-ceiling/inputs/PR4610-ARITHMETIC.json create mode 100644 research/controller-thinning-global-ceiling/verify.py diff --git a/research/controller-thinning-global-ceiling/FROZEN-SOURCE.json b/research/controller-thinning-global-ceiling/FROZEN-SOURCE.json new file mode 100644 index 0000000000..00494cdb30 --- /dev/null +++ b/research/controller-thinning-global-ceiling/FROZEN-SOURCE.json @@ -0,0 +1,10 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "pr": 4610, + "commit": "1eb8da6cfb35512c0cc2533413e5ca42f48e13c6", + "path": "research/kappa-round3-warp-20261022/ARITHMETIC.json", + "snapshot": "inputs/PR4610-ARITHMETIC.json", + "git_blob": "c89e009ca4a5ad316c69f0371d885d72045ba415", + "sha256": "ab10f6a4a8a4f589d4b094aac663e002c43ec44774e6bd181c51915c7fa7e521", + "credit": "Cao Yifan (intqwq), substantial OpenAI Codex assistance; Apache-2.0; cumulative PR4470/predecessor attribution retained in original source." +} diff --git a/research/controller-thinning-global-ceiling/PROOF.md b/research/controller-thinning-global-ceiling/PROOF.md new file mode 100644 index 0000000000..cad9588d7a --- /dev/null +++ b/research/controller-thinning-global-ceiling/PROOF.md @@ -0,0 +1,190 @@ +# A ceiling for every thinning of the retained paired-path moment + +Prepared for Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. + +## Scope and conclusion + +Freeze Cao Yifan's PR4610 round-three profile at +`1eb8da6cfb35512c0cc2533413e5ca42f48e13c6`: + +``` +H = {4:28, 7:7, 8:47, 9:326} +P = {1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}. +``` + +There are 112 ports, fresh block width 8, and one paid rank-one query per +port at each thin stage. Keep the predecessor's paired-path scalar word, +all its middle idle windows, a prefix of initial idle windows and the +complementary suffix of terminal idle windows. Allow **every** pair count +`p>=1`, every split `a+b=p-1`, and every binary subset of the `2p+1` full +stages. Specialize every removed stage multiplier to the identity in both +the idle words and the advertised main targets. Keep all productive helper +losses, paid native jobs, owned centres and thin queries. + +Under this retained endpoint/invoice contract, no such word has positive +raw surplus at any saving `0.0030217759 <= C < 1`. The p16, a7/a8 word +has positive surplus at `C=0.0030217758`. Thus the best raw crossing is +in that interval of width `10^-10`; p16 with the existing alternating +full-stage pattern attains it. This is an infinite-family **moment theorem**, +not a new operator-admission theorem or a global barrier for other words. + +The endpoint pattern is an explicit hypothesis inherited from the path +construction: one pair has all stage factors; the other pairs have the +successive prefix or suffix factors below. We do not infer a new universal +native/phase identity from finite tests. The verifier independently checks +the literal source's exact rational projectors and the complete formula +for every split and stage subset through p5. Those tests bind the stated +contract to the retained examples; the reductions and calculus below are +the infinite part of the theorem. + +## 1. Arbitrary-mask formula + +Fix `0=0`, by subadditivity of x^t. This includes +equality when c=0. + +**Remove an empty pair.** For `(0,0)` remove that window and its two +thin stages. Its contribution is `g(c)=h(c)-f(c)<=1`, including g(0)=1. +The query saving is 224, so the surplus gain is `224(1-g(c))>=0`. +The side length and p each decrease by one; no full stage or helper is lost. + +**Split a double-full pair.** Replace `(1,1)` by two successive `(1,0)` +pairs, adding one window and two stages, with k unchanged. The extra thin +query charge is 224. The surplus gain divided by 224 is + +``` +h(c+1) - f(c+2) + f(1) - 1 + = (8^t-1) - [(8(c+2))^t-(8(c+1)+1)^t] > 0. +``` + +Both differences on the right integrate the strictly decreasing derivative +`t*x^(t-1)` over an interval of length 7. The first interval starts at 1; +the second starts at `8(c+1)+1>=9`. This proves strict positivity. + +Apply the first move to even-only pairs and split every double-full pair. +Then remove all empty pairs. The process terminates with only `(1,0)` +pairs. It preserves the three separate bits `l=s_0`, `r=s_(2p)`, and m +at the intervening odd stage, each in {0,1}. Splitting may increase p; +no finite pair-count cutoff is used. + +## 3. Eight concave sequences replace the infinite mask search + +Write `S=a+b`, `B=l+r+m`, `k=S+B`, and `g(j)=h(j)-f(j)`. +For a normalized mask, + +``` +F(S,a,b;l,r,m) = k A(t) + + 224 [h(k) + sum_(j=1)^a g(l+j) + sum_(j=1)^b g(r+j)] + - 112(2S+3-k). +``` + +The positive sequence g(j) is strictly decreasing for integer j>=1. +For fixed S and bits, the largest side sum is obtained by merging the +two decreasing lists `g(l+1),g(l+2),...` and `g(r+1),g(r+2),...`, taking +their S largest terms. This uses only integer argument order, not floating +comparisons. Let their sum be G(S). + +For each of the eight bit triples, the resulting upper envelope has increment + +``` +F(S+1)-F(S) = A(t)-112 + +224 [h(S+B+1)-h(S+B) + (G(S+1)-G(S))]. +``` + +The h increment strictly decreases and the next merged g term never increases. +Thus F is strictly discretely concave. A strict positive preceding increment +and strict negative following increment certify its unique integer maximum +over **all S>=0**. No tail search or unexplored large-p assumption remains. + +At `C=0.0030217759` the exact interval certificate gives: + +| l,r,m | Maximizing S | Upper bound for F | +|---|---:|---:| +| 0,0,0 | 18 | -7.78098 | +| 1,0,0 | 17 | -5.66497 | +| 0,1,0 | 17 | -5.66497 | +| 1,1,0 | 16 | -3.54895 | +| 0,0,1 | 17 | -4.23203 | +| 1,0,1 | 16 | -2.11602 | +| 0,1,1 | 16 | -2.11602 | +| 1,1,1 | 15 | -0.00000722 | + +Displayed bounds are rounded upward; exact outward enclosures and adjacent +increments are in RESULT.json. All eight maxima are strictly negative. +For bits (1,1,1), S=15 means p=16, with sides 7 and 8 in either order. +Its surplus is strictly positive at the stated lower endpoint. + +## 4. Exclude every larger C, rather than only one sampled exponent + +Let `L(t)=P(t)-H(t)`. Its derivative divided by 9^t is + +``` +sum_(r=2,3,4,5) n_r (r/9)^t log r + - 7(7/9)^t log 7 - 39(8/9)^t log 8 - 326 log 9, +n_2=412, n_3=510, n_4=99, n_5=40. +``` + +For `1/4<=t<=1`, upper-bound the positive terms at t=1/4 and +upper-bound each negative term at t=1. The exact resulting bound is below +`-9.53`. Hence L strictly decreases on this whole interval. Each h(k) +increases in t; so does each g(j), since `x^t log x` increases in x>=1. +Consequently every normalized F increases in t on [1/4,1]. Negativity +at `t=1-0.0030217759` excludes all smaller t down to 1/4. + +For `0=3298 and H(t)<=2*408, since `9^(1/4)<2`. +Thus L(t)>=2482. Concavity gives `h(k)<=1+8kt` and `g(j)<=t` +for integer j>=1. Therefore every normalized surplus satisfies + +``` +F <= -112 + k(112+1792t-2482) + 224S(t-1) < 0. +``` + +This also covers k=S=0. Combining the two ranges and the dominance +reduction excludes every `0.0030217759<=C<1` in the stated family. + +## Implication and limits + +The existing p16 allocation already attains this family's best raw crossing +with the frozen round-three inventory. More pair counts, asymmetric splits, +partial thinning, or mixtures of even and odd full stages cannot beat it. +The scope does not cover changed idle masks outside the prefix/suffix contract, +changed scalar words, nonbinary replacements, altered queries, different local +profiles, noncommuting stage actions, or a different supplier interface. + +No new kappa, selected-frontier change, BIT improvement, compiler admission, +absolute-phase proof, physical implementation or multiplication theorem follows. +The remaining productive direction is to change one of those hypotheses. +Credit Cao Yifan and the source's full PR4470/native/controller lineage, +including Cinna Davis, zxv, Jacob Alan Sussman and the retained predecessors. diff --git a/research/controller-thinning-global-ceiling/README.md b/research/controller-thinning-global-ceiling/README.md new file mode 100644 index 0000000000..545d802ad8 --- /dev/null +++ b/research/controller-thinning-global-ceiling/README.md @@ -0,0 +1,51 @@ +# Arbitrary stage thinning cannot improve the retained p16 moment + +**No new kappa.** With Cao Yifan's frozen PR4610 round-three local profile, +the retained paired-path moment has its best raw crossing in +**(0.0030217758, 0.0030217759)**, attained by the existing p16 controller. +The result covers every pair count, every prefix/suffix split and every +binary choice of full versus query-only stages, under the stated endpoint +contract. It is a written infinite-family reduction with an exact arithmetic +certificate, rather than an optimality inference from a finite search. + +Read [PROOF.md](PROOF.md) for the hypotheses and proof. Three concavity +moves reduce every stage mask to eight canonical families. Their surplus +sequences are discretely concave, so exact adjacent differences certify +their maxima over all pair counts. A separate derivative and small-exponent +bound excludes every larger saving C<1. Changed words, idle topologies, +query alphabets and local profiles remain open. + +The source binding checks the literal path's rational projector identities and +all 12,744 full/thin stage subsets, for every split through p5. This bounded +operator check supports the invoice binding; the proof supplies the infinite +claim. It does not prove native or absolute-phase admission for unexecuted words. + +Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json) +and [FROZEN-SOURCE.json](FROZEN-SOURCE.json). The PR4610 arithmetic is retained +byte for byte, including its original line endings. We use its local profile +as the theorem's fixed input, without adopting every claim in that artifact. + +```sh +python3.12 -B scripts/research_package.py --package research/controller-thinning-global-ceiling +``` + +The registered replay requires Python 3.12 and the standard library only. +It verifies the committed [RESULT.json](RESULT.json), source/profile pins, +outward rational intervals and charge controls. `--write` regenerates the +receipt and is an authoring command, not the publication replay. + +No selected record, BIT construction, compiler, production verifier or +canonical mathematical source is changed. This establishes no higher K, +unconditional multiplication theorem or independent human acceptance. + +## Open next questions + +Find a profitable change outside the retained path: a different scalar word, +idle topology, nonbinary replacement or native query interface. First emit its +complete endpoint contract and paid/target moment. An optimistic moment gain +is a reason for native replay, not supplier admission. + +Credit Cao Yifan (PR4610), Cinna Davis and the cumulative PR4470/controller +lineage, zxv, Jacob Alan Sussman, and all retained source authors. Prepared +for Cinna Davis with substantial OpenAI Codex assistance; no subagents. +Apache-2.0. See PROOF.md for precise scope and predecessor credit. diff --git a/research/controller-thinning-global-ceiling/RESULT.json b/research/controller-thinning-global-ceiling/RESULT.json new file mode 100644 index 0000000000..7fd929c39c --- /dev/null +++ b/research/controller-thinning-global-ceiling/RESULT.json @@ -0,0 +1,219 @@ +{ + "canonical_maxima": [ + { + "flags": [ + 0, + 0, + 0 + ], + "following_difference": { + "lower": "-0.081259960753640189239502236922", + "upper": "-0.081259960753640189239502236921" + }, + "previous_difference": { + "lower": "0.282017688477600448025204453377", + "upper": "0.282017688477600448025204453378" + }, + "side_windows": 18, + "sides": [ + 9, + 9 + ], + "surplus": { + "lower": "-7.780986677904772171993008083067", + "upper": "-7.780986677904772171993008083066" + } + }, + { + "flags": [ + 1, + 0, + 0 + ], + "following_difference": { + "lower": "-0.081259960753640189239502236922", + "upper": "-0.081259960753640189239502236921" + }, + "previous_difference": { + "lower": "0.282017688477600448025204453377", + "upper": "0.282017688477600448025204453378" + }, + "side_windows": 17, + "sides": [ + 8, + 9 + ], + "surplus": { + "lower": "-5.664970652517184212649039376361", + "upper": "-5.664970652517184212649039376360" + } + }, + { + "flags": [ + 0, + 1, + 0 + ], + "following_difference": { + "lower": "-0.081259960753640189239502236922", + "upper": "-0.081259960753640189239502236921" + }, + "previous_difference": { + "lower": "0.282017688477600448025204453377", + "upper": "0.282017688477600448025204453378" + }, + "side_windows": 17, + "sides": [ + 9, + 8 + ], + "surplus": { + "lower": "-5.664970652517184212649039376361", + "upper": "-5.664970652517184212649039376360" + } + }, + { + "flags": [ + 1, + 1, + 0 + ], + "following_difference": { + "lower": "-0.081259960753640189239502236922", + "upper": "-0.081259960753640189239502236921" + }, + "previous_difference": { + "lower": "0.282017688477600448025204453377", + "upper": "0.282017688477600448025204453378" + }, + "side_windows": 16, + "sides": [ + 8, + 8 + ], + "surplus": { + "lower": "-3.548954627129596253305070669654", + "upper": "-3.548954627129596253305070669653" + } + }, + { + "flags": [ + 0, + 0, + 1 + ], + "following_difference": { + "lower": "-0.011543266237527041426701826571", + "upper": "-0.011543266237527041426701826570" + }, + "previous_difference": { + "lower": "0.282017688477600448025204453377", + "upper": "0.282017688477600448025204453378" + }, + "side_windows": 17, + "sides": [ + 9, + 8 + ], + "surplus": { + "lower": "-4.232039275456939754330616141324", + "upper": "-4.232039275456939754330616141323" + } + }, + { + "flags": [ + 1, + 0, + 1 + ], + "following_difference": { + "lower": "-0.011543266237527041426701826571", + "upper": "-0.011543266237527041426701826570" + }, + "previous_difference": { + "lower": "0.282017688477600448025204453377", + "upper": "0.282017688477600448025204453378" + }, + "side_windows": 16, + "sides": [ + 8, + 8 + ], + "surplus": { + "lower": "-2.116023250069351794986647434617", + "upper": "-2.116023250069351794986647434616" + } + }, + { + "flags": [ + 0, + 1, + 1 + ], + "following_difference": { + "lower": "-0.011543266237527041426701826571", + "upper": "-0.011543266237527041426701826570" + }, + "previous_difference": { + "lower": "0.282017688477600448025204453377", + "upper": "0.282017688477600448025204453378" + }, + "side_windows": 16, + "sides": [ + 9, + 7 + ], + "surplus": { + "lower": "-2.116023250069351794986647434617", + "upper": "-2.116023250069351794986647434616" + } + }, + { + "flags": [ + 1, + 1, + 1 + ], + "following_difference": { + "lower": "-0.011543266237527041426701826571", + "upper": "-0.011543266237527041426701826570" + }, + "previous_difference": { + "lower": "0.282017688477600448025204453377", + "upper": "0.282017688477600448025204453378" + }, + "side_windows": 15, + "sides": [ + 8, + 7 + ], + "surplus": { + "lower": "-0.000007224681763835642678727911", + "upper": "-0.000007224681763835642678727910" + } + } + ], + "controls": [ + "charged queries", + "strict even-to-odd swap", + "source and profile pins" + ], + "exact_source_masks_checked": 12744, + "local_derivative_upper": { + "lower": "-9.534824922458622507134205148508", + "upper": "-9.534824922458622507134205148507" + }, + "lower_endpoint_surplus": { + "lower": "0.000017497552532353535072733660", + "upper": "0.000017497552532353535072733661" + }, + "new_kappa": false, + "proof": "PROOF.md supplies infinite-family dominance and concavity", + "raw_root_bracket": [ + "15108879/5000000000", + "30217759/10000000000" + ], + "scope": "All pair counts, prefix/suffix splits, and binary full-stage subsets of the retained path", + "source_pr": 4610, + "status": "PASS_GLOBAL_PAIRED_PATH_THINNING_CEILING" +} diff --git a/research/controller-thinning-global-ceiling/SOURCES.json b/research/controller-thinning-global-ceiling/SOURCES.json new file mode 100644 index 0000000000..af0ca540d7 --- /dev/null +++ b/research/controller-thinning-global-ceiling/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497" + }, + { + "path": "research/query-thinned-controllers/controller.py", + "usage": "input", + "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583", + "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + } + ] +} diff --git a/research/controller-thinning-global-ceiling/TASK.json b/research/controller-thinning-global-ceiling/TASK.json new file mode 100644 index 0000000000..f08251c61b --- /dev/null +++ b/research/controller-thinning-global-ceiling/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a global raw-moment ceiling for arbitrary full/query thinning in the retained paired-path controller, with the PR4610 round-three local profile.", + "scope_change_reason": "User explicitly requests a much higher K and a bottleneck breakthrough. Replace more stage-mask search with an infinite-family dominance theorem to identify the required architectural change.", + "bottleneck_link": "Whole-idle work dominates the current budget. This theorem exhausts all pair counts and binary stage-thinning choices under the retained path endpoint contract, requiring a changed word or interface for a larger raw K.", + "budget_minutes": 60, + "stop_rule": "Finish the infinite-family reduction, exact maxima and exponent-range bounds, source binding, mutation controls and publication; do not infer a global architecture barrier.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, frozen PR4610 arithmetic, and verify.py", + "author": "Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, implementation and checking; no subagents, independent human review or formal proof assistant.", + "open_questions": [ + { + "question": "Can a changed scalar word, idle topology, or native query interface exceed the path ceiling?", + "why_it_matters": "All binary stage-thinning and pair-count changes in this family are exhausted by the proved ceiling.", + "first_step": "Emit a changed operator word and compare its fully charged mixed moment before expensive native/phase reconstruction.", + "blocked_by": "No profitable changed topology established here." + } + ] +} diff --git a/research/controller-thinning-global-ceiling/VERIFY.json b/research/controller-thinning-global-ceiling/VERIFY.json new file mode 100644 index 0000000000..0f771ceb31 --- /dev/null +++ b/research/controller-thinning-global-ceiling/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/higher-moment-strictification/verify.py", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/query-thinned-controllers/controller.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Source/profile pins, exact rational interval all-family ceiling, literal source projectors and every stage subset through p5, and rejecting charge/profile controls." + } + ] +} diff --git a/research/controller-thinning-global-ceiling/inputs/PR4610-ARITHMETIC.json b/research/controller-thinning-global-ceiling/inputs/PR4610-ARITHMETIC.json new file mode 100644 index 0000000000..9400a8f178 --- /dev/null +++ b/research/controller-thinning-global-ceiling/inputs/PR4610-ARITHMETIC.json @@ -0,0 +1,241 @@ +{ + "compiler": { + "H": 31385200000000, + "N": "2^31385200000000", + "eta": { + "lower": "0.000000204541256425394083726654", + "upper": "0.000000204541256425394083726655" + }, + "gap": "1/700000000", + "integer_test_exponent": 44836, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "1057619/350000000", + "word_materialized": false + }, + "gain_over_PR4535": "319/200000000", + "kappa": "9443/3125000", + "local_helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "local_paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "margin_at_old_root_upper": [ + "78072058023577019965454984044224523228758899702419408235/196159429230833773869868419475239575503198607639501078528", + "1249152928377232319447279744707592371660142395238823308861/3138550867693340381917894711603833208051177722232017256448" + ], + "native_receipt_sha256": "eec3b14241430b6c9f5de3cbf0e3d45a172d8071d2dccd2b59d56a1fbac3d428", + "negative_controls": { + "closed_epsilon": [ + "epsilon_below_one", + "global_gamma_power_slack", + "actual_logarithmic_gamma_guard", + "source_axis_superpolynomial", + "gaussian_above_main", + "new_semantic_guard_with_C1_one" + ], + "closed_uniform": [ + "new_complex_uniform_saving_above_b" + ], + "old_BIT": [ + "actual_bit_above_effective" + ], + "unfunded_endpoint": [ + "main_transform_above_kappa", + "global_coordinate_router_above_kappa", + "fused_gaussian_above_kappa", + "group_bit_router_above_kappa", + "boundary_algebraic_matrix_above_kappa" + ] + }, + "nonrecursive": { + "local_routes": 4802000, + "local_scalar": 158168, + "raw_scalar_upper": 181098496 + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "174299999253/175000000000", + "fixed_halo_explicit_metadata_branch": "13475000001/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", + "new_semantic_group_guard": "3/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "296133039576953/98000000000000000", + "fused_gaussian": "296133038730859/98000000000000000", + "global_coordinate_router": "528809/175000000", + "group_bit_router": "370166473413573/122500000000000000", + "group_scans": "349999999/350000000", + "main_transform": "296132899576953/98000000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "40108633039576953/98000000000000000" + }, + "parameters": { + "a": "528809/175000000", + "b": "2115237/700000000", + "beta": "699999997/700000000", + "bit_saving": "17/5000", + "cap_xi": "89108632899576953/98000000000000000", + "complex_uniform_saving": "1057619/350000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "9443/3125000", + "lambda_": "199395647/200000000", + "lambda_prime": "139576953/140000000", + "layout": "1/700000000", + "q": "423047/140000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "302177/100000000" + }, + "strict_checks": { + "actual_bit_above_effective": "66191/175000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "8891367310423047/49000000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "559576953/98000000000000000", + "cap_above_band": "40108632899576953/98000000000000000", + "cap_below_cell": "8891366960423047/98000000000000000", + "cap_below_phase_cell_power": "106891367100423047/98000000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "19759763/700000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "558730859/98000000000000000", + "gaussian_above_main": "69576953/49000000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "873413573/122500000000000000", + "group_gauge_power_slack": "8891367303423047/49000000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "348942383/350000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "645394790400418148631/500000000000000000000000", + "lambda_above_internal": "1/1400000000", + "lambda_above_sigma": "3/1400000000", + "lambda_above_tau": "1/1400000000", + "lambda_prime_above_lambda": "1/1400000000", + "lambda_prime_above_leaf": "1397884763/490000000000000000", + "leaf_saving_above_effective": "697884763/490000000000000000", + "main_transform_above_kappa": "419576953/98000000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "13474471193/175000000", + "microbox_halo_volume": "55300000003/700000000", + "new_complex_uniform_saving_above_b": "1/700000000", + "new_semantic_guard_with_C1_one": "1/700000000", + "polynomial_products_above_kappa": "697884767/700000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "1397884763/490000000000000000", + "q_positive": "423047/140000000", + "short_record_fallback": "697884763/700000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "39812500559576953/98000000000000000", + "stop_below_one": "699999999/700000000", + "stop_positive": "1/700000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/700000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/700000000", + "union_tag_work_per_visit_fits_record": "3/700000000" + } + }, + "paid": { + "1": 41298, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 144 + }, + "paid_calls": 64404, + "productive_fields": 10928, + "rank_mass_surplus": 752, + "raw_root_interval": [ + "15108879/5000000000", + "30217759/10000000000" + ], + "scope": "Exact changed-profile arithmetic only. Requires separately admitted changed native programs, paid transports and absolute phases. Retained compiler/native/precision/tape/analytic/recovery assumptions.", + "source_sha256": { + "research/fresh-helper-boundary/native.py": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "research/joint-helper-lattice/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", + "research/joint-helper-lattice/native_joint.py": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46", + "research/joint-helper-lattice/verify.py": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "research/kappa-interface-round2-20261022/price_profile.py": "adde619968d3ac37147d239e25145b28150650e9ce0f76035f680f22589adcbb", + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + }, + "status": "PASS_CHANGED_PROFILE_ARITHMETIC_NATIVE_ADMISSION_SEPARATE", + "strictification": { + "alpha": { + "lower": "0.999999993884252622740095906769", + "upper": "0.999999993884252622740095906770" + }, + "cutoff": 20, + "delta": { + "lower": "0.958285305508943939401236992035", + "upper": "0.958285305508943939401236992036" + }, + "floor": 21, + "gamma": { + "lower": "0.956217506703714253758457710273", + "upper": "0.956217506703714253758457710274" + }, + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "tail_offset": "1/5", + "tested": "302177/100000000" + }, + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5868 + } +} diff --git a/research/controller-thinning-global-ceiling/verify.py b/research/controller-thinning-global-ceiling/verify.py new file mode 100644 index 0000000000..a5a478914b --- /dev/null +++ b/research/controller-thinning-global-ceiling/verify.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +"""Exact paired-path thinning bound. Apache-2.0; OpenAI Codex assistance. + +PROOF.md supplies the infinite-family argument; the census is a source check. +""" +import argparse +import ast +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha1, sha256 +import importlib.util +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +UPPER, LOWER = Q('0.0030217759'), Q('0.0030217758') +V, D = 112, 8 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticate(): + for row in json.loads((HERE/'SOURCES.json').read_text())['files']: + if row['usage'] == 'input': + need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], + 'Live source pin: '+row['path']) + row = json.loads((HERE/'FROZEN-SOURCE.json').read_text()) + raw = (HERE/row['snapshot']).read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'Frozen PR4610 bytes') + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], + 'Frozen PR4610 Git blob identity') + source = json.loads(raw) + h = {int(k): n for k, n in source['local_helpers'].items()} + p = {int(k): n for k, n in source['local_paid'].items()} + need(h == {4:28, 7:7, 8:47, 9:326}, 'Named productive profile') + need(p == {1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}, 'Named paid profile') + return h, p + + +def interval_engine(): + path = ROOT/'research/higher-moment-strictification/verify.py' + spec = importlib.util.spec_from_file_location('thinning_exact_intervals', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def add(*intervals): + return tuple(sum(x[i] for x in intervals) for i in (0, 1)) + + +def optimal_sides(count, left, right): + a = b = 0 + indices = [] + for _ in range(count): + if left+a+1 <= right+b+1: + a += 1 + indices.append(left+a) + else: + b += 1 + indices.append(right+b) + return a, b, indices + + +def canonical(E, H, P, count, flags, saving): + t, k = 1-saving, count+sum(flags) + a, b, indices = optimal_sides(count, *flags[:2]) + local = add(E.moment(H, t), E.scale(E.moment(P, t), -1)) + terms = [E.power(1+D*k, t)] + for j in indices: + terms.append(add(E.power(1+D*j, t), E.scale(E.power(D*j, t), -1))) + return add(E.scale(local, k), E.scale(add(*terms), 2*V), + (Q(-V*(2*count+3-k)),)*2), (a, b) + + +def inverse(a): + n = len(a) + w = [list(map(Q, row))+[Q(i == j) for j in range(n)] for i, row in enumerate(a)] + for j in range(n): + pivot = next(i for i in range(j, n) if w[i][j]) + w[j], w[pivot] = w[pivot], w[j] + w[j] = [x/w[j][j] for x in w[j]] + for i in range(n): + if i != j: + c = w[i][j] + w[i] = [x-c*y for x, y in zip(w[i], w[j])] + return [row[n:] for row in w] + + +def matmul(a, b): + return [[sum(x*y for x, y in zip(row, col)) for col in zip(*b)] for row in a] + + +def source_functions(path, names): + tree = ast.parse(path.read_text()) + tree.body = [n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name in names] + need(len(tree.body) == len(names), 'Exact named source functions') + env = {'Q': Q} + exec(compile(tree, str(path), 'exec'), env) + return env + + +def finite_source_binding(): + source = source_functions(ROOT/'research/kappa-rebuild/bit/complex_controller_factor.py', + {'plus', 'monomial_times', 'controller'}) + mask = source_functions(ROOT/'research/query-thinned-controllers/controller.py', {'keep_mask'})['keep_mask'] + cases = 0 + for p in range(1, 6): + for a in range(p): + b = p-1-a + coefficients, _, idles = source['controller'](p, mask(p, a)) + n = 2*p + total = [[sum(m[i][j] for m in coefficients.values()) for j in range(n)] for i in range(n)] + inv = inverse(total) + projectors = {key:matmul(inv, matrix) for key, matrix in coefficients.items()} + for key, projection in projectors.items(): + need(matmul(projection, projection) == projection, 'Literal source projector') + need(sum(projection[i][i] for i in range(n)) == 1, 'Rank-one source projector') + for other, second in projectors.items(): + if key != other: + need(not any(any(row) for row in matmul(projection, second)), 'Orthogonal source projectors') + expected = [set(range(2*p+1))]+[set(range(2*j+1)) for j in range(1, a+1)] + expected += [set(range(2*p-2*j, 2*p+1)) for j in range(1, b+1)] + actual = Counter(tuple(i for i, v in enumerate(key[1:]) if v) for key in projectors) + need(actual == Counter({tuple(sorted(s)):2 for s in expected}), 'Source diagonal stage sets') + for bits in product((0, 1), repeat=2*p+1): + full = {j for j, x in enumerate(bits) if x} + main = Counter(1+D*len(full.intersection(s)) for s in expected) + idle = Counter(D*len(full.intersection(row['stages'])) for row in idles if row['retained']) + idle.pop(0, None) + other_main, other_idle = Counter({1+D*sum(bits):1}), Counter() + for end, length, reverse in [(bits[0], a, False), (bits[-1], b, True)]: + c = end + for j in range(1, length+1): + odd, even = ((2*p-2*j+1, 2*p-2*j) if reverse else (2*j-1, 2*j)) + o, e = bits[odd], bits[even] + other_main[1+D*(c+o+e)] += 1 + if c+o: + other_idle[D*(c+o)] += 1 + c += o+e + other_idle[D] += sum(bits[2:2*p:2]) + other_idle += Counter() + need(main == other_main and idle == other_idle, 'Full arbitrary-mask invoice binding') + surplus = 2*V*(sum(r*n for r, n in main.items())-sum(r*n for r, n in idle.items())) + surplus -= 1856*sum(bits)+V*(2*p+1-sum(bits)) + need(surplus == 48*sum(bits)-V, 'Rank mass includes every thin query') + cases += 1 + return cases + + +def certify(): + H, P = authenticate() + E = interval_engine() + derivative = (Q(0), Q(0)) + for r, n in {2:412, 3:510, 4:99, 5:40}.items(): + term = E.mul(E.divide(E.power(r, Q(1,4)), E.power(9, Q(1,4))), E.log_bounds(r)) + derivative = add(derivative, E.scale(term, n)) + for r, n in {7:7, 8:39, 9:326}.items(): + derivative = add(derivative, E.scale(E.log_bounds(r), -Q(n*r, 9))) + need(derivative[1] < 0, 'Uniform local derivative sign on [1/4,1]') + need(sum(P.values())-2*sum(H.values()) == 2482 > V+2*V*D*Q(1,4), + 'All 0> j) & 1 for j in range(3)) + current, sides = canonical(E, H, P, count, flags, UPPER) + previous, _ = canonical(E, H, P, count-1, flags, UPPER) + following, _ = canonical(E, H, P, count+1, flags, UPPER) + need(current[0] > previous[1] and current[0] > following[1], 'Discrete concave maximum') + need(current[1] < 0, 'Entire canonical family fails at upper endpoint') + maxima.append({'flags':flags, 'side_windows':count, 'sides':sides, + 'surplus':E.display(current), + 'previous_difference':E.display(add(current, E.scale(previous, -1))), + 'following_difference':E.display(add(following, E.scale(current, -1)))}) + low, _ = canonical(E, H, P, 15, (1,1,1), LOWER) + need(low[0] > 0, 'Tight lower endpoint from p16') + high, _ = canonical(E, H, P, 15, (1,1,1), UPPER) + need(high[0]+15*V > 0, 'Control: unpaid queries would falsely pass') + swap = add(E.power(8, Q(1,2)), E.power(8, Q(1,2)), E.scale(E.power(16,Q(1,2)), -1)) + need(swap[0] > 0, 'Strict even-to-odd swap control') + return {'status':'PASS_GLOBAL_PAIRED_PATH_THINNING_CEILING', 'source_pr':4610, + 'scope':'All pair counts, prefix/suffix splits, and binary full-stage subsets of the retained path', + 'raw_root_bracket':[str(LOWER), str(UPPER)], 'new_kappa':False, + 'local_derivative_upper':E.display(derivative), 'canonical_maxima':maxima, + 'lower_endpoint_surplus':E.display(low), 'exact_source_masks_checked':finite_source_binding(), + 'controls':['charged queries', 'strict even-to-odd swap', 'source and profile pins'], + 'proof':'PROOF.md supplies infinite-family dominance and concavity'} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = certify() + if args.write: + (HERE/'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + need(json.loads((HERE/'RESULT.json').read_text()) == result, 'Committed exact receipt') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main() From 3bd50bfa55d9c85a4d6e3a3fd8805fdaebe8dca1 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Thu, 22 Oct 2026 09:31:01 -0500 Subject: [PATCH 2/5] Preserve frozen CRLF source bytes and compare canonical JSON receipts --- .../.gitattributes | 1 + .../inputs/PR4610-ARITHMETIC.json | 482 +++++++++--------- .../verify.py | 3 +- 3 files changed, 244 insertions(+), 242 deletions(-) create mode 100644 research/controller-thinning-global-ceiling/.gitattributes diff --git a/research/controller-thinning-global-ceiling/.gitattributes b/research/controller-thinning-global-ceiling/.gitattributes new file mode 100644 index 0000000000..59b4922b2f --- /dev/null +++ b/research/controller-thinning-global-ceiling/.gitattributes @@ -0,0 +1 @@ +inputs/PR4610-ARITHMETIC.json -text diff --git a/research/controller-thinning-global-ceiling/inputs/PR4610-ARITHMETIC.json b/research/controller-thinning-global-ceiling/inputs/PR4610-ARITHMETIC.json index 9400a8f178..c89e009ca4 100644 --- a/research/controller-thinning-global-ceiling/inputs/PR4610-ARITHMETIC.json +++ b/research/controller-thinning-global-ceiling/inputs/PR4610-ARITHMETIC.json @@ -1,241 +1,241 @@ -{ - "compiler": { - "H": 31385200000000, - "N": "2^31385200000000", - "eta": { - "lower": "0.000000204541256425394083726654", - "upper": "0.000000204541256425394083726655" - }, - "gap": "1/700000000", - "integer_test_exponent": 44836, - "logarithm_power": 1000, - "theta": "63/64", - "uniform_saving": "1057619/350000000", - "word_materialized": false - }, - "gain_over_PR4535": "319/200000000", - "kappa": "9443/3125000", - "local_helpers": { - "4": 28, - "7": 7, - "8": 47, - "9": 326 - }, - "local_paid": { - "1": 2201, - "2": 412, - "3": 510, - "4": 127, - "5": 40, - "8": 8 - }, - "margin_at_old_root_upper": [ - "78072058023577019965454984044224523228758899702419408235/196159429230833773869868419475239575503198607639501078528", - "1249152928377232319447279744707592371660142395238823308861/3138550867693340381917894711603833208051177722232017256448" - ], - "native_receipt_sha256": "eec3b14241430b6c9f5de3cbf0e3d45a172d8071d2dccd2b59d56a1fbac3d428", - "negative_controls": { - "closed_epsilon": [ - "epsilon_below_one", - "global_gamma_power_slack", - "actual_logarithmic_gamma_guard", - "source_axis_superpolynomial", - "gaussian_above_main", - "new_semantic_guard_with_C1_one" - ], - "closed_uniform": [ - "new_complex_uniform_saving_above_b" - ], - "old_BIT": [ - "actual_bit_above_effective" - ], - "unfunded_endpoint": [ - "main_transform_above_kappa", - "global_coordinate_router_above_kappa", - "fused_gaussian_above_kappa", - "group_bit_router_above_kappa", - "boundary_algebraic_matrix_above_kappa" - ] - }, - "nonrecursive": { - "local_routes": 4802000, - "local_scalar": 158168, - "raw_scalar_upper": 181098496 - }, - "ordinary_BIT": { - "admitted": "17/5000", - "after_cover": "69/20000", - "atom": "1/250", - "before_cover": "3459/1000000", - "ordinary_saving": "8590884599/2500000000000", - "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" - }, - "outer": { - "functional_checks": { - "actual_new_BIT_stock_sublinear": "174299999253/175000000000", - "fixed_halo_explicit_metadata_branch": "13475000001/175000000", - "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", - "new_semantic_group_guard": "3/700000000" - }, - "margins": { - "boundary_algebraic_matrix": "296133039576953/98000000000000000", - "fused_gaussian": "296133038730859/98000000000000000", - "global_coordinate_router": "528809/175000000", - "group_bit_router": "370166473413573/122500000000000000", - "group_scans": "349999999/350000000", - "main_transform": "296132899576953/98000000000000000", - "microbox_face_corrections": "13475000001/175000000", - "polynomial_products": "699999999/700000000", - "sparse_union_movement": "40108633039576953/98000000000000000" - }, - "parameters": { - "a": "528809/175000000", - "b": "2115237/700000000", - "beta": "699999997/700000000", - "bit_saving": "17/5000", - "cap_xi": "89108632899576953/98000000000000000", - "complex_uniform_saving": "1057619/350000000", - "d": "1/700000000", - "epsilon": "699999999/700000000", - "kappa": "9443/3125000", - "lambda_": "199395647/200000000", - "lambda_prime": "139576953/140000000", - "layout": "1/700000000", - "q": "423047/140000000", - "r0": "1/7000000000", - "stop": "1/700000000", - "tested_saving": "302177/100000000" - }, - "strict_checks": { - "actual_bit_above_effective": "66191/175000000", - "actual_logarithmic_gamma_guard": "1/700000000", - "actual_logarithmic_group_guard": "8891367310423047/49000000000000000", - "alpha_logarithm_absorption": "1/7000000000", - "boundary_algebraic_matrix_above_kappa": "559576953/98000000000000000", - "cap_above_band": "40108632899576953/98000000000000000", - "cap_below_cell": "8891366960423047/98000000000000000", - "cap_below_phase_cell_power": "106891367100423047/98000000000000000", - "complex_above_effective": "1/700000000", - "complex_below_one_over_32": "19759763/700000000", - "complex_endpoint": "1/350000000", - "epsilon_below_one": "1/700000000", - "epsilon_positive": "699999999/700000000", - "fine_prime_halo_umbrella": "7/2", - "fused_gaussian_above_kappa": "558730859/98000000000000000", - "gaussian_above_main": "69576953/49000000000000000", - "global_coordinate_router_above_kappa": "1/175000000", - "global_gamma_power_slack": "9/7000000000", - "group_below_dimension": "1/350000000", - "group_bit_router_above_kappa": "873413573/122500000000000000", - "group_gauge_power_slack": "8891367303423047/49000000000000000", - "group_key_fits_record": "1/350000000", - "group_positive": "699999997/700000000", - "group_scans_above_kappa": "348942383/350000000", - "halo_covers_generic_inverse_radius": "5", - "improvement_over_user_baseline": "645394790400418148631/500000000000000000000000", - "lambda_above_internal": "1/1400000000", - "lambda_above_sigma": "3/1400000000", - "lambda_above_tau": "1/1400000000", - "lambda_prime_above_lambda": "1/1400000000", - "lambda_prime_above_leaf": "1397884763/490000000000000000", - "leaf_saving_above_effective": "697884763/490000000000000000", - "main_transform_above_kappa": "419576953/98000000000000000", - "membership_arithmetic_fits_record": "1/700000000", - "microbox_face_corrections_above_kappa": "13474471193/175000000", - "microbox_halo_volume": "55300000003/700000000", - "new_complex_uniform_saving_above_b": "1/700000000", - "new_semantic_guard_with_C1_one": "1/700000000", - "polynomial_products_above_kappa": "697884767/700000000", - "positive_layout_slack": "1/700000000", - "q_below_effective": "1/700000000", - "q_below_internal": "1/700000000", - "q_below_leaf": "1397884763/490000000000000000", - "q_positive": "423047/140000000", - "short_record_fallback": "697884763/700000000", - "source_axis_superpolynomial": "1/700000000", - "sparse_union_movement_above_kappa": "39812500559576953/98000000000000000", - "stop_below_one": "699999999/700000000", - "stop_positive": "1/700000000", - "strassen_integer_power_gap": "1951441519231", - "support_router_span": "3/700000000", - "theta_positive_polynomial_power": "2", - "union_header_fits_record": "3/700000000", - "union_tag_work_per_visit_fits_record": "3/700000000" - } - }, - "paid": { - "1": 41298, - "16": 448, - "2": 7416, - "24": 448, - "3": 9180, - "32": 448, - "4": 2286, - "40": 448, - "48": 448, - "5": 720, - "56": 448, - "64": 448, - "72": 224, - "8": 144 - }, - "paid_calls": 64404, - "productive_fields": 10928, - "rank_mass_surplus": 752, - "raw_root_interval": [ - "15108879/5000000000", - "30217759/10000000000" - ], - "scope": "Exact changed-profile arithmetic only. Requires separately admitted changed native programs, paid transports and absolute phases. Retained compiler/native/precision/tape/analytic/recovery assumptions.", - "source_sha256": { - "research/fresh-helper-boundary/native.py": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", - "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", - "research/joint-helper-lattice/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", - "research/joint-helper-lattice/native_joint.py": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46", - "research/joint-helper-lattice/verify.py": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f", - "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", - "research/kappa-interface-round2-20261022/price_profile.py": "adde619968d3ac37147d239e25145b28150650e9ce0f76035f680f22589adcbb", - "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", - "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", - "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", - "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", - "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", - "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" - }, - "status": "PASS_CHANGED_PROFILE_ARITHMETIC_NATIVE_ADMISSION_SEPARATE", - "strictification": { - "alpha": { - "lower": "0.999999993884252622740095906769", - "upper": "0.999999993884252622740095906770" - }, - "cutoff": 20, - "delta": { - "lower": "0.958285305508943939401236992035", - "upper": "0.958285305508943939401236992036" - }, - "floor": 21, - "gamma": { - "lower": "0.956217506703714253758457710273", - "upper": "0.956217506703714253758457710274" - }, - "normalized_paid_upper": "2097152001953127/2097154147483648", - "power": 1024, - "tail_offset": "1/5", - "tested": "302177/100000000" - }, - "targets": { - "145": 224, - "17": 448, - "25": 448, - "33": 448, - "4": 504, - "41": 448, - "49": 448, - "57": 448, - "65": 448, - "7": 126, - "73": 224, - "8": 846, - "9": 5868 - } -} +{ + "compiler": { + "H": 31385200000000, + "N": "2^31385200000000", + "eta": { + "lower": "0.000000204541256425394083726654", + "upper": "0.000000204541256425394083726655" + }, + "gap": "1/700000000", + "integer_test_exponent": 44836, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "1057619/350000000", + "word_materialized": false + }, + "gain_over_PR4535": "319/200000000", + "kappa": "9443/3125000", + "local_helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "local_paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "margin_at_old_root_upper": [ + "78072058023577019965454984044224523228758899702419408235/196159429230833773869868419475239575503198607639501078528", + "1249152928377232319447279744707592371660142395238823308861/3138550867693340381917894711603833208051177722232017256448" + ], + "native_receipt_sha256": "eec3b14241430b6c9f5de3cbf0e3d45a172d8071d2dccd2b59d56a1fbac3d428", + "negative_controls": { + "closed_epsilon": [ + "epsilon_below_one", + "global_gamma_power_slack", + "actual_logarithmic_gamma_guard", + "source_axis_superpolynomial", + "gaussian_above_main", + "new_semantic_guard_with_C1_one" + ], + "closed_uniform": [ + "new_complex_uniform_saving_above_b" + ], + "old_BIT": [ + "actual_bit_above_effective" + ], + "unfunded_endpoint": [ + "main_transform_above_kappa", + "global_coordinate_router_above_kappa", + "fused_gaussian_above_kappa", + "group_bit_router_above_kappa", + "boundary_algebraic_matrix_above_kappa" + ] + }, + "nonrecursive": { + "local_routes": 4802000, + "local_scalar": 158168, + "raw_scalar_upper": 181098496 + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "174299999253/175000000000", + "fixed_halo_explicit_metadata_branch": "13475000001/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", + "new_semantic_group_guard": "3/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "296133039576953/98000000000000000", + "fused_gaussian": "296133038730859/98000000000000000", + "global_coordinate_router": "528809/175000000", + "group_bit_router": "370166473413573/122500000000000000", + "group_scans": "349999999/350000000", + "main_transform": "296132899576953/98000000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "40108633039576953/98000000000000000" + }, + "parameters": { + "a": "528809/175000000", + "b": "2115237/700000000", + "beta": "699999997/700000000", + "bit_saving": "17/5000", + "cap_xi": "89108632899576953/98000000000000000", + "complex_uniform_saving": "1057619/350000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "9443/3125000", + "lambda_": "199395647/200000000", + "lambda_prime": "139576953/140000000", + "layout": "1/700000000", + "q": "423047/140000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "302177/100000000" + }, + "strict_checks": { + "actual_bit_above_effective": "66191/175000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "8891367310423047/49000000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "559576953/98000000000000000", + "cap_above_band": "40108632899576953/98000000000000000", + "cap_below_cell": "8891366960423047/98000000000000000", + "cap_below_phase_cell_power": "106891367100423047/98000000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "19759763/700000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "558730859/98000000000000000", + "gaussian_above_main": "69576953/49000000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "873413573/122500000000000000", + "group_gauge_power_slack": "8891367303423047/49000000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "348942383/350000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "645394790400418148631/500000000000000000000000", + "lambda_above_internal": "1/1400000000", + "lambda_above_sigma": "3/1400000000", + "lambda_above_tau": "1/1400000000", + "lambda_prime_above_lambda": "1/1400000000", + "lambda_prime_above_leaf": "1397884763/490000000000000000", + "leaf_saving_above_effective": "697884763/490000000000000000", + "main_transform_above_kappa": "419576953/98000000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "13474471193/175000000", + "microbox_halo_volume": "55300000003/700000000", + "new_complex_uniform_saving_above_b": "1/700000000", + "new_semantic_guard_with_C1_one": "1/700000000", + "polynomial_products_above_kappa": "697884767/700000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "1397884763/490000000000000000", + "q_positive": "423047/140000000", + "short_record_fallback": "697884763/700000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "39812500559576953/98000000000000000", + "stop_below_one": "699999999/700000000", + "stop_positive": "1/700000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/700000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/700000000", + "union_tag_work_per_visit_fits_record": "3/700000000" + } + }, + "paid": { + "1": 41298, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 144 + }, + "paid_calls": 64404, + "productive_fields": 10928, + "rank_mass_surplus": 752, + "raw_root_interval": [ + "15108879/5000000000", + "30217759/10000000000" + ], + "scope": "Exact changed-profile arithmetic only. Requires separately admitted changed native programs, paid transports and absolute phases. Retained compiler/native/precision/tape/analytic/recovery assumptions.", + "source_sha256": { + "research/fresh-helper-boundary/native.py": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "research/joint-helper-lattice/CONTROLLER.json": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f", + "research/joint-helper-lattice/native_joint.py": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46", + "research/joint-helper-lattice/verify.py": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "research/kappa-interface-round2-20261022/price_profile.py": "adde619968d3ac37147d239e25145b28150650e9ce0f76035f680f22589adcbb", + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + }, + "status": "PASS_CHANGED_PROFILE_ARITHMETIC_NATIVE_ADMISSION_SEPARATE", + "strictification": { + "alpha": { + "lower": "0.999999993884252622740095906769", + "upper": "0.999999993884252622740095906770" + }, + "cutoff": 20, + "delta": { + "lower": "0.958285305508943939401236992035", + "upper": "0.958285305508943939401236992036" + }, + "floor": 21, + "gamma": { + "lower": "0.956217506703714253758457710273", + "upper": "0.956217506703714253758457710274" + }, + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "tail_offset": "1/5", + "tested": "302177/100000000" + }, + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 846, + "9": 5868 + } +} diff --git a/research/controller-thinning-global-ceiling/verify.py b/research/controller-thinning-global-ceiling/verify.py index a5a478914b..6c11e28135 100644 --- a/research/controller-thinning-global-ceiling/verify.py +++ b/research/controller-thinning-global-ceiling/verify.py @@ -200,7 +200,8 @@ def main(): if args.write: (HERE/'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') else: - need(json.loads((HERE/'RESULT.json').read_text()) == result, 'Committed exact receipt') + need(json.loads((HERE/'RESULT.json').read_text()) == json.loads(json.dumps(result)), + 'Committed exact receipt') print(json.dumps(result, sort_keys=True)) From 00582e77ebb917bdafbe15c4f9c31f85f8aae436 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Thu, 22 Oct 2026 09:33:59 -0500 Subject: [PATCH 3/5] Add actual mutation rejection controls for the thinning certificate --- .../README.md | 4 +- .../VERIFY.json | 9 +++ .../adversarial.py | 65 +++++++++++++++++++ 3 files changed, 77 insertions(+), 1 deletion(-) create mode 100644 research/controller-thinning-global-ceiling/adversarial.py diff --git a/research/controller-thinning-global-ceiling/README.md b/research/controller-thinning-global-ceiling/README.md index 545d802ad8..cc82123420 100644 --- a/research/controller-thinning-global-ceiling/README.md +++ b/research/controller-thinning-global-ceiling/README.md @@ -31,7 +31,9 @@ python3.12 -B scripts/research_package.py --package research/controller-thinning The registered replay requires Python 3.12 and the standard library only. It verifies the committed [RESULT.json](RESULT.json), source/profile pins, -outward rational intervals and charge controls. `--write` regenerates the +outward rational intervals and charge controls. A second replay rejects four +actual source/profile mutations, including an unpaid owned-centre profile +with its hashes maliciously rebound. `--write` regenerates the receipt and is an authoring command, not the publication replay. No selected record, BIT construction, compiler, production verifier or diff --git a/research/controller-thinning-global-ceiling/VERIFY.json b/research/controller-thinning-global-ceiling/VERIFY.json index 0f771ceb31..89a40d73da 100644 --- a/research/controller-thinning-global-ceiling/VERIFY.json +++ b/research/controller-thinning-global-ceiling/VERIFY.json @@ -17,6 +17,15 @@ ], "timeout_seconds": 300, "checks": "Source/profile pins, exact rational interval all-family ceiling, literal source projectors and every stage subset through p5, and rejecting charge/profile controls." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/adversarial.py" + ], + "timeout_seconds": 60, + "checks": "Actual source hash, Git blob, frozen byte and rebound owned-job profile corruptions are rejected." } ] } diff --git a/research/controller-thinning-global-ceiling/adversarial.py b/research/controller-thinning-global-ceiling/adversarial.py new file mode 100644 index 0000000000..eca18e7d1c --- /dev/null +++ b/research/controller-thinning-global-ceiling/adversarial.py @@ -0,0 +1,65 @@ +#!/usr/bin/env python3 +"""Reject actual source/profile corruptions. Apache-2.0; Codex assistance.""" +from hashlib import sha1, sha256 +import importlib.util +import json +from pathlib import Path +import shutil +from tempfile import TemporaryDirectory + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('thinning_mutation_target', HERE/'verify.py') +V = importlib.util.module_from_spec(spec) +spec.loader.exec_module(V) + + +def reject(name, mutate): + with TemporaryDirectory(prefix='thinning-control-') as directory: + target = Path(directory)/'package' + shutil.copytree(HERE, target) + original = V.HERE + V.HERE = target + try: + mutate(target) + try: + V.authenticate() + except ValueError: + return name + raise RuntimeError('Mutation accepted: '+name) + finally: + V.HERE = original + + +def bad_live_pin(target): + path = target/'SOURCES.json' + value = json.loads(path.read_text()) + next(x for x in value['files'] if x['usage'] == 'input')['sha256'] = '0'*64 + path.write_text(json.dumps(value)) + + +def bad_blob(target): + path = target/'FROZEN-SOURCE.json' + value = json.loads(path.read_text()) + value['git_blob'] = '0'*40 + path.write_text(json.dumps(value)) + + +def change_profile(target, rebind): + path = target/'inputs/PR4610-ARITHMETIC.json' + value = json.loads(path.read_bytes()) + value['local_paid']['8'] = 0 + raw = (json.dumps(value)+'\n').encode() + path.write_bytes(raw) + if rebind: + manifest_path = target/'FROZEN-SOURCE.json' + manifest = json.loads(manifest_path.read_text()) + manifest['sha256'] = sha256(raw).hexdigest() + manifest['git_blob'] = sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() + manifest_path.write_text(json.dumps(manifest)) + + +V.authenticate() +results = [reject('live source pin', bad_live_pin), reject('frozen Git blob', bad_blob), + reject('frozen source bytes', lambda p: change_profile(p, False)), + reject('owned jobs removed with rebound hashes', lambda p: change_profile(p, True))] +print(json.dumps({'status':'PASS_FOUR_ACTUAL_MUTATION_REJECTIONS', 'rejected':results})) From 8ccc47da053412ba28bc6ab04c368c4ebf21be30 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Thu, 22 Oct 2026 09:41:01 -0500 Subject: [PATCH 4/5] Bound the free-centre relaxation below 0.01 after global retuning --- .../PROOF.md | 21 +++ .../README.md | 6 + .../RESULT.json | 142 ++++++++++++++++++ .../VALIDATION.md | 41 +++++ .../verify.py | 23 +++ 5 files changed, 233 insertions(+) create mode 100644 research/controller-thinning-global-ceiling/VALIDATION.md diff --git a/research/controller-thinning-global-ceiling/PROOF.md b/research/controller-thinning-global-ceiling/PROOF.md index cad9588d7a..92b6fc3c7c 100644 --- a/research/controller-thinning-global-ceiling/PROOF.md +++ b/research/controller-thinning-global-ceiling/PROOF.md @@ -174,6 +174,27 @@ F <= -112 + k(112+1792t-2482) + 224S(t-1) < 0. This also covers k=S=0. Combining the two ranges and the dominance reduction excludes every `0.0030217759<=C<1` in the stated family. +## 5. Even free owned centres do not reach C=0.01 + +As an explicitly unrealized optimistic relaxation, remove all eight paid +rank-eight owned-centre jobs, keeping every other charge and target. The +same dominance proof applies. The local derivative L' becomes still smaller, +and the small-t lower bound becomes 2474, which still exceeds 560. + +Reoptimizing **all** pair counts, splits and thinning masks, rather than +keeping p16, puts the best relaxed crossing in +`(0.0080596238,0.0080596239)`, at p5 with both side lengths 2 and all three +separate flags full. The eight maximizing S values at the upper endpoint, +in the bit order used above, are `7,6,6,5,6,5,5,4`; all maxima are strictly +negative, and their adjacent differences have the required strict signs. +The p5 surplus is positive at the lower endpoint. Exact certificates are +in RESULT.json. The same monotonicity and small-t argument excludes every +larger C<1 in this relaxed family. + +Thus even deleting the entire owned-centre bill cannot reach C=0.01 by +retuning this path. A C>=0.01 attack needs another changed hypothesis. +This is a planning obstruction, not an implementation of free centres. + ## Implication and limits The existing p16 allocation already attains this family's best raw crossing diff --git a/research/controller-thinning-global-ceiling/README.md b/research/controller-thinning-global-ceiling/README.md index cc82123420..cebde8f0d0 100644 --- a/research/controller-thinning-global-ceiling/README.md +++ b/research/controller-thinning-global-ceiling/README.md @@ -15,6 +15,12 @@ their maxima over all pair counts. A separate derivative and small-exponent bound excludes every larger saving C<1. Changed words, idle topologies, query alphabets and local profiles remain open. +An optimistic corollary removes all eight owned-centre charges and reoptimizes +the whole family. Its best raw crossing is only +**(0.0080596238, 0.0080596239)**, at p5. Thus even free centres cannot reach +C=0.01 through this path. Free centres are a hypothetical relaxation; +this does not supply a construction at that larger value. + The source binding checks the literal path's rational projector identities and all 12,744 full/thin stage subsets, for every split through p5. This bounded operator check supports the invoice binding; the proof supplies the infinite diff --git a/research/controller-thinning-global-ceiling/RESULT.json b/research/controller-thinning-global-ceiling/RESULT.json index 7fd929c39c..fd2394b4f8 100644 --- a/research/controller-thinning-global-ceiling/RESULT.json +++ b/research/controller-thinning-global-ceiling/RESULT.json @@ -199,6 +199,148 @@ "source and profile pins" ], "exact_source_masks_checked": 12744, + "free_owned_centres": { + "canonical_maxima": [ + { + "flags": [ + 0, + 0, + 0 + ], + "side_windows": 7, + "sides": [ + 4, + 3 + ], + "surplus": { + "lower": "-19.160692467124252864938109681869", + "upper": "-19.160692467124252864938109681868" + } + }, + { + "flags": [ + 1, + 0, + 0 + ], + "side_windows": 6, + "sides": [ + 3, + 3 + ], + "surplus": { + "lower": "-13.556781328096692196152849765181", + "upper": "-13.556781328096692196152849765180" + } + }, + { + "flags": [ + 0, + 1, + 0 + ], + "side_windows": 6, + "sides": [ + 4, + 2 + ], + "surplus": { + "lower": "-13.556781328096692196152849765181", + "upper": "-13.556781328096692196152849765180" + } + }, + { + "flags": [ + 1, + 1, + 0 + ], + "side_windows": 5, + "sides": [ + 3, + 2 + ], + "surplus": { + "lower": "-7.952870189069131527367589848493", + "upper": "-7.952870189069131527367589848492" + } + }, + { + "flags": [ + 0, + 0, + 1 + ], + "side_windows": 6, + "sides": [ + 3, + 3 + ], + "surplus": { + "lower": "-11.207828944080986568999085355421", + "upper": "-11.207828944080986568999085355420" + } + }, + { + "flags": [ + 1, + 0, + 1 + ], + "side_windows": 5, + "sides": [ + 2, + 3 + ], + "surplus": { + "lower": "-5.603917805053425900213825438734", + "upper": "-5.603917805053425900213825438733" + } + }, + { + "flags": [ + 0, + 1, + 1 + ], + "side_windows": 5, + "sides": [ + 3, + 2 + ], + "surplus": { + "lower": "-5.603917805053425900213825438734", + "upper": "-5.603917805053425900213825438733" + } + }, + { + "flags": [ + 1, + 1, + 1 + ], + "side_windows": 4, + "sides": [ + 2, + 2 + ], + "surplus": { + "lower": "-0.000006666025865231428565522046", + "upper": "-0.000006666025865231428565522045" + } + } + ], + "conclusion": "Even free centres and arbitrary stage thinning cannot reach C=0.01", + "lower_endpoint_surplus": { + "lower": "0.000001549532231927529811361690", + "upper": "0.000001549532231927529811361691" + }, + "raw_root_bracket": [ + "40298119/5000000000", + "80596239/10000000000" + ], + "scope": "Unrealized optimistic relaxation; no higher K construction" + }, "local_derivative_upper": { "lower": "-9.534824922458622507134205148508", "upper": "-9.534824922458622507134205148507" diff --git a/research/controller-thinning-global-ceiling/VALIDATION.md b/research/controller-thinning-global-ceiling/VALIDATION.md new file mode 100644 index 0000000000..4eddb36918 --- /dev/null +++ b/research/controller-thinning-global-ceiling/VALIDATION.md @@ -0,0 +1,41 @@ +# Executed checks and evidence boundary + +Scientific baseline and publication refresh: canonical main +`b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, 2026-10-22. +The relevant guidance, selected result and three live source inputs did not +change at the refresh. PR4610 input head: +`1eb8da6cfb35512c0cc2533413e5ca42f48e13c6`. + +Completed on CPython 3.12.15, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/controller-thinning-global-ceiling +python3.12 -B scripts/check_research_commit.py --package research/controller-thinning-global-ceiling --check-source-history +git diff --check +``` + +The registered replay reconstructs both the actual-profile and free-centre +certificates. It checks every maximum and both adjacent differences, both +tight lower endpoints, the uniform derivative bound, both small-exponent +inequalities, all 12,744 source masks and every source projector for the +declared p<=5 cases. Its second command rejects four actual mutations: +live source hash, frozen Git blob, frozen bytes, and an owned-job deletion +whose source hashes were also rebound. + +The original arithmetic input and its committed snapshot have the identical +Git blob `c89e009ca4a5ad316c69f0371d885d72045ba415`. The package's local +attributes preserve its CRLF bytes. Earlier authoring runs caught and fixed +a JSON tuple/list comparison and Git line-ending normalization; the normal +registered replay passed after those fixes. `--write` is not substituted for +the registered check. + +The exact interval engine is the source-pinned rational Taylor/atanh engine +from higher-moment-strictification, credited to zxv. Floating discovery is +not used by acceptance. The written dominance and calculus proof has not +received independent human or proof-assistant review. The finite source +binding does not prove the retained endpoint contract for unexecuted p. + +The current selected cold replay, historical suites, Lean and manual hosted +workflows were not run: no selected construction or shared code changed. +Hosted CI status must be checked separately. No native, physical, compiler, +BIT or outer admission is established by these arithmetic checks. diff --git a/research/controller-thinning-global-ceiling/verify.py b/research/controller-thinning-global-ceiling/verify.py index 6c11e28135..cd682e1d2b 100644 --- a/research/controller-thinning-global-ceiling/verify.py +++ b/research/controller-thinning-global-ceiling/verify.py @@ -183,11 +183,34 @@ def certify(): need(high[0]+15*V > 0, 'Control: unpaid queries would falsely pass') swap = add(E.power(8, Q(1,2)), E.power(8, Q(1,2)), E.scale(E.power(16,Q(1,2)), -1)) need(swap[0] > 0, 'Strict even-to-odd swap control') + # Optimistic relaxation: delete all eight owned rank-eight charges. + # The local derivative becomes still smaller, so its proved sign persists. + free_paid = dict(P) + free_paid[8] -= 8 + need(sum(free_paid.values())-2*sum(H.values()) == 2474 > V+2*V*D*Q(1,4), + 'Small-exponent bound also covers free owned centres') + free_lower, free_upper = Q('0.0080596238'), Q('0.0080596239') + free_maxima = [] + for encoded, count in enumerate([7, 6, 6, 5, 6, 5, 5, 4]): + flags = tuple((encoded >> j) & 1 for j in range(3)) + current, sides = canonical(E, H, free_paid, count, flags, free_upper) + previous, _ = canonical(E, H, free_paid, count-1, flags, free_upper) + following, _ = canonical(E, H, free_paid, count+1, flags, free_upper) + need(current[0] > previous[1] and current[0] > following[1] and current[1] < 0, + 'Global maximum with free centres, not fixed-p lever pricing') + free_maxima.append({'flags':flags, 'side_windows':count, 'sides':sides, + 'surplus':E.display(current)}) + free_low, _ = canonical(E, H, free_paid, 4, (1,1,1), free_lower) + need(free_low[0] > 0, 'Tight free-centre lower endpoint at p5') return {'status':'PASS_GLOBAL_PAIRED_PATH_THINNING_CEILING', 'source_pr':4610, 'scope':'All pair counts, prefix/suffix splits, and binary full-stage subsets of the retained path', 'raw_root_bracket':[str(LOWER), str(UPPER)], 'new_kappa':False, 'local_derivative_upper':E.display(derivative), 'canonical_maxima':maxima, 'lower_endpoint_surplus':E.display(low), 'exact_source_masks_checked':finite_source_binding(), + 'free_owned_centres':{'scope':'Unrealized optimistic relaxation; no higher K construction', + 'raw_root_bracket':[str(free_lower), str(free_upper)], + 'canonical_maxima':free_maxima, 'lower_endpoint_surplus':E.display(free_low), + 'conclusion':'Even free centres and arbitrary stage thinning cannot reach C=0.01'}, 'controls':['charged queries', 'strict even-to-odd swap', 'source and profile pins'], 'proof':'PROOF.md supplies infinite-family dominance and concavity'} From 342f584157cf1a868c4c25d4870e7476d10480df Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Thu, 22 Oct 2026 09:44:53 -0500 Subject: [PATCH 5/5] Credit concurrent path ceiling and identify the typed-interface escape --- .../controller-thinning-global-ceiling/README.md | 13 +++++++++++++ .../VALIDATION.md | 4 ++++ 2 files changed, 17 insertions(+) diff --git a/research/controller-thinning-global-ceiling/README.md b/research/controller-thinning-global-ceiling/README.md index cebde8f0d0..6bbcf6bfff 100644 --- a/research/controller-thinning-global-ceiling/README.md +++ b/research/controller-thinning-global-ceiling/README.md @@ -48,6 +48,19 @@ unconditional multiplication theorem or independent human acceptance. ## Open next questions +Publication refresh found concurrent [PR4658](https://github.com/CrocSwap/integer-mult-bounds/pull/4658): +it certifies C<0.003022 for three pinned profiles through p64 using a max-plus +DP. This contribution instead proves the reduction for unbounded p, sharpens +the round-three bracket and adds the globally retuned free-centre corollary. +PR4658 was inspected at the description level; no independent replay is claimed. + +The concurrent [typed quotient interface, PR4654](https://github.com/CrocSwap/integer-mult-bounds/pull/4654), +is outside this theorem. [PR4660](https://github.com/CrocSwap/integer-mult-bounds/pull/4660) +reports that extracting its B pairs and keeping an A-only path fails for all p +and C. Its remaining constructive target is a controller that keeps both types +active, or a changed centre/phase schedule. These are provisional source claims, +not newly replayed native constructions in this package. + Find a profitable change outside the retained path: a different scalar word, idle topology, nonbinary replacement or native query interface. First emit its complete endpoint contract and paid/target moment. An optimistic moment gain diff --git a/research/controller-thinning-global-ceiling/VALIDATION.md b/research/controller-thinning-global-ceiling/VALIDATION.md index 4eddb36918..249f171446 100644 --- a/research/controller-thinning-global-ceiling/VALIDATION.md +++ b/research/controller-thinning-global-ceiling/VALIDATION.md @@ -39,3 +39,7 @@ The current selected cold replay, historical suites, Lean and manual hosted workflows were not run: no selected construction or shared code changed. Hosted CI status must be checked separately. No native, physical, compiler, BIT or outer admission is established by these arithmetic checks. + +The final live PR refresh included concurrent #4658, #4654 and #4660. +Their descriptions were inspected and the overlap/escape scope recorded in +README.md. Their full sources and proofs were not independently replayed.