diff --git a/research/four-shear-window-ceilings/README.md b/research/four-shear-window-ceilings/README.md new file mode 100644 index 0000000000..ff2f5b858a --- /dev/null +++ b/research/four-shear-window-ceilings/README.md @@ -0,0 +1,40 @@ +# Four-shear ceilings for twelve receiver windows + +**All twelve windows have certified zero headroom at C=0.00302015. No new kappa.** Assignment B independently covers every word of at most four unit shears on the same three persistent fields and fixed boundaries used by fork PR15. Even a favourable geometric relaxation cannot improve their paid moment. [RESULT.json](RESULT.json) retains the exact source-bound receipt; [VALIDATION.md](VALIDATION.md) records the passing hosted replay. + +## Complete alphabet and scope + +The twelve generators are y_i += sign*y_j for i != j and sign in {-1,1}. Every word of lengths zero through four is enumerated, including cancellations: 22,621 words. For each of the four sign choices exactly 84 words have the required exact integer 3 by 3 receiver endpoint, comprising two length-two, two length-three and eighty length-four words. No heuristic pruning or floating-point equality is used. + +The source has 128 eligible adjacent pairs. Only the explicitly bounded first twelve are tested; all are in phase B. Each has all 84 matching words admitted by the dimension screen. Ten windows have one relaxed paid profile, and the two at indices 10575 and 10579 have four. Every profile's directed gain upper bound is nonpositive; the best is exactly zero. The original path is included, so the optimistic ceiling is attained by the incumbent. This does not cover the other 116 windows or joint changes to overlapping windows. + +## Why the relaxation is a valid ceiling + +For each endpoint-matching word, propagate mandatory lower subspaces forward. At a contact of fields i,j, every legal common frame contains the sum of their current lower bounds; update both to that sum. Propagate permissible upper subspaces backwards from the fixed exits, replacing both operands' bounds by their intersection. Induction gives L_j contained in F_j contained in U_j for every actual monotone path. If L_j is not contained in U_j, the word is impossible under this contract. + +For surviving words, enumerate every integer contact dimension between dim(L_j) and dim(U_j), nondecreasing along each operand's path and bounded by its fixed terminal dimension. Charge each positive entrance/intermediate gap and every remaining exit gap. The sum of charged ranks equals total terminal-minus-entrance rank mass. Forgetting simultaneous incidence constraints can add profiles, never remove a legal one. Thus minimum relaxed paid moment is a lower bound on legal cost, and old cost minus that lower bound is an upper bound on possible gain. + +All distinct relaxed profiles are retained. Directed rational intervals bound signed old-minus-new costs, with identical profiles treated as exact equality. The independent power method uses binary-reduced logarithms and an alternating expansion of r*exp(-C log r). Optimistic positive profiles would not establish a construction; here none exists. Individual window gains must never be summed across overlapping operations or shared resources. + +## Reproduction and independence + +Python 3.12, standard library only: + +```sh +python -B scripts/research_package.py --package research/four-shear-window-ceilings +python -I -O -B research/four-shear-window-ceilings/verify.py --self-test +``` + +The registered source-bound replay passed on CPython 3.12.15, including normal verification, optimised controls and preservation of committed inputs. Seven source files are pinned by Git blob and SHA256. The inherited constructor emits candidate data only; no predecessor proof engine or PR15 acceptance routine is imported. Window extraction, scalar enumeration, relaxation and interval arithmetic are separately implemented. Normal replay compares the full retained receipt without rewriting it. Exact small-domain controls include 68 actual geometric paths plus exit-charge, incompatible-exit and equality checks. + +## Task and overlap + +Canonical base f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc, priority revision 7; PR4470 source b9a13c1673e0e9697de410de16e8bbf3207a7363. TASK.json records the refined independent-moment assignment. PR4121 uses older T360 sources; #4091's fixed-inventory ceiling is not transferred outside its hypotheses. PR4529/4532/4533 concern compiler gates and ranks. Searches were targeted, not exhaustive overlap pagination or proof of novelty. The historical baseline helper was not run. No selected record or frozen input changed. + +## Open next questions + +Do not reseed this exact domain. A useful next experiment must change the length cap, coefficient alphabet, adjacency, owned-field allowance or producer/consumer boundary explicitly and reprice the complete contract. Another window is outside the certificate but should have a concrete structural reason for investigation. Physical lowering, full native correctness and consumer transfer remain necessary for any later positive candidate. TASK.json records the next question and blockers. + +## Credit + +Credit zxv's receiver-sharing and productive-helper work, Cinna Davis's PR4470, Jacob Alan Sussman, GamingPuzzled's earlier finite census and the retained native/Clifford/geometry/outer contributors. Prepared for Chris R / Clear1nsight with substantial OpenAI assistance, Apache-2.0. Separate implementations in one session do not imply separately launched agents, independent human review or formal acceptance. diff --git a/research/four-shear-window-ceilings/RECEIPT-COMPARISON.md b/research/four-shear-window-ceilings/RECEIPT-COMPARISON.md new file mode 100644 index 0000000000..47c8ce7bf3 --- /dev/null +++ b/research/four-shear-window-ceilings/RECEIPT-COMPARISON.md @@ -0,0 +1,5 @@ +# Canonical JSON receipt adapter + +The fresh scientific result uses integer rank keys in Python dictionaries; JSON object keys are strings. The original direct main function compares those Python objects before normalisation, so it cannot verify an otherwise identical stored result. The registered entry point is now replay.py, which authenticates the unchanged scientific engine at blob 804451f1b6a420d32cb2f4bc660c23550021badb, executes run() with every source and mathematical check, and compares every field in canonical JSON form. It never invokes the --write authoring path or changes RESULT.json. + +Only object order and JSON's required string key representation are normalised. No value is rounded or omitted. Arrays remain ordered and encoded boolean/integer and integer/float values remain distinct. Six controls reject changed counts, types, array order and missing/extra fields in normal and optimised modes. Use the registered command or replay.py for the stored receipt; the original --self-test remains valid. This adapter preserves scientific evidence rather than changing acceptance predicates. diff --git a/research/four-shear-window-ceilings/RESULT.json b/research/four-shear-window-ceilings/RESULT.json new file mode 100644 index 0000000000..f2f411003d --- /dev/null +++ b/research/four-shear-window-ceilings/RESULT.json @@ -0,0 +1 @@ +{"controls":{"actual_small_paths_checked":68,"enumerated_words_per_sign_case":22621,"exact_equality_control":true,"exit_charge_control":true,"incompatible_exit_control":true,"word_counts":{"(-1, -1)":84,"(-1, 1)":84,"(1, -1)":84,"(1, 1)":84}},"excluded_window_count":12,"new_kappa":false,"not_covered":["geometric attainability of relaxed profiles","nonadjacent or larger windows","joint overlapping rewrites","physical native admission","global ceiling or new kappa"],"scale":1000000000000000000,"schema":"four-shear-window-ceilings/v1","source_head":"b9a13c1673e0e9697de410de16e8bbf3207a7363","status":"PASS_FINITE_ALPHABET_CEILINGS","tested_saving":"60403/20000000","tested_windows":12,"total_eligible_windows":128,"windows":[{"certified_no_strict_gain":true,"coefficients":[-1,1],"compatible_words":84,"exit_dimensions":[0,2,0],"index":10554,"old_paid":{"2":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":2,"phase":"B","relaxed_profiles":1,"roles":[162,172,513],"start_dimensions":[0,0,0]},{"certified_no_strict_gain":true,"coefficients":[1,1],"compatible_words":84,"exit_dimensions":[2,0,0],"index":10555,"old_paid":{"2":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":3,"phase":"B","relaxed_profiles":1,"roles":[172,196,513],"start_dimensions":[0,0,0]},{"certified_no_strict_gain":true,"coefficients":[1,-1],"compatible_words":84,"exit_dimensions":[2,1,1],"index":10557,"old_paid":{"1":3},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":5,"phase":"B","relaxed_profiles":1,"roles":[140,144,502],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[-1,1],"compatible_words":84,"exit_dimensions":[1,1,1],"index":10558,"old_paid":{"1":2},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":6,"phase":"B","relaxed_profiles":1,"roles":[144,187,502],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[1,1],"compatible_words":84,"exit_dimensions":[1,2,1],"index":10560,"old_paid":{"1":3},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":8,"phase":"B","relaxed_profiles":1,"roles":[168,150,548],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[1,-1],"compatible_words":84,"exit_dimensions":[2,1,1],"index":10561,"old_paid":{"1":3},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":9,"phase":"B","relaxed_profiles":1,"roles":[150,115,548],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[1,-1],"compatible_words":84,"exit_dimensions":[2,1,1],"index":10563,"old_paid":{"1":3},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":11,"phase":"B","relaxed_profiles":1,"roles":[131,117,560],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,1,1],"index":10564,"old_paid":{"1":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":12,"phase":"B","relaxed_profiles":1,"roles":[117,584,560],"start_dimensions":[0,1,1]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,2,3],"index":10575,"old_paid":{"1":1,"2":1,"3":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":23,"phase":"B","relaxed_profiles":4,"roles":[205,170,452],"start_dimensions":[0,0,0]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,1,3],"index":10577,"old_paid":{"1":2,"2":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":25,"phase":"B","relaxed_profiles":1,"roles":[118,194,453],"start_dimensions":[0,0,1]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,2,3],"index":10579,"old_paid":{"1":1,"2":1,"3":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":27,"phase":"B","relaxed_profiles":4,"roles":[120,207,454],"start_dimensions":[0,0,0]},{"certified_no_strict_gain":true,"coefficients":[-1,-1],"compatible_words":84,"exit_dimensions":[1,1,3],"index":10581,"old_paid":{"1":2,"2":1},"optimistic_gain_upper_scaled":0,"optimistic_positive_profiles":0,"ordinal":29,"phase":"B","relaxed_profiles":1,"roles":[192,179,455],"start_dimensions":[0,0,1]}]} diff --git a/research/four-shear-window-ceilings/SOURCES.json b/research/four-shear-window-ceilings/SOURCES.json new file mode 100644 index 0000000000..443dcd0ada --- /dev/null +++ b/research/four-shear-window-ceilings/SOURCES.json @@ -0,0 +1 @@ +{"schema_version":1,"base_commit":"f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc","files":[{"path":"certificates/selected-result.json","usage":"provenance","git_blob":"ed33caef5c5827693e9572d252a66f99cbb73d40","sha256":"5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"},{"path":"docs/research/agent-task-catalog.json","usage":"provenance","git_blob":"64bfc5af6709ed9811171e0a2108f05e1219cb65","sha256":"352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"},{"path":"research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz","usage":"input","git_blob":"4a8c4ed26e53a72362d571c972e65aff546be784","sha256":"6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61"},{"path":"research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz","usage":"input","git_blob":"b46d44c6ee624968dd57be928b0c15d9d45f3b2c","sha256":"c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39"},{"path":"research/fresh-helper-boundary/native.py","usage":"input","git_blob":"1b36f6cb5f205c33bf48811e0b1b3621c55e8154","sha256":"9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29"},{"path":"research/fresh-helper-boundary/CHANGES.json","usage":"input","git_blob":"45744fedd0e28967aa72586048b8bc0c72f419a9","sha256":"cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624"},{"path":"research/missing-join-frame/PATCH.json","usage":"input","git_blob":"f96d295d40014d4dd503f58eb3cdabcbb4b8e101","sha256":"9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e"},{"path":"research/joint-helper-lattice/PATCH.json","usage":"input","git_blob":"51304a6601061ed4e698f910b09135ef109555e3","sha256":"296d0e8c58cc70febe042c681ef30d6bb469818c0835fbcaac8aa8d330f5b727"},{"path":"research/joint-helper-lattice/native_joint.py","usage":"input","git_blob":"0315f80e2fdef5e0eef13e3e9b8f72066238164d","sha256":"50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46"}]} diff --git a/research/four-shear-window-ceilings/TASK.json b/research/four-shear-window-ceilings/TASK.json new file mode 100644 index 0000000000..c98527387b --- /dev/null +++ b/research/four-shear-window-ceilings/TASK.json @@ -0,0 +1 @@ +{"schema_version":1,"task_id":"independent-moment","priority_revision":7,"base_commit":"f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc","original_card":{"id":"independent-moment","question":"Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?","starting_points":["docs/research/research-family-status.md","certificates/selected-result.json","research/staged544-mixed-fourth-entry/README.md","research/staged-fourth-mixture-ceiling/README.md","research/r437-two-window-carrier/README.md"],"methods":["Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.","Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."],"acceptance_gate":"Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.","first_step":{"command":["python3","-B","scripts/research_baseline.py"],"expected":"PASS_RESEARCH_BASELINE_BINDINGS_ONLY","inspect":"Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.","scope":"Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."},"first_experiment":"Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.","bottleneck_link":"Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.","allowed_variations":["Reconstruct either a source ledger or a numeric enclosure with a different method."],"scope_change_triggers":["Importing the primary function and calling its output independent verification.","Calling an aggregate histogram or source archive an independently accepted physical supplier."],"overlap_terms":["independent moment","rank histogram","exact enclosure","2979","rank7 joint endframes","paired extraction","joint lowering","4088","4091","4067","staged544-mixed-fourth-entry","staged-fourth-mixture-ceiling","r437-two-window-carrier"],"existing_checks":[{"scope":"PR #4088: mixed local/owner/phase ledger and moment reported.","evidence":"research/staged544-mixed-fourth-entry/README.md","remaining":"Independent binding of changed construction to paid histogram, distinct from full admission.","status":"author-checked","source_commit":"72d7efc181edb21806a878f174847c96dd410ab0","selected_record_sha256":"bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"},{"scope":"PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.","evidence":"research/staged-fourth-mixture-ceiling/README.md","remaining":"Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.","status":"author-checked","source_commit":"a29bdd8f56cd18b805917775cdec09ff935eddc4","selected_record_sha256":"bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"},{"scope":"PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.","evidence":"research/r437-two-window-carrier/README.md","remaining":"Independent full cost delta; remaining caller/precision/stock obligations are separate.","status":"author-checked","source_commit":"a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e","selected_record_sha256":"bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"}]},"scope_status":"refined","actual_scope":"Assignment B: exact finite-alphabet optimistic ceilings for twelve PR4470 receiver windows, all words of at most four unit shears with fully charged monotone dimension paths.","scope_change_reason":"User-requested ceiling support alongside construction. The alphabet is larger than the three-shear construction, while simultaneous geometry is relaxed only towards lower costs.","bottleneck_link":"Avoid expanding a rewrite domain with no complete paid-moment headroom, without mistaking optimistic profiles for circuits.","budget_minutes":60,"stop_rule":"Stop at twelve individual fixed-window ceilings; do not add overlapping gains, reseed an excluded domain or claim a universal barrier.","outcome":"negative-result","evidence":"Hosted registered replay 39724143539 at dce9576ec448af52009ec13a4f8c1a740fb4a8d8 passes CPython 3.12.15. All twelve windows have exact optimistic gain upper bound zero. Each includes all 84 endpoint-matching words from 22621 enumerated words per sign case. Ten windows have one relaxed profile, two have four. RESULT.json preserves all observed fields. Normal and optimised controls, 68 legal toy paths and committed-input preservation pass. Receipt-retention metadata used negative and was corrected to the schema's negative-result value without changing science or evidence.","author":"Chris R / Clear1nsight","ai_assistance":"Substantial OpenAI assistance; separate implementation in one session, not independently launched agents, human review or formal-kernel acceptance.","overlap":{"nearby_prs":[4085,4091,4121,4359,4470,4478,4483,4504,4529,4532,4533],"fork_companion":15,"method":"Targeted searches and bounded Discussion reads, not exhaustive pagination or novelty proof.","baseline_helper_run":false,"canonical_refresh":"2026-10-22T04:44:00Z"},"open_questions":[{"question":"Which explicit changed contract can escape the twelve-window four-shear ceiling?","why_it_matters":"A new seed in the same finite domain cannot improve its exact ceiling.","first_step":"Change one of length cap, coefficients, adjacency, owned-field allowance or producer/consumer boundary, derive the fully charged optimistic model and test one structurally justified window.","blocked_by":"No conclusion about the other 116 windows, larger or joint rewrites, physical lowering or complete consumer admission is supplied."}]} diff --git a/research/four-shear-window-ceilings/VALIDATION.md b/research/four-shear-window-ceilings/VALIDATION.md new file mode 100644 index 0000000000..57f6fdb3f3 --- /dev/null +++ b/research/four-shear-window-ceilings/VALIDATION.md @@ -0,0 +1,11 @@ +# Executed finite-domain ceiling evidence + +The first source-bound registered replay passed in [workflow 39724143539](https://github.com/Clear1nsight/integer-mult-bounds/actions/runs/39724143539), job 119644988257, at head dce9576ec448af52009ec13a4f8c1a740fb4a8d8. GitHub tested merge ref ceb38f099bd3f2e9366cd131527c92843f2a2a17 against isolated base 59d57c8c662e62b9a03f5ebd6ba52ebdd19ed20b. Ubuntu 24.04.5, CPython 3.12.15, standard library only. Scientific execution completed at 2026-10-22T04:49:42Z. Onboarding, metadata/source authentication, full ceiling replay, optimised controls and unchanged committed inputs passed. + +All twelve tested windows have certified optimistic gain upper bound zero at C=0.00302015. Every one of the 84 exact endpoint-matching words per sign case is included. Ten windows admit only the original paid profile even in the relaxation; the two at indices 10575 and 10579 admit four relaxed profiles, none improving. The source has 128 eligible adjacent pairs, but the declared domain is only the first twelve, all in phase B. No exclusion of the other 116 windows, nonadjacent rewrites, longer words, nonunit coefficients, extra fields or changed boundary contracts follows. + +RESULT.json preserves every field of the observed scientific JSON output. Normal replay compares fresh output with this receipt, without rewriting it. The checker and exact scientific inputs were unchanged when retaining the receipt. A separate local comparison using the twelve boundary fixtures observed in PR15's hosted output reproduces every ceiling row; this is a cross-check, not a second fresh source extraction. + +The complete scalar enumeration visits 22,621 words for each of four sign choices and finds 84 matches per choice. Exact toy controls include all 68 actual legal geometric paths in the declared small domain, obligatory exit charges, incompatible exits and exact equal-profile handling. The written forward/backward containment induction proves that the relaxation cannot exclude an actual legal path; the finite fixtures do not substitute for that argument. + +No physical normal-form lowering, complete native endpoint, compiler/outer transfer, global optimum, selected-frontier cold replay or optional publication source-history preflight was run. The result is a bounded no-headroom certificate, not a new multiplication theorem or new kappa. Read the current PR checks for later publication heads. diff --git a/research/four-shear-window-ceilings/VERIFY.json b/research/four-shear-window-ceilings/VERIFY.json new file mode 100644 index 0000000000..e3b401ce86 --- /dev/null +++ b/research/four-shear-window-ceilings/VERIFY.json @@ -0,0 +1 @@ +{"schema_version":1,"status":"ready","python":"3.12","requirements":[],"inputs":["research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz","research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz","research/fresh-helper-boundary/native.py","research/fresh-helper-boundary/CHANGES.json","research/missing-join-frame/PATCH.json","research/joint-helper-lattice/PATCH.json","research/joint-helper-lattice/native_joint.py"],"commands":[{"argv":["{python}","-I","-B","{package}/replay.py"],"timeout_seconds":300,"checks":"Fresh unchanged authenticated finite-alphabet engine, every source/geometry/interval check, full canonical JSON receipt comparison and six comparison rejection controls."},{"argv":["{python}","-I","-O","-B","{package}/verify.py","--self-test"],"timeout_seconds":60,"checks":"Original complete word census, 68 actual geometric paths and exit/domain/equality controls under optimised Python."},{"argv":["{python}","-I","-O","-B","{package}/replay.py","--self-test"],"timeout_seconds":60,"checks":"Reject altered counts, boolean/integer and integer/float substitutions, reordered arrays and missing/extra receipt fields under optimised Python."}]} diff --git a/research/four-shear-window-ceilings/replay.py b/research/four-shear-window-ceilings/replay.py new file mode 100644 index 0000000000..a7bfe6d3fe --- /dev/null +++ b/research/four-shear-window-ceilings/replay.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 +"""Canonical JSON replay of the unchanged finite-ceiling engine. + +JSON object keys are strings; fresh Python rank keys are integers. +All encoded fields and values remain checked. Apache-2.0; OpenAI assistance. +""" +from pathlib import Path +import argparse +import hashlib +import importlib.util +import json + +HERE=Path(__file__).resolve().parent +ENGINE='804451f1b6a420d32cb2f4bc660c23550021badb' + +def canonical(value): + encoded=json.dumps(value,allow_nan=False) + return json.dumps(json.loads(encoded),sort_keys=True,separators=(',',':'),allow_nan=False) + +def compare(expected,actual): + if canonical(expected)!=canonical(actual):raise ValueError('Complete scientific receipt mismatch') + +def controls(): + actual={'paid':{1:2},'flag':True,'ordered':[1,2]} + expected=json.loads(json.dumps(actual));compare(expected,actual) + bads=[{**actual,'paid':{1:3}},{**actual,'flag':1},{**actual,'paid':{1:2.0}}, + {**actual,'ordered':[2,1]},{**actual,'extra':0},{'paid':{1:2},'flag':True}] + for bad in bads: + try:compare(expected,bad) + except ValueError:pass + else:raise ValueError('Receipt mutation accepted') + return 6 + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--self-test',action='store_true');args=ap.parse_args() + n=controls() + if not args.self_test: + path=HERE/'verify.py';raw=path.read_bytes() + digest=hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() + if path.is_symlink() or digest!=ENGINE:raise ValueError('Scientific engine changed') + spec=importlib.util.spec_from_file_location('ceiling_scientific_engine',path) + engine=importlib.util.module_from_spec(spec);spec.loader.exec_module(engine) + fresh=engine.run();compare(json.loads((HERE/'RESULT.json').read_bytes()),fresh) + print(json.dumps(fresh,indent=2,sort_keys=True)) + print('PASS_CANONICAL_RECEIPT_CONTROLS rejected='+str(n)) + +if __name__=='__main__':main() diff --git a/research/four-shear-window-ceilings/verify.py b/research/four-shear-window-ceilings/verify.py new file mode 100644 index 0000000000..804451f1b6 --- /dev/null +++ b/research/four-shear-window-ceilings/verify.py @@ -0,0 +1,223 @@ +#!/usr/bin/env python3 +"""Independent finite-alphabet optimistic ceilings. Apache-2.0; OpenAI assistance. + +No construction checker or acceptance function is imported. Geometry is relaxed +only in the direction that can lower cost; optimistic profiles are not circuits. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from itertools import product +from pathlib import Path +import argparse +import hashlib +import json +import subprocess +import sys +import tempfile + +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +SCALE=10**18;SAVING=Q('0.00302015') +GATES=tuple((i,j,s) for i in range(3) for j in range(3) if i!=j for s in (-1,1)) +IDENTITY=tuple(int(i==j) for i in range(3) for j in range(3)) + +def need(ok,why): + if not ok:raise ValueError(why) + +def apply(m,g): + i,j,s=g;out=list(m) + for k in range(3):out[3*i+k]+=s*m[3*j+k] + return tuple(out) + +@lru_cache(None) +def matching_words(ca,cb): + target=apply(apply(IDENTITY,(0,2,ca)),(1,2,cb)) + layer=[(IDENTITY,())];found=[];visited=0 + for length in range(5): + visited+=len(layer) + found.extend(w for m,w in layer if m==target) + if length<4:layer=[(apply(m,g),w+(g,)) for m,w in layer for g in GATES] + need(visited==22621,'Complete length-zero-through-four alphabet') + return tuple(found) + +@lru_cache(None) +def span(basis): + values={0} + for v in basis: + need(type(v) is int and 0a:hh[b-a]+=1 + need(sum(r*n for r,n in enumerate(hh))==sum(end)-sum(initial),'Complete exit rank mass') + out.add(tuple(hh));return + i,j,_=word[k];lo,hi=bounds[k] + for d in range(max(lo,state[i],state[j]),min(hi,end[i],end[j])+1): + hh=list(h);ss=list(state) + for role in (i,j): + gap=d-ss[role] + if gap:hh[gap]+=1 + ss[role]=d + visit(k+1,tuple(ss),tuple(hh)) + visit(0,initial,(0,)*10) + return out + +def actual_profile(starts,ends,word,frames): + state=list(starts);out=[0]*10 + for (i,j,_),f in zip(word,frames): + for r in (i,j): + if not state[r]<=f:return None + gap=dim(f)-dim(state[r]);out[gap]+=int(gap>0);state[r]=f + for a,b in zip(state,ends): + if not a<=b:return None + gap=dim(b)-dim(a);out[gap]+=int(gap>0) + need(sum(r*n for r,n in enumerate(out))==sum(map(dim,ends))-sum(map(dim,starts)),'Actual cleanup mass') + return tuple(out) + +def logarithm(x): + e=0 + while x>=2:x/=2;e+=1 + def core(y): + z=(y-1)/(y+1);p=z;lo=Q(0) + for k in range(96):lo+=2*p/(2*k+1);p*=z*z + return lo,lo+2*p/(193*(1-z*z)) + a,b=core(x);c,d=core(Q(2));return a+e*c,b+e*d + +def weights(): + out=[(0,0),(SCALE,SCALE)] + for r in range(2,10): + a,b=logarithm(Q(r));a*=SAVING;b*=SAVING + need(0=0 else 1] for r,n in enumerate(delta)), + sum(n*w[r][1 if n>=0 else 0] for r,n in enumerate(delta))) + +def authenticate(): + for r in json.loads((HERE/'SOURCES.json').read_bytes())['files']: + if r['usage']!='input':continue + p=ROOT/r['path'];need(p.is_file() and not p.is_symlink(),'Source location') + b=p.read_bytes();need(hashlib.sha256(b).hexdigest()==r['sha256'],'Source SHA256') + need(hashlib.sha1(b'blob '+str(len(b)).encode()+b'\0'+b).hexdigest()==r['git_blob'],'Source blob') + +def source(): + authenticate() + with tempfile.TemporaryDirectory(prefix='ceiling-source-cache-') as cache: + code="import json,sys;sys.path.insert(0,sys.argv[1]);import native_joint;c,p,b,o,n=native_joint.construct();print(json.dumps({'c':c,'p':p['forward']}))" + run=subprocess.run([sys.executable,'-I','-B','-X','pycache_prefix='+cache,'-c',code,str(ROOT/'research/joint-helper-lattice')],capture_output=True,check=True,timeout=60) + return json.loads(run.stdout) + +def windows(c,program): + word=[e for e in program if e[0]!='climb'];state=list(c['start']);phase=None;ordinals=Counter();out=[] + def roles(e): + g=e[1];return g[1:3] if g[0] in ('add','copy') else g[1:2] + for pos,e in enumerate(word): + if e[0]=='phase':phase=e[1] + ordinal=ordinals[phase] + if e[0]=='scalar' and all(r[0]=='L' for r in roles(e)):ordinals[phase]+=1 + if phase in ('B','cleanup_tail') and pos+13:continue + starts=[spaces[0]]*3;ends=[spaces[-1]]*3;relax=relaxed_profiles(starts,ends,word) + for fs in product(spaces,repeat=len(word)): + p=actual_profile(starts,ends,word,fs) + if p is not None:need(p in relax,'Relaxation excluded an actual path');checked+=1 + p=actual_profile([spaces[0]]*3,[spaces[1]]*3,(),()) + need(p[1]==3 and p!=(0,)*10,'Exit charges may not be omitted') + need(not relaxed_profiles([span((4,))]*3,[span((1,2))]*3,((0,1,1),)),'Incompatible exits') + w=weights();need(gain(p,p,w)==(0,0),'Identical invoice is exact equality') + return dict(word_counts=counts,enumerated_words_per_sign_case=22621,actual_small_paths_checked=checked, + exit_charge_control=True,incompatible_exit_control=True,exact_equality_control=True) + +def run(): + tests=self_tests();data=source();allwindows=windows(data['c'],data['p']);w=weights();results=[] + for info,starts,ends,oldframes in allwindows[:12]: + a,b=info['coefficients'];old=actual_profile(starts,ends,((0,2,a),(1,2,b)),oldframes) + need(old is not None,'Actual source path') + ps=set();admitted=0 + for word in matching_words(a,b): + found=relaxed_profiles(starts,ends,word) + if found:admitted+=1;ps.update(found) + need(old in ps,'Relaxation includes original source word') + intervals=[gain(old,p,w) for p in sorted(ps)] + ceiling=max(hi for lo,hi in intervals) + results.append({**info,'compatible_words':admitted,'relaxed_profiles':len(ps), + 'optimistic_gain_upper_scaled':ceiling,'certified_no_strict_gain':ceiling<=0, + 'optimistic_positive_profiles':sum(lo>0 for lo,hi in intervals), + 'old_paid':{r:n for r,n in enumerate(old) if n}, + 'start_dimensions':list(map(dim,starts)),'exit_dimensions':list(map(dim,ends))}) + return dict(schema='four-shear-window-ceilings/v1',status='PASS_FINITE_ALPHABET_CEILINGS', + source_head='b9a13c1673e0e9697de410de16e8bbf3207a7363',tested_saving=str(SAVING),scale=SCALE, + total_eligible_windows=len(allwindows),tested_windows=len(results),windows=results, + excluded_window_count=sum(r['certified_no_strict_gain'] for r in results),controls=tests,new_kappa=False, + not_covered=['geometric attainability of relaxed profiles','nonadjacent or larger windows','joint overlapping rewrites','physical native admission','global ceiling or new kappa']) + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--self-test',action='store_true');ap.add_argument('--write',action='store_true');args=ap.parse_args() + result=self_tests() if args.self_test else run();text=json.dumps(result,indent=2,sort_keys=True)+'\n' + if args.write:(HERE/'RESULT.json').write_text(text) + elif not args.self_test and (HERE/'RESULT.json').exists():need(json.loads((HERE/'RESULT.json').read_bytes())==result,'Receipt changed') + print(text,end='') + +if __name__=='__main__':main()