diff --git a/research/controller-stage-ceiling/PROOF.md b/research/controller-stage-ceiling/PROOF.md new file mode 100644 index 0000000000..23a4ba90aa --- /dev/null +++ b/research/controller-stage-ceiling/PROOF.md @@ -0,0 +1,126 @@ +# Complete stage-family ceiling and a native repair target + +Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. + +## Family and scope + +Fix one of the three source-bound local invoices: selected PR4470, PR4610, +or PR4626. There are v=112 ports and transverse rank b=8. For each +1 <= p <= 64, take any split a in {0,...,p-1} of the minimal-cut paired +path controller, and **any** subset S of its 2p+1 native stage positions. +Stages outside S become fully paid query shears, lose all helper credit, +and lose their stage multiplier in both main targets and idle jobs. +This is the specialization operation of PR4440, not deletion of a bill. + +The family is deliberately an invoice relaxation: all these substitutions +are priced even if a particular new physical contact has not been admitted. +Rejecting this stronger relaxation is safe; positive scores alone would not +admit a word. No other idle masks, words, native suppliers, typed outputs, +or p>64 are excluded. The selected record is unchanged. + +## Complete surplus + +Let n=|S|, t=1-C, and let H_t and P_t be the local helper and paid moments. +Write V=112 and B=8. The complete surplus is + + F(C) = n(H_t-P_t+V) - V(2p+1) + 2V(1+Bn)^t + + sum_arm 2V[(1+B(k+e))^t - (Bk)^t - e B^t]. + +There are a left arm of length a and a right arm of length p-1-a. At +an arm step j, k is the number of selected bits in the first 2j positions +of that arm and e is the next, even-position bit. The right arm is read +in reverse stage order. Rank-zero idle terms mean zero cost, including +in the limit t -> 0. The central odd-position bit contributes only to n. + +The first term includes all n independent helper inventories and all n +native paid inventories. The V correction replaces the otherwise paid +query at each native stage. The second term charges every query position. +The third term is the two copies of the long main target. Each arm term +includes its shorter main target, initial/terminal idle, and the separate +middle idle of rank B when e=1. Thus no middle idle is silently erased +when its stage remains native. `literal_control` independently counts every +LOCAL, QUERY_SHEAR, IDLE and diagonal target of the retained p16 word. + +## Dynamic program, with outward rounding + +An arm's score depends on a prefix only through its selected-bit count. +For a nonempty arm its first two bits have no separate charge and therefore +only their count 0,1,2 matters. An empty arm has one bit. At each subsequent +step choose e, add its displayed complete arm contribution, then choose the +following odd bit unless this is the last step. Keep the largest score +for each count. This is exhaustive induction on the bit prefix, not a +local hill climb. It is the recurrence of the credited historical floating +DP, now evaluated with exact, outward integer bounds. + +The retained rational interval engine encloses each r^t. Scale by 2^64, +round positive occurrences up and negative occurrences down. Every DP +score is consequently an upper bound on its real surplus. Maxima preserve +upper bounds. Combine both arms, every split and the middle bit, then +maximize over every p=1,...,64. The three native profiles share that +combinatorial envelope. Their local replacement terms are added separately. + +At C=0.003022, every final upper bound is strictly negative. `RESULT.json` +records the exact rational upper bounds, integer scale and witness parameters. +The covered count is sum(p*2^(2p+1), p=1,...,64) per native invoice. It +counts split/support pairs; it is not a claim that all invoices are distinct. + +Acceptance also exhausts every arm bit pattern through length four and +all complete stage supports/splits through p=3; checks the actual p16 +invoice for each local substitution; and recomputes a witness moment with +the independent full-invoice path of the rational engine. Omitting the +real middle-idle charge or duplicating independent helper credit changes +the rejection into an apparent positive result. These are rejected models. + +## Why one test excludes every larger saving in this family + +For each fixed support, divide the surplus by 8^t. Its normalized local +replacement is + + L(C) = (H_t - P_t + V)/8^t. + +All paid ranks are at most 8. For t in (0,1], its derivative with respect +to C has upper bound + + L'(C) <= -((P_1-V)/8)*log(8) + + sum_(r<8) H_r log(8/r) < 0. + +Indeed, retain only the negative rank-one paid contribution; its magnitude +is at least (P_1-V)log(8)/8. Bound each possible positive helper contribution +by H_r log(8/r), and drop the other negative contributions. The final strict +inequality is enclosed rationally for each frozen invoice. + +For an arm step with k>=1, the derivative of + + (k+e+1/8)^t - k^t - e + +is negative, since x^t log(x) is increasing for x>=1. If k=0,e=1, +its derivative is again negative. The only positive case k=e=0 contributes +at most (1/8)^t log(8) before the multiplicity 2V. There are at most p-1 +such arm steps. The normalized negative query term contributes +-V(2p+1)(1/8)^t log(8), more than cancelling all of them. If n>=1, +the normalized long main target has negative derivative. If n=0, its +positive derivative leaves the total derivative exactly +-V(1/8)^t log(8). Thus F(C)/8^(1-C) is strictly decreasing throughout +0<=C<1 for every support in the family. + +The negative bound at .003022 therefore excludes **all C>=.003022, +C<1**, not merely that one numerical point. This is a conditional invoice +ceiling, not a universal limit on integer multiplication. + +## Changed model: the H repair budget + +The old H112 reconstruction changes a local rank-eight correction bill +8 H8 to 8 H1, saving 56 units of rank per full call. Applying that +56-unit change to PR4610's stronger native invoice is an **optimistic +unrealized combination**. It is not a source-compatible H word: changed +warp contacts, cross-port response, head/hole normalizers, absolute phases +and arbitrary-input helper restoration all still need proof. + +For that explicitly hypothetical invoice, the same complete DP gives +exact upper repair budgets at .004, .006 and .01. A full-invoice lower +bound at each saved witness confirms the scale of the positive budgets. +A rank-one repair request costs exactly one unit at every C; a rank-r +request costs r^(1-C). Storage, scalar work and all other requests also +need their actual ledger. These numbers are spending limits, not free +allowances or proposed K values. In particular the .01 screen fails even +before a repair in this bounded family. No conclusion for p>64 follows. diff --git a/research/controller-stage-ceiling/README.md b/research/controller-stage-ceiling/README.md new file mode 100644 index 0000000000..cedeb5c908 --- /dev/null +++ b/research/controller-stage-ceiling/README.md @@ -0,0 +1,63 @@ +# Exact ceiling for native/thin path-controller changes + +**No higher K or new supplier is claimed.** For the source-pinned PR4470, +PR4610 and PR4626 invoices, every minimal-cut path controller with 1..64 +pairs, every split, and every native/thin stage subset fails at +C=0.003022. A normalized-moment monotonicity proof excludes all larger +C<1 in this family. This turns the earlier floating stage search into an +exact certificate and identifies a model change required for a substantial +increase. The selected conditional K remains 0.00302015 at the base commit. + +[PROOF.md](PROOF.md) derives the complete invoice, the exhaustive max-plus +recurrence, outward integer bounds and the monotone rank-eight separator. +[RESULT.json](RESULT.json) contains the exact receipt. This does not exclude +new words, native interfaces, idle masks, coded corrections, or p>64. + +The changed-model calculation also prices an optimistic combination of +PR4610 with H112's 56-rank-unit local saving. Its repair budgets at .004, +.006 and .01 are included, with the unproved native/caller compatibility +explicitly retained. A budget or positive invoice is not an implementation. + +| Candidate C | Maximum optimistic rank-one repair budget | +| --- | ---: | +| .004 | 2641.1932795534 (p=64) | +| .006 | 342.1085144324 (p=37) | +| .01 | Already negative: -93.1789150428 | + +These are bounded-family upper limits; source compatibility is unproved. + +Reproduce from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/controller-stage-ceiling +``` + +The verifier uses the standard library and the pinned rational interval +engine. It does not require a solver. Controls compare small complete +censuses and literal p16 event bills, and show why dropping middle idles +or duplicating independent helper credit would give false apparent gains. +The external PR inputs are exact unmodified Git blobs, not newly admitted +native words; their provenance and heads are in SOURCES.json. + +## Open next questions + +1. Construct a physical H caller with a complete correction invoice below + the recorded repair budget. Start with one actual head/hole boundary and + check all columns, source/complement ownership and absolute phases. The + old local H invoice and its scalar involution do not close that caller. +2. Change the native word, interface or controller topology. A further + native/thin subset scan inside the certified family cannot reach .004. + A new candidate must provide an exact endpoint and a complete paid bill. + +## Attribution and status + +Prepared by Cinna Davis with substantial OpenAI Codex assistance, Apache-2.0. +The branch recurrence is credited to the pre-existing +`research/kappa-hybrid-controller/search/direct_stage_dp.py` authors and +Cinna Davis's PR4440/PR4470 controller lineage. Cao Yifan's PR4610 supplies +the changed warp invoice; hexapode's PR4626 supplies the helper621 invoice. +Retain zxv's exact interval/native/strictification contributions and Jacob +Alan Sussman's mixed-job/compiler work. The new contribution is the exact +integer bound, the monotonicity proof and the current source-bound repair +budget. It does not assert independent human review, a formal proof-kernel +check, or a new multiplication theorem. diff --git a/research/controller-stage-ceiling/RESULT.json b/research/controller-stage-ceiling/RESULT.json new file mode 100644 index 0000000000..853657405f --- /dev/null +++ b/research/controller-stage-ceiling/RESULT.json @@ -0,0 +1,82 @@ +{ + "all_native_stage_subsets": true, + "all_splits": true, + "ceiling": "1511/500000", + "controls": [ + "all_5_small_arm_censuses", + "all_complete_patterns_p1_to_p3", + "all_3_literal_p16_invoices", + "missing_middle_idle_changes_sign", + "duplicate_helper_credit_changes_sign" + ], + "fixed_point_scale": "18446744073709551616", + "new_kappa": null, + "optimistic_H_repair_budgets": { + "1/100": { + "best_surplus_upper": "-53713987464422013341/576460752303423488", + "status": "OPTIMISTIC_INVOICE_ONLY_NO_H_NATIVE_ADMISSION", + "witness_parameters": [ + 1, + 0, + 6 + ], + "witness_surplus_lower": "-292446764658482249839017434957133446527108325308117437477329/3138550867693340381917894711603833208051177722232017256448" + }, + "1/250": { + "best_surplus_upper": "24360708238561784637317/9223372036854775808", + "status": "OPTIMISTIC_INVOICE_ONLY_NO_H_NATIVE_ADMISSION", + "witness_parameters": [ + 64, + 31, + 680564733840226340207702041255296892927 + ], + "witness_surplus_lower": "2072379864822052426775990683944584074709758170880344027228125/784637716923335095479473677900958302012794430558004314112" + }, + "3/500": { + "best_surplus_upper": "3155394105585959091153/9223372036854775808", + "status": "OPTIMISTIC_INVOICE_ONLY_NO_H_NATIVE_ADMISSION", + "witness_parameters": [ + 37, + 18, + 31482443219130968091307 + ], + "witness_surplus_lower": "2147449949634335534650179046572602361862313365888596319687777/6277101735386680763835789423207666416102355444464034512896" + } + }, + "pair_counts": [ + 1, + 64 + ], + "patterns_per_profile": "57772384072799330241337377795082425233864", + "profiles": { + "PR4470": { + "separator_derivative_lower": "834868369783004008952768229585313202122157833070803325402459/1569275433846670190958947355801916604025588861116008628224", + "surplus_upper": "-4184234018831163103/9223372036854775808", + "witness_parameters": [ + 16, + 7, + 7158278827 + ] + }, + "PR4610": { + "separator_derivative_lower": "410091947704675574684453227077902260907026584522260683631425/784637716923335095479473677900958302012794430558004314112", + "surplus_upper": "-1014518977939581775/9223372036854775808", + "witness_parameters": [ + 16, + 7, + 7158278827 + ] + }, + "PR4626": { + "separator_derivative_lower": "1640764499882385906456930065487073635005120770603694469307877/3138550867693340381917894711603833208051177722232017256448", + "surplus_upper": "-977466852836146591/9223372036854775808", + "witness_parameters": [ + 16, + 7, + 7158278827 + ] + } + }, + "scope": "Frozen native invoices and minimal-cut path family, p<=64. No global operator/controller ceiling or new supplier.", + "status": "PASS_EXACT_STAGE_FAMILY_CEILING" +} diff --git a/research/controller-stage-ceiling/SOURCES.json b/research/controller-stage-ceiling/SOURCES.json new file mode 100644 index 0000000000..f9d535c7a8 --- /dev/null +++ b/research/controller-stage-ceiling/SOURCES.json @@ -0,0 +1,70 @@ +{ + "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/joint-helper-lattice/NATIVE.json.gz", + "usage": "input", + "git_blob": "0910f74138decf498e7fc445cc2daff4390169d6", + "sha256": "74582cce642c80f0235be7fcbce3716174666326ac6a1d46d02a62a75d7be4c6" + }, + { + "path": "research/kappa-hybrid-controller/search/direct_stage_dp.py", + "usage": "input", + "git_blob": "0717a3a577fd7a4e3eea9901bb266955bdb908de", + "sha256": "4a457525a8c041d3e0fd2671634627d831e3c0dc2970219b11b3b2692ba32125" + }, + { + "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" + }, + { + "path": "research/controller-stage-ceiling/inputs/pr4610-native.json", + "usage": "input", + "git_blob": "88fa05cb3d0b7227f85ba0c42eb427184949447d", + "sha256": "c6f16840b3f7bed8686ad494b479df599b18b420c239dc6167c214130b78eb64", + "pin": "head:6ba2f0ad1809172be7ebf04ad750592f14475dab:research/controller-stage-ceiling/inputs/pr4610-native.json", + "original_source_pin": "head:1eb8da6cfb35512c0cc2533413e5ca42f48e13c6:research/warp-interface-20261022/NATIVE-VALIDATION.json" + }, + { + "path": "research/controller-stage-ceiling/inputs/pr4626-arithmetic.json", + "usage": "input", + "git_blob": "bec84f7dc990a0a892fd77fd74665d49df66d4de", + "sha256": "5787bae88594f8d05e1a7bbecdc98c8635523c817093b717af621ac893277d28", + "pin": "head:6ba2f0ad1809172be7ebf04ad750592f14475dab:research/controller-stage-ceiling/inputs/pr4626-arithmetic.json", + "original_source_pin": "head:e4413c43eeaacdd20be123fdd7d7add53427f028:research/helper621-warp-combination/ARITHMETIC.json" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + } + ] +} diff --git a/research/controller-stage-ceiling/TASK.json b/research/controller-stage-ceiling/TASK.json new file mode 100644 index 0000000000..836809f2d5 --- /dev/null +++ b/research/controller-stage-ceiling/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "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 #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "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.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "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", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact all-subset controller invoice ceiling and changed-model H repair budget.", + "scope_change_reason": "The user explicitly requested a substantially higher K and a bottleneck change, rather than the historical QQ16 card. Live frontier, withdrawn quotient, existing H and stage-DP work were inspected first.", + "bottleneck_link": "Certify that stage repacking cannot produce the requested large gain inside the frozen family; price the correction a changed H mechanism must afford.", + "budget_minutes": 60, + "stop_rule": "Stop the fixed-stage search when its exact upper bound is negative; require a changed operator contract before another construction round.", + "outcome": "negative-result", + "evidence": "PROOF.md; RESULT.json; registered verification", + "author": "Cinna Davis, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for research, proof, implementation and verification.", + "open_questions": [ + { + "question": "Can a physical H caller fit the recorded correction budget?", + "why_it_matters": "This changes the native rank surplus rather than the stage subset.", + "first_step": "Implement one actual head/hole boundary and price every request.", + "blocked_by": "No source-compatible H adaptation of the changed warp native word." + }, + { + "question": "Can a different controller word beat the certified path family?", + "why_it_matters": "All native/thin subsets in the bounded family are excluded above .003022.", + "first_step": "Emit and exactly replay a word with a changed topology or output contract.", + "blocked_by": "A complete new word and paid profile are not yet supplied." + } + ] +} diff --git a/research/controller-stage-ceiling/VALIDATION.md b/research/controller-stage-ceiling/VALIDATION.md new file mode 100644 index 0000000000..5c7c5e23a1 --- /dev/null +++ b/research/controller-stage-ceiling/VALIDATION.md @@ -0,0 +1,16 @@ +# Validation + +The direct CPython 3.14 replay and registered CPython 3.12.15 replay passed. +Both regenerated the same exact receipt. Metadata/live pins and the committed +byte/source-history preflight passed at publication. The package uses no solver. + +The exact acceptance checks cover three frozen local invoices, every pair +count 1..64, all splits and all native/thin supports through the integer DP; +all five small-arm censuses; all complete split/support choices through p=3; +three literal p16 substitutions; and two deliberately invalid model controls. +The normalized derivative bounds are rational. The all-C exclusion follows +from the written separator proof, not a floating grid or numerical root. + +PR4654's subsequent typed supplier is outside this family. No full native +re-admission, new supplier, higher K, selected cold replay or formal kernel +acceptance is claimed. PR4658's hosted checks are distinct from this local run. diff --git a/research/controller-stage-ceiling/VERIFY.json b/research/controller-stage-ceiling/VERIFY.json new file mode 100644 index 0000000000..2c08ff63eb --- /dev/null +++ b/research/controller-stage-ceiling/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/higher-moment-strictification/verify.py", + "research/joint-helper-lattice/NATIVE.json.gz", + "research/kappa-hybrid-controller/search/direct_stage_dp.py", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/query-thinned-controllers/controller.py", + "research/controller-stage-ceiling/inputs/pr4610-native.json", + "research/controller-stage-ceiling/inputs/pr4626-arithmetic.json", + "research/joint-helper-lattice/CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Integer interval dynamic program, complete invoice controls, all-pattern small brute force and monotone separator" + } + ] +} diff --git a/research/controller-stage-ceiling/inputs/pr4610-native.json b/research/controller-stage-ceiling/inputs/pr4610-native.json new file mode 100644 index 0000000000..88fa05cb3d --- /dev/null +++ b/research/controller-stage-ceiling/inputs/pr4610-native.json @@ -0,0 +1,144 @@ +{ + "controls": [ + { + "name": "wrong_warp_source_frame", + "rejected": "Warp input frame" + }, + { + "name": "old_paid_profile_at_new_word", + "rejected": "Complete paid profile" + } + ], + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "native": { + "backward": { + "arbitrary_owned_C0_cleared": true, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "l1_witness": { + "event": 6396, + "role": [ + "L", + 225 + ] + }, + "max_denominator": 64, + "max_formal_prefix_l1": "169", + "paid_profile": { + "1": 2201, + "2": 412, + "3": 506, + "4": 135, + "5": 36, + "8": 8 + }, + "paid_rank_mass": 5327, + "real_scalar_allowance": 158168, + "scalar_frames_checked": true, + "second_literal": { + "all_scalar_frames_checked": true, + "clean_J": false, + "conservative_real_scalar_primitive_allowance": 158168, + "direction": "backward", + "dyadic_coefficients_and_unit_scales_checked": true, + "event_counts": { + "adapter": 448, + "center": 8, + "climb": 3290, + "phase": 10, + "scalar": 17453, + "warp": 240 + }, + "expected_restored_arbitrary_cleanup_buffers": 0, + "expected_restored_helpers": 408, + "explicitly_owned_C_fields_cleared": 1, + "free_warp_operator_endpoint_matches": true, + "independent_borrowed_input_fields": 632, + "mismatch_examples": [], + "negative_control_omitted_last_cleanup_scalar": false, + "original_data_fields": 224, + "paid_profile": { + "1": 2201, + "2": 412, + "3": 506, + "4": 135, + "5": 36, + "8": 8 + }, + "paid_rank_mass": 5327 + } + }, + "forward": { + "arbitrary_owned_C0_cleared": true, + "independent_owned_entry_columns": 1, + "independent_persistent_columns": 632, + "l1_witness": { + "event": 19036, + "role": [ + "L", + 224 + ] + }, + "max_denominator": 32, + "max_formal_prefix_l1": "457", + "paid_profile": { + "1": 2201, + "2": 412, + "3": 506, + "4": 135, + "5": 36, + "8": 8 + }, + "paid_rank_mass": 5327, + "real_scalar_allowance": 158120, + "scalar_frames_checked": true, + "second_literal": { + "all_scalar_frames_checked": true, + "clean_J": false, + "conservative_real_scalar_primitive_allowance": 158120, + "direction": "forward", + "dyadic_coefficients_and_unit_scales_checked": true, + "event_counts": { + "adapter": 448, + "center": 8, + "climb": 3290, + "phase": 10, + "scalar": 17453, + "warp": 240 + }, + "expected_restored_arbitrary_cleanup_buffers": 0, + "expected_restored_helpers": 408, + "explicitly_owned_C_fields_cleared": 1, + "free_warp_operator_endpoint_matches": true, + "independent_borrowed_input_fields": 632, + "mismatch_examples": [], + "negative_control_omitted_last_cleanup_scalar": false, + "original_data_fields": 224, + "paid_profile": { + "1": 2201, + "2": 412, + "3": 506, + "4": 135, + "5": 36, + "8": 8 + }, + "paid_rank_mass": 5327 + } + } + }, + "paid": { + "1": 2201, + "2": 412, + "3": 506, + "4": 135, + "5": 36, + "8": 8 + }, + "seconds": 4.289734500023769, + "status": "PASS_CHANGED_G_NATIVE_BOTH_632_COLUMN_INTERPRETERS" +} diff --git a/research/controller-stage-ceiling/inputs/pr4626-arithmetic.json b/research/controller-stage-ceiling/inputs/pr4626-arithmetic.json new file mode 100644 index 0000000000..bec84f7dc9 --- /dev/null +++ b/research/controller-stage-ceiling/inputs/pr4626-arithmetic.json @@ -0,0 +1,244 @@ +{ + "compiler": { + "H": 337848000000000, + "N": "2^337848000000000", + "eta": { + "lower": "0.000000204749879400317649609837", + "upper": "0.000000204749879400317649609838" + }, + "gap": "1/7000000000", + "integer_test_exponent": 48264, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "21150989/7000000000", + "word_materialized": false + }, + "gain_over_PR4535": "351/250000000", + "gain_over_PR4610": "49/1000000000", + "kappa": "3021569/1000000000", + "local_helpers": { + "4": 28, + "7": 8, + "8": 47, + "9": 325 + }, + "local_paid": { + "1": 2202, + "2": 414, + "3": 505, + "4": 134, + "5": 36, + "8": 8 + }, + "margin_at_old_root_upper": [ + "545270589884341605855340249577885626836418302199787051413/1569275433846670190958947355801916604025588861116008628224", + "1090541179768683211710680499155771253672836604399686847725/3138550867693340381917894711603833208051177722232017256448" + ], + "native_data_sha256": "352d01646e8016ab7eb20cc3985db176f7dfa155b8b1f34cba89170790cddee5", + "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": 4803000, + "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": "1742999999253/1750000000000", + "fixed_halo_explicit_metadata_branch": "134750000001/1750000000", + "new_BIT_row_stock_sublinear_in_active_group": "6978999997009/7000000000000", + "new_semantic_group_guard": "3/7000000000" + }, + "margins": { + "boundary_algebraic_matrix": "74028454489424507/24500000000000000000", + "fused_gaussian": "74028454468273521/24500000000000000000", + "global_coordinate_router": "21150987/7000000000", + "group_bit_router": "148056915936547039/49000000000000000000", + "group_scans": "3499999999/3500000000", + "main_transform": "74028450989424507/24500000000000000000", + "microbox_face_corrections": "134750000001/1750000000", + "polynomial_products": "6999999999/7000000000", + "sparse_union_movement": "10027153454489424507/24500000000000000000" + }, + "parameters": { + "a": "21150987/7000000000", + "b": "5287747/1750000000", + "beta": "6999999997/7000000000", + "bit_saving": "17/5000", + "cap_xi": "22277153450989424507/24500000000000000000", + "complex_uniform_saving": "21150989/7000000000", + "d": "1/7000000000", + "epsilon": "6999999999/7000000000", + "kappa": "3021569/1000000000", + "lambda_": "1993956861/2000000000", + "lambda_prime": "3489424507/3500000000", + "layout": "1/7000000000", + "q": "10575493/3500000000", + "r0": "1/70000000000", + "stop": "1/7000000000", + "tested_saving": "302157/100000000" + }, + "strict_checks": { + "actual_bit_above_effective": "2649013/7000000000", + "actual_logarithmic_gamma_guard": "1/7000000000", + "actual_logarithmic_group_guard": "2222846554260575493/12250000000000000000", + "alpha_logarithm_absorption": "1/70000000000", + "boundary_algebraic_matrix_above_kappa": "13989424507/24500000000000000000", + "cap_above_band": "10027153450989424507/24500000000000000000", + "cap_below_cell": "2222846545510575493/24500000000000000000", + "cap_below_phase_cell_power": "26722846549010575493/24500000000000000000", + "complex_above_effective": "1/7000000000", + "complex_below_one_over_32": "49399753/1750000000", + "complex_endpoint": "1/3500000000", + "epsilon_below_one": "1/7000000000", + "epsilon_positive": "6999999999/7000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "13968273521/24500000000000000000", + "gaussian_above_main": "1739424507/12250000000000000000", + "global_coordinate_router_above_kappa": "1/1750000000", + "global_gamma_power_slack": "9/70000000000", + "group_below_dimension": "1/3500000000", + "group_bit_router_above_kappa": "34936547039/49000000000000000000", + "group_gauge_power_slack": "2222846554085575493/12250000000000000000", + "group_key_fits_record": "1/3500000000", + "group_positive": "6999999997/7000000000", + "group_scans_above_kappa": "1395769803/1400000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "645299290400418148631/500000000000000000000000", + "lambda_above_internal": "1/14000000000", + "lambda_above_sigma": "3/14000000000", + "lambda_above_tau": "1/14000000000", + "lambda_prime_above_lambda": "1/14000000000", + "lambda_prime_above_leaf": "3494712253/12250000000000000000", + "leaf_saving_above_effective": "1744712253/12250000000000000000", + "main_transform_above_kappa": "10489424507/24500000000000000000", + "membership_arithmetic_fits_record": "1/7000000000", + "microbox_face_corrections_above_kappa": "538978849021/7000000000", + "microbox_halo_volume": "553000000003/7000000000", + "new_complex_uniform_saving_above_b": "1/7000000000", + "new_semantic_guard_with_C1_one": "1/7000000000", + "polynomial_products_above_kappa": "872356127/875000000", + "positive_layout_slack": "1/7000000000", + "q_below_effective": "1/7000000000", + "q_below_internal": "1/7000000000", + "q_below_leaf": "3494712253/12250000000000000000", + "q_positive": "10575493/3500000000", + "short_record_fallback": "1744712253/1750000000", + "source_axis_superpolynomial": "1/7000000000", + "sparse_union_movement_above_kappa": "9953125013989424507/24500000000000000000", + "stop_below_one": "6999999999/7000000000", + "stop_positive": "1/7000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/7000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/7000000000", + "union_tag_work_per_visit_fits_record": "3/7000000000" + } + }, + "paid": { + "1": 41316, + "16": 448, + "2": 7452, + "24": 448, + "3": 9090, + "32": 448, + "4": 2412, + "40": 448, + "48": 448, + "5": 648, + "56": 448, + "64": 448, + "72": 224, + "8": 144 + }, + "paid_calls": 64422, + "productive_fields": 10928, + "rank_mass_surplus": 752, + "raw_root_interval": [ + "30215713/10000000000", + "15107857/5000000000" + ], + "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/helper621-warp-combination/arithmetic.py": "1a87db26b2d3fdf7de10424309523541fd53248e648b0d06b1836c38e8caec8c", + "research/helper621-warp-combination/vendor/price_profile_4610.py": "bbbafd38b8fee15f4a19f5b726aaf67b8c4e897ecb01ea89a5722168eb27e151", + "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-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/kappa-rebuild/complex/full-identity-certificates/RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6", + "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.999999998585401279767941804505", + "upper": "0.999999998585401279767941804506" + }, + "cutoff": 20, + "delta": { + "lower": "0.958429239685014938905792889089", + "upper": "0.958429239685014938905792889090" + }, + "floor": 21, + "gamma": { + "lower": "0.956206638044871931847709338655", + "upper": "0.956206638044871931847709338656" + }, + "normalized_paid_upper": "2097152001953127/2097154147483648", + "power": 1024, + "tail_offset": "1/5", + "tested": "302157/100000000" + }, + "targets": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 144, + "73": 224, + "8": 846, + "9": 5850 + } +} diff --git a/research/controller-stage-ceiling/verify.py b/research/controller-stage-ceiling/verify.py new file mode 100644 index 0000000000..1cd93e936b --- /dev/null +++ b/research/controller-stage-ceiling/verify.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +"""Exact stage-family bound. Apache-2.0; substantial OpenAI Codex assistance. + +Credits the floating DP in kappa-hybrid-controller/search/direct_stage_dp.py. +All acceptance scores here are outward integer bounds, never floating output. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import argparse,gzip,importlib.util,json,sys +sys.dont_write_bytecode=True +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +SCALE=2**64 +MAX_P=64 + +def need(v,s): + if not v:raise ValueError(s) +def read(path): + raw=path.read_bytes();return json.loads(gzip.decompress(raw) if path.suffix=='.gz' else raw) +def authenticate(): + for row in read(HERE/'SOURCES.json')['files']: + if row['usage']=='input':need(sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'Changed input: '+row['path']) +def engine(): + spec=importlib.util.spec_from_file_location('stage_intervals',ROOT/'research/higher-moment-strictification/verify.py') + m=importlib.util.module_from_spec(spec);sys.modules[spec.name]=m;spec.loader.exec_module(m);return m +def profiles(): + a=read(ROOT/'research/joint-helper-lattice/NATIVE.json.gz');b=read(HERE/'inputs/pr4610-native.json');c=read(HERE/'inputs/pr4626-arithmetic.json') + ints=lambda d:{int(k):v for k,v in d.items()} + return {'PR4470':(ints(a['helpers']),ints(a['paid'])),'PR4610':(ints(b['helpers']),ints(b['paid'])),'PR4626':(ints(c['local_helpers']),ints(c['local_paid']))} +def weights(E,c): + ranks={*range(1,10),*(8*k for k in range(1,2*MAX_P+2)),*(1+8*k for k in range(2*MAX_P+2))} + low,high={0:0},{0:0} + for r in sorted(ranks): + a,b=E.power(r,1-c);low[r]=(a*SCALE).__floor__();high[r]=-((-b*SCALE).__floor__()) + need(Q(low[r],SCALE)<=a<=b<=Q(high[r],SCALE),'Outward integer powers') + return low,high + +def branches(length,low,high,omit_middle=False): + states={k:(0,(1<new[nn][0]:new[nn]=val,mm + states=new + return states + +def envelope(low,high,max_p=MAX_P,omit_middle=False): + arms=[branches(n,low,high,omit_middle) for n in range(max_p)];best={} + for p in range(1,max_p+1): + for cut in range(p): + right=p-1-cut + for nl,(sl,ml) in arms[cut].items(): + for nr,(sr,mr) in arms[right].items(): + for middle in (0,1): + n=nl+nr+middle + val=sl+sr-112*(2*p+1)*low[1]+224*high[1+8*n] + if n not in best or val>best[n][0]: + reflected=sum(1<<(2*p-j) for j in range(2*right+1) if mr>>j&1) + best[n]=val,(p,cut,ml|reflected|(middle<<(2*cut+1))) + return best + +def maximum(env,lo,hi,h,paid): + delta=112*hi[1]+sum(v*hi[r] for r,v in h.items())-sum(v*lo[r] for r,v in paid.items()) + return max((score+n*delta,args) for n,(score,args) in env.items()) + +def invoice(p,cut,mask,h,local,omit_middle=False): + n=mask.bit_count();T=Counter({r:n*v for r,v in h.items()});P=Counter({r:n*v for r,v in local.items()}) + P[1]+=112*(2*p+1-n);T[1+8*n]+=224 + for length,reverse in ((cut,False),(p-1-cut,True)): + for j in range(1,length+1): + pos=list(range(2*j+1)) + if reverse:pos=[2*p-s for s in pos] + count=sum(mask>>s&1 for s in pos);idle=sum(mask>>s&1 for s in pos[:-1]) + T[1+8*count]+=224 + if idle:P[8*idle]+=224 + if not omit_middle:P[8]+=224*sum(mask>>(2*j)&1 for j in range(1,p)) + return +T,+P + +def brute_arm(length,lo,hi): + result={} + for mask in range(1<<(2*length+1)): + val=0 + for j in range(1,length+1): + old=(mask&((1<<(2*j))-1)).bit_count();even=mask>>(2*j)&1 + val+=224*(hi[1+8*(old+even)]-lo[8*old]-even*lo[8]) + n=mask.bit_count();result[n]=max(result.get(n,val),val) + return result + +def monotonicity(E,h,paid): + lg=E.log_bounds(8);lower=Q(paid[1]-112,8)*lg[0] + for r,v in h.items(): + if r<8:lower-=v*(lg[1]-E.log_bounds(r)[0]) + need(lower>0 and max(paid)<=8 and min(h)>=1,'Strict separator derivative') + return str(lower) + +def literal_control(h,paid): + row=read(ROOT/'research/joint-helper-lattice/CONTROLLER.json');T,P=Counter(),Counter() + for e in row['physical_events']: + if e[0]=='LOCAL':T.update(h);P.update(paid) + elif e[0]=='QUERY_SHEAR':P[1]+=112 + elif e[0]=='IDLE':P[8*len(e[2])]+=224 + for term in row['diagonal']:T[1+8*sum(term[1:])]+=112 + mask=sum(1<0,'Omitting real middle-idle work changes sign') + duplicate,_=maximum(env,lo,hi,{r:2*v for r,v in h.items()},paid) + need(duplicate>0,'Duplicate helper credit changes sign') + print('CEILING_AND_CONTROLS_PASS',flush=True);funding={};optimistic=dict(paid);optimistic[1]+=8;del optimistic[8] + for tested in (Q('.004'),Q('.006'),Q('.01')): + low,high=weights(E,tested);ee=envelope(low,high);val,args=maximum(ee,low,high,h,optimistic) + T,P=invoice(*args,h,optimistic);a,b=E.moment(T,1-tested),E.moment(P,1-tested) + funding[str(tested)]={'best_surplus_upper':str(Q(val,SCALE)),'witness_surplus_lower':str(a[0]-b[1]),'witness_parameters':args,'status':'OPTIMISTIC_INVOICE_ONLY_NO_H_NATIVE_ADMISSION'} + print('BUDGET_READY',tested,flush=True) + return {'status':'PASS_EXACT_STAGE_FAMILY_CEILING','ceiling':str(c),'pair_counts':[1,MAX_P],'all_splits':True,'all_native_stage_subsets':True,'patterns_per_profile':str(sum(p*(1<<(2*p+1)) for p in range(1,MAX_P+1))),'fixed_point_scale':str(SCALE),'profiles':receipt,'optimistic_H_repair_budgets':funding,'controls':['all_5_small_arm_censuses','all_complete_patterns_p1_to_p3','all_3_literal_p16_invoices','missing_middle_idle_changes_sign','duplicate_helper_credit_changes_sign'],'new_kappa':None,'scope':'Frozen native invoices and minimal-cut path family, p<=64. No global operator/controller ceiling or new supplier.'} + +if __name__=='__main__': + p=argparse.ArgumentParser(description=__doc__);p.add_argument('--write',action='store_true');args=p.parse_args();result=run();target=HERE/'RESULT.json' + if args.write:target.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else:need(read(target)==json.loads(json.dumps(result)),'Exact stored receipt') + print(json.dumps(result,indent=2,sort_keys=True))