From 7207b930f8362bf1cf95d8a3ee9c3596948e2dd8 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Mon, 26 Oct 2026 15:38:47 -0700 Subject: [PATCH] Certify a current-budget obstruction for the fixed unpooled R437 moment contract --- .../r437-unpooled-budget-obstruction/NOTICE | 31 +++ .../ORACLE.json | 107 ++++++++ .../r437-unpooled-budget-obstruction/PROOF.md | 137 +++++++++++ .../README.md | 57 +++++ .../RESULT.json | 192 +++++++++++++++ .../SOURCES.json | 95 +++++++ .../TASK.json | 88 +++++++ .../VERIFY.json | 47 ++++ .../oracle.py | 232 ++++++++++++++++++ .../source/HOST-RESULT.json | 122 +++++++++ .../source/ORDINARY-TRANSFER-PROOF.md | 165 +++++++++++++ .../source/SELECTED-CLAIM.json | 33 +++ .../source/SELECTED-RECORD.json | 112 +++++++++ .../source/host.py | 167 +++++++++++++ .../verify.py | 222 +++++++++++++++++ 15 files changed, 1807 insertions(+) create mode 100644 research/r437-unpooled-budget-obstruction/NOTICE create mode 100644 research/r437-unpooled-budget-obstruction/ORACLE.json create mode 100644 research/r437-unpooled-budget-obstruction/PROOF.md create mode 100644 research/r437-unpooled-budget-obstruction/README.md create mode 100644 research/r437-unpooled-budget-obstruction/RESULT.json create mode 100644 research/r437-unpooled-budget-obstruction/SOURCES.json create mode 100644 research/r437-unpooled-budget-obstruction/TASK.json create mode 100644 research/r437-unpooled-budget-obstruction/VERIFY.json create mode 100644 research/r437-unpooled-budget-obstruction/oracle.py create mode 100644 research/r437-unpooled-budget-obstruction/source/HOST-RESULT.json create mode 100644 research/r437-unpooled-budget-obstruction/source/ORDINARY-TRANSFER-PROOF.md create mode 100644 research/r437-unpooled-budget-obstruction/source/SELECTED-CLAIM.json create mode 100644 research/r437-unpooled-budget-obstruction/source/SELECTED-RECORD.json create mode 100644 research/r437-unpooled-budget-obstruction/source/host.py create mode 100644 research/r437-unpooled-budget-obstruction/verify.py diff --git a/research/r437-unpooled-budget-obstruction/NOTICE b/research/r437-unpooled-budget-obstruction/NOTICE new file mode 100644 index 0000000000..091a9c4fb2 --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/NOTICE @@ -0,0 +1,31 @@ +Retained source contributions and licenses: + +Chris R / Clear1nsight with substantial OpenAI Codex assistance, Apache-2.0: +PR4067 two-window R437 carrier, complete fixed OQ4 host, paid profile and price. +The source already establishes its word/geometry/dirty-state and local gain; +this package does not claim those constructions or rederive the root. + +Retain ai-nanachi/PR3647 for R437 and helper464 deletion; Ali Romman/PR1043 +for SOURCE77-carrier deletion; Sagar Thakrar/PR3700 and PR2423 for OQ4 and +independent checks; PR4005/Chris R for the source-quotient cut and boundary +handoff; mightyOil/PR1281 and Rohan Arun/PR3959 for packing/pooled context; +eumemic, DreamingOfClouds, DaysSky, Crow, chafreaky and retained notices for +word, geometry, native, hosting and compiler lineage. +The source host lowering, owner-invoice pattern and rational interval +technique adapt the credited PR3647/3700 audit. + +zxv/PR3690 supplies the source-relative ordinary recurrence/transfer argument. +unpaidmoon/PR4147 supplies the reverse-row coefficient follow-up and distinction +between arithmetic envelope values and physical caller-bound admission. +Retain Mihir Srivastava, JoyboyBrian, Krzysztof Wojt, commdata2338, +Jose Manuel/jmbarrancoml, David Arias, Nick Petalas, ywz65 and the actual +physical/caller/stock/pooling lineage in Discussion4682 and its linked packages. +Current selected conditional P104/frontier5599 certificate and all inherited +native/compiler/precision/tape/analytic authors retain their original credit. + +New fixed-unpooled current-budget implication, checker, independent integer +oracle and scoped proof: ToikY with substantial OpenAI Codex assistance in +separate primary, independent-oracle and proof-review contexts. Apache-2.0. +Classical log/exp inequalities are not claimed as new general discoveries. +No independent human or proof-kernel acceptance, physical theorem extension, +full supplier admission or selected-frontier change is claimed. diff --git a/research/r437-unpooled-budget-obstruction/ORACLE.json b/research/r437-unpooled-budget-obstruction/ORACLE.json new file mode 100644 index 0000000000..ab225ebdff --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/ORACLE.json @@ -0,0 +1,107 @@ +{ + "controls": { + "changed_profile_rank42_to_rank1": { + "bound": { + "A": "18673/18944", + "B": "4287625175886659/2380780979216640", + "base_denominator": 1818624, + "common_log_denominator": 335132457660, + "integer_cross_product_gap": -24934285326954060032, + "integer_lower_denominator": 3047399653397299200000, + "integer_lower_numerator": 3022465368070345139968, + "lower": "694500314354399159/700229699769600000", + "lower_minus_one": "-5729385415200841/700229699769600000", + "mass": 1792608, + "saving": "17/5000", + "slope_numerator": 1097632045026984704 + }, + "meaning": "Synthetic different-profile sign control only. L<1 is not a proof that its actual moment passes or that the changed jobs have a physical realization.", + "moved_paid_jobs": 384, + "total_paid_calls_unchanged": true + }, + "rejections": { + "changed_source_byte": "Oracle exact source bytes: HOST-RESULT.json", + "different_normalization": "Oracle frozen width and normalization", + "different_profile": "Oracle frozen unpooled profile", + "negative_saving": "Oracle nonnegative saving", + "whole_kappa_as_supplier_target": "Oracle selected whole kappa is provenance, not a supplier target" + }, + "zero_saving": { + "A": "18837/18944", + "B": "227656981418642299/126181391898481920", + "base_denominator": 1818624, + "common_log_denominator": 17762020255980, + "integer_cross_product_gap": -182451472069426560, + "integer_lower_denominator": 32302436326011371520, + "integer_lower_numerator": 32119984853941944960, + "lower": "18837/18944", + "lower_minus_one": "-107/18944", + "mass": 1808352, + "saving": "0", + "slope_numerator": 58280187243172428544 + } + }, + "inequalities": [ + "For x>=1, ln(x)>=2(x-1)/(x+1): the derivative gap is (x-1)^2/[x(x+1)^2]>=0, and the gap vanishes at1.", + "For c>=0 and y=c*ln(x), exp(y)>=1+y; each paid weight is positive.", + "Therefore M0(c)>=L(c)=A+cB. B>0, so L(17/5000)>1 obstructs every c>=17/5000 in this retained moment-certification budget.", + "Under the declared necessary ordinary bridge a<=c, reaching a>=17/5000 would require such a rejected c. No physical bridge is extrapolated." + ], + "integer_certificates": { + "admitted_BIT": { + "A": "18837/18944", + "B": "227656981418642299/126181391898481920", + "base_denominator": 1818624, + "common_log_denominator": 17762020255980, + "integer_cross_product_gap": 78505822786798485248, + "integer_lower_denominator": 161512181630056857600000, + "integer_lower_numerator": 161590687452843656085248, + "lower": "37130213109568854799/37112174087788800000", + "lower_minus_one": "18039021780054799/37112174087788800000", + "mass": 1808352, + "saving": "17/5000", + "slope_numerator": 58280187243172428544 + }, + "ordinary_BIT": { + "A": "18837/18944", + "B": "227656981418642299/126181391898481920", + "base_denominator": 1818624, + "common_log_denominator": 17762020255980, + "integer_cross_product_gap": 44549682840639884280077593856, + "integer_lower_denominator": 80756090815028428800000000000000, + "integer_lower_numerator": 80800640497869068684280077593856, + "lower": "28693409267709186322542641191/28677589067836800000000000000", + "lower_minus_one": "15820199872386322542641191/28677589067836800000000000000", + "mass": 1808352, + "saving": "8590884599/2500000000000", + "slope_numerator": 58280187243172428544 + } + }, + "normalization": 28416, + "profile": { + "1": 380448, + "2": 400288, + "26": 32, + "3": 22464, + "4": 26592, + "42": 384, + "5": 29376, + "6": 17376, + "7": 26496 + }, + "scope": "Fixed unpooled invoice and retained moment-certification/contraction budget only; no runtime complexity lower bound or algorithmic impossibility. All omitted nonnegative charges are optimistic omissions, not real zero costs. The source ordinary proof fixes c=1/576 within c<1/512; it does not establish physical extension to 17/5000. Changed pooled invoices, native action, source words, compiler and full physical/stock implementation remain outside.", + "selected_stages": { + "admitted_BIT": "17/5000", + "ordinary_BIT": "8590884599/2500000000000", + "whole_kappa_provenance_only": "62009/20000000" + }, + "source_sha256": { + "HOST-RESULT.json": "000837b2b7a1e9d7e4b6b657a055c6f5f3886c7ea343239f8620f79d5d7b2ae8", + "ORDINARY-TRANSFER-PROOF.md": "29ed43abaf5451a8514dff2233ba02f44c1d3839e72035ec5711d4edf060b8f9", + "SELECTED-CLAIM.json": "66fbb5b21f32f1c4ba544c20d5a44ebcdfd11bce2bfa2d609c656ae520d3b21e", + "SELECTED-RECORD.json": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "host.py": "df01e61dc31a1cb6b2bf3549be1e2241f7a30829c2c98567f462271e3fc216ee" + }, + "status": "PASS_R437_UNPOOLED_BUDGET_ORACLE", + "width": 64 +} diff --git a/research/r437-unpooled-budget-obstruction/PROOF.md b/research/r437-unpooled-budget-obstruction/PROOF.md new file mode 100644 index 0000000000..92a73ed60f --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/PROOF.md @@ -0,0 +1,137 @@ +# A current-budget obstruction for one fixed unpooled moment contract + +This is an exact rational screen for the published PR #4067 unpooled OQ4 host, +not a runtime lower bound or a universal R437 exclusion. It fixes the paid +profile, productive normalization and moment-certification route below. +All source files are the exact current-main bytes pinned in SOURCES.json; +the predecessor host implementation is read as data, not imported or executed. + +## Source model and destination budget + +The frozen HOST-RESULT gives the new paid profile + +``` +{1:380448, 2:400288, 3:22464, 4:26592, 5:29376, + 6:17376, 7:26496, 26:32, 42:384}. +``` + +It has rank mass 1,808,352, dimension 64 and productive width W=28,416. +These are supplied predecessor host results, not a new reconstruction of the +288 calls or 125,856 hosted owner occurrences. The source `host.py:price` +uses the moment `sum n_r*(r/64)^(1-c)/W`, after adding the nonnegative rank-one +bad-event surcharge `32*64^2*E/10^16`, where E is the total paid count. + +Delete that surcharge and every other added cost as a favorable relaxation. +For c>=0 define the fixed optimistic moment + +``` +M0(c) = sum_r [n_r*r/(64*28416)] * exp(c*log(64/r)). +``` + +The **budget-contract premise** is that the proposed retained admission route +requires `M0(c)+D(c) <= 1`, where every added normalized charge D(c) is +nonnegative. Some source contraction arguments require a strict inequality; +failure even of this weak version suffices here. This premise is about that +moment-certification method. An upper-bound recurrence with a failed moment +does not prove a lower bound on actual runtime, exclude a different analysis, +or make the underlying algorithm impossible. + +The pinned selected CLAIM distinguishes three quantities: + +``` +ordinary BIT saving = 8590884599/2500000000000, +admitted BIT saving s = 17/5000, +whole multiplication kappa = 62009/20000000. +``` + +The first is strictly larger than s. Thus s is a favorable ordinary-slot +target for this screen; the smaller whole multiplication kappa is not the +ordinary moment target. No selected frontier is changed. + +## Exact lower certificate + +For x>=1, + +``` +log(x) >= 2*(x-1)/(x+1). +``` + +For example, the difference vanishes at x=1 and its derivative is +`(x-1)^2/[x*(x+1)^2] >= 0`. Also `exp(y) >= 1+y` for every real y. +All supplied ranks satisfy `0=0, so these inequalities give + +``` +M0(c) >= L(c), +L(c) = sum_r [n_r*r/(64*28416)] * [1+2*c*(64-r)/(64+r)] + = A + B*c, +A = 18837/18944, +B = 227656981418642299/126181391898481920 > 0. +``` + +No numerical logarithm, exponential approximation or root search is needed. +Exact rational evaluation at the freshly bound budget gives + +``` +L(17/5000) = 37130213109568854799/37112174087788800000, +L(17/5000)-1 = 18039021780054799/37112174087788800000 > 0. +``` + +Consequently, for **every** c>=17/5000 and **every** nonnegative added charge +D(c), `M0(c)+D(c) >= L(c) >= L(17/5000) > 1`. There is no feasible point +with c in that range for the fixed budget contract. By contrast, +`M0(0)=L(0)=18837/18944<1`; this is a positive-saving obstruction, not a claim +that the zero-saving host fails. + +## Conditional ordinary-saving bridge + +The retained PR #3690 transfer text fixes `c=1/576` and sets ordinary saving +`a=c*(1-c)`. Its physical estimates retain the historical restriction +`17/10000=s and uses this bridge, then +c>=s, contradicting the fixed moment-contract bound above. The actual pinned +ordinary saving is larger than s and therefore also cannot be reached by +that unchanged contract and bridge. + +Allowing all c>=s deliberately relaxes the historical physical range to make +the necessary algebraic test favorable. It does **not** extend PR #3690's +physical transfer theorem to c=s or to any new parameter. Within its original +range, c<1/512=2(x-1)/(x+1) for x>=1 and exp(y)>=1+y give: + +``` +M0(c) >= L(c) = A+B*c, +A = 18837/18944, +B = 227656981418642299/126181391898481920 > 0, +L(17/5000)-1 = 18039021780054799/37112174087788800000 > 0. +``` + +Thus **every c>=17/5000 fails M0(c)+D(c)<=1 for every nonnegative added normalized charge D(c)**. No numerical log, exponential or root search is used. The quantified implication is proved in PROOF.md; finite exact arithmetic authenticates its constants. + +The budget-contract premise is the retained contraction/moment gate requiring M<=1. A failed upper-bound recurrence test does not lower-bound actual runtime or exclude a different analysis. Under the separately declared ordinary bridge0<=a<=c, reaching a>=s would require one of these rejected c values. The historical #3690 text uses a=c(1-c) at c=1/576, with c<1/512 and physical refinement assumptions. Dropping that range is only a favorable mathematical relaxation. This package does not extend its physical theorem or establish physical refinement of the changed #4067 host. + +## Evidence and controls + +RESULT.json records each rational term, source/AST-site bindings, current budget stages and six controls. The separate ORACLE.json independently accumulates an integer common denominator and proves a positive cross-product gap78505822786798485248. Neither checker imports the other or executes predecessor code. + +The controls expose model dependence. At c=0, M0=L=18837/18944<1. Moving rank42jobs to rank1 preserves total paid calls and makes this lower-bound screen inconclusive, but the frozen-profile guard rejects the substitution; it is not a physically realized improvement or admission. Using whole kappa also loses this particular lower-bound rejection and is rejected as the wrong target role. Wrong productive normalization, source-byte drift and typed receipt aliases reject. The oracle additionally rejects negative saving. Default complete canonical receipt comparisons preserve bool/int/float distinctions. + +Source bytes are copied directly from current main and checked by raw SHA256/Git blob identity. The primary statically checks selected price AST sites; the complete source formula is also read and stated explicitly in the proof. This does not execute or independently replay the original host. All runtime inputs are package-local and no dependency installation is needed. + +## Reproduction + +Python3.12, standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/r437-unpooled-budget-obstruction +``` + +Registered normal/optimized primary and separate optimized oracle use explicit guards. --emit is an explicit candidate mode on stdout and never rewrites a receipt. SOURCES.json pins main ancestry separately from the mathematical contract. Metadata, committed-byte/mode, export and cold checks are integrity evidence, not supplier admission. No native, source-word, pooled compiler, full selected replay or Lean build ran. + +## Open next questions + +A different invoice, productive normalization, target allocation, transfer law or moment analysis needs its own bound. The [released pooled allocation](https://github.com/CrocSwap/integer-mult-bounds/pull/3967#issuecomment-6267387753) already exists and changes the profile; its complete pooled price and regenerated physical catalogue remain open. This result does not call that work unperformed or exclude it. The #4682 stock/payload/caller handoffs remain separate. + +Freeze a complete changed pooled invoice and receiver contract before applying this screen. Native/compiler/stock/precision/tape/analytic obligations and the five framework assumptions remain open. No selected-frontier or kappa change follows; independent acceptance remains. + +## Credit + +Chris R/Clear1nsight supplied #4067's carrier, fixed host and price; unpaidmoon supplied #4147's reverse-envelope distinction. Retain ai-nanachi/#3647, Ali Romman/#1043, Sagar Thakrar/#3700/#2423, zxv/#3690, mightyOil/#1281, Rohan Arun/#3959 and all source/native/hosting/physical/compiler/analytic authors in NOTICE. #3668/#3700 already cover historical profiles/root comparisons; no such result is claimed as new here. The new contribution is this compact revision8 budget implication and independent exact certificate. ToikY with substantial OpenAI Codex assistance in separate primary/oracle/proof-review contexts. Classical inequalities are not new general discoveries. Apache-2.0. diff --git a/research/r437-unpooled-budget-obstruction/RESULT.json b/research/r437-unpooled-budget-obstruction/RESULT.json new file mode 100644 index 0000000000..67a0c6230f --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/RESULT.json @@ -0,0 +1,192 @@ +{ + "admitted_saving": "17/5000", + "bridge_limit": "Historical transfer is stated at c=1/576 with c<1/512; dropping that range is only an optimistic moment relaxation, not an extension of its physical theorem", + "excluded_retained_moment_contraction_budget": true, + "failure_controls": [ + { + "interpretation": "Changed invoice; original exclusion must not be transferred. This is not a candidate admission.", + "name": "dropped_rank_two_bin", + "reason": "fixed unpooled paid profile", + "recomputed_changed_model_lower": "1880792081203895039/3373834007980800000", + "rejected": true + }, + { + "interpretation": "Changed invoice; original exclusion must not be transferred. This is not a candidate admission.", + "name": "moved_rank_42_bin_to_rank_one", + "reason": "fixed unpooled paid profile", + "recomputed_changed_model_lower": "694500314354399159/700229699769600000", + "rejected": true + }, + { + "name": "physical_width_as_productive_width", + "reason": "fixed productive normalization", + "rejected": true + }, + { + "interpretation": "This lower bound is inconclusive at the wrong slot; it is not an actual-moment pass.", + "name": "whole_kappa_as_target", + "reason": "target role must be admitted BIT saving", + "recomputed_wrong_slot_lower": "2523490598475003040318691/2523627837969638400000000", + "rejected": true + }, + { + "name": "changed_source_bytes", + "reason": "raw source authentication: HOST-RESULT.json", + "rejected": true + }, + { + "name": "boolean_integer_receipt_alias", + "reason": "canonical typed receipt mismatch", + "rejected": true + } + ], + "linear_lower_bound": { + "A": "18837/18944", + "B": "227656981418642299/126181391898481920", + "L": "37130213109568854799/37112174087788800000", + "L_minus_one": "18039021780054799/37112174087788800000", + "formula": "L(c)=A+c*B <= M0(c)", + "target": "17/5000", + "terms": [ + { + "count": 380448, + "linear_term": "648231873/3078400000", + "log_lower": "126/65", + "rank": 1, + "rank_weight": "3963/18944" + }, + { + "count": 400288, + "linear_term": "1038584743/2344320000", + "log_lower": "62/33", + "rank": 2, + "rank_weight": "12509/28416" + }, + { + "count": 22464, + "linear_term": "59156487/1586560000", + "log_lower": "122/67", + "rank": 3, + "rank_weight": "351/9472" + }, + { + "count": 26592, + "linear_term": "139331/2368000", + "log_lower": "30/17", + "rank": 4, + "rank_weight": "277/4736" + }, + { + "count": 29376, + "linear_term": "8848653/108928000", + "log_lower": "118/69", + "rank": 5, + "rank_weight": "765/9472" + }, + { + "count": 17376, + "linear_term": "47780199/828800000", + "log_lower": "58/35", + "rank": 6, + "rank_weight": "543/9472" + }, + { + "count": 26496, + "linear_term": "86200527/840640000", + "log_lower": "114/71", + "rank": 7, + "rank_weight": "483/4736" + }, + { + "count": 32, + "linear_term": "1466699/3196800000", + "log_lower": "38/45", + "rank": 26, + "rank_weight": "13/28416" + }, + { + "count": 384, + "linear_term": "2786427/313760000", + "log_lower": "22/53", + "rank": 42, + "rank_weight": "21/2368" + } + ] + }, + "model": { + "checked_sites": [ + "factor=Q(n*r,64*28416)", + "log_bounds(64,r)", + "exp_bounds(c*l,c*h)", + "nonnegative rank-one surcharge" + ], + "dimension": 64, + "price_ast_sha256": "bacd021ed1168eb645fe8293ed09c1f84935940388d00a75e571a2219fca8b50", + "productive_width": 28416, + "scope": "Static model-site binding; no predecessor implementation execution" + }, + "optimistic_moment": "M0(c)=sum_r n_r*r/(64*28416)*exp(c*log(64/r))", + "ordinary_saving": "8590884599/2500000000000", + "paid_children": 903456, + "positive_control_zero_saving": { + "L_at_zero": "18837/18944", + "strictly_below_one": true + }, + "profile": { + "1": 380448, + "2": 400288, + "26": 32, + "3": 22464, + "4": 26592, + "42": 384, + "5": 29376, + "6": 17376, + "7": 26496 + }, + "proof": [ + "For 1<=r<=64, log(64/r)>=2*(64-r)/(64+r).", + "For nonnegative u, exp(u)>=1+u; summing positive rank weights gives L(c)<=M0(c).", + "B>0, so every relaxed c>=admitted target has L(c)>=L(target)>1.", + "The declared bridge a=c*(1-c)<=c makes c>=a>=admitted a necessary condition.", + "All omitted bad-event or added costs are nonnegative under this fixed model." + ], + "rank_mass": 1808352, + "relaxation": "All nonnegative extra charges omitted optimistically; not asserted zero in the real caller", + "remaining": "Different pooled invoice, changed receiver/model, physical compiler/native/stock/precision admission and all-R437 exclusion are outside scope; selected frontier unchanged", + "schema": "r437-unpooled-budget-obstruction/1", + "scope": "Only the frozen unpooled invoice and declared moment-certification budget requiring M<=1; not a runtime lower bound or exclusion of other analyses", + "selected_whole_kappa_provenance_only": "62009/20000000", + "sources": [ + { + "bytes": 3594, + "git_blob": "ee0952e10f744cf1c6d9c237006ccae4ce3c36c8", + "path": "source/HOST-RESULT.json", + "sha256": "000837b2b7a1e9d7e4b6b657a055c6f5f3886c7ea343239f8620f79d5d7b2ae8" + }, + { + "bytes": 10905, + "git_blob": "2cb9b22890fdfacea4ee51a75b7746dd35b78489", + "path": "source/host.py", + "sha256": "df01e61dc31a1cb6b2bf3549be1e2241f7a30829c2c98567f462271e3fc216ee" + }, + { + "bytes": 9424, + "git_blob": "092408728aa81e5a1e6d63307a3c0b85174e2ff2", + "path": "source/ORDINARY-TRANSFER-PROOF.md", + "sha256": "29ed43abaf5451a8514dff2233ba02f44c1d3839e72035ec5711d4edf060b8f9" + }, + { + "bytes": 6419, + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "path": "source/SELECTED-RECORD.json", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "bytes": 1460, + "git_blob": "3a8673160d129f0bec6aacf3ff2c2cf693839221", + "path": "source/SELECTED-CLAIM.json", + "sha256": "66fbb5b21f32f1c4ba544c20d5a44ebcdfd11bce2bfa2d609c656ae520d3b21e" + } + ], + "target_role": "weaker admitted BIT saving; ordinary saving is larger" +} diff --git a/research/r437-unpooled-budget-obstruction/SOURCES.json b/research/r437-unpooled-budget-obstruction/SOURCES.json new file mode 100644 index 0000000000..9df6952ec5 --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/SOURCES.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "research/r437-two-window-carrier/HOST-RESULT.json", + "usage": "provenance", + "git_blob": "ee0952e10f744cf1c6d9c237006ccae4ce3c36c8", + "sha256": "000837b2b7a1e9d7e4b6b657a055c6f5f3886c7ea343239f8620f79d5d7b2ae8" + }, + { + "path": "research/r437-two-window-carrier/host.py", + "usage": "provenance", + "git_blob": "2cb9b22890fdfacea4ee51a75b7746dd35b78489", + "sha256": "df01e61dc31a1cb6b2bf3549be1e2241f7a30829c2c98567f462271e3fc216ee" + }, + { + "path": "research/r437-ordinary-t360/PROOF.md", + "usage": "provenance", + "git_blob": "092408728aa81e5a1e6d63307a3c0b85174e2ff2", + "sha256": "29ed43abaf5451a8514dff2233ba02f44c1d3839e72035ec5711d4edf060b8f9" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "certificates/frontier5599/CLAIM.json", + "usage": "provenance", + "git_blob": "3a8673160d129f0bec6aacf3ff2c2cf693839221", + "sha256": "66fbb5b21f32f1c4ba544c20d5a44ebcdfd11bce2bfa2d609c656ae520d3b21e" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ], + "vendored_inputs": [ + { + "path": "source/HOST-RESULT.json", + "source_path": "research/r437-two-window-carrier/HOST-RESULT.json", + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "repository": "CrocSwap/integer-mult-bounds", + "git_blob": "ee0952e10f744cf1c6d9c237006ccae4ce3c36c8", + "sha256": "000837b2b7a1e9d7e4b6b657a055c6f5f3886c7ea343239f8620f79d5d7b2ae8", + "bytes": 3594, + "usage": "Frozen exact main bytes; source data only, no predecessor implementation execution." + }, + { + "path": "source/host.py", + "source_path": "research/r437-two-window-carrier/host.py", + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "repository": "CrocSwap/integer-mult-bounds", + "git_blob": "2cb9b22890fdfacea4ee51a75b7746dd35b78489", + "sha256": "df01e61dc31a1cb6b2bf3549be1e2241f7a30829c2c98567f462271e3fc216ee", + "bytes": 10905, + "usage": "Frozen exact main bytes; source data only, no predecessor implementation execution." + }, + { + "path": "source/ORDINARY-TRANSFER-PROOF.md", + "source_path": "research/r437-ordinary-t360/PROOF.md", + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "repository": "CrocSwap/integer-mult-bounds", + "git_blob": "092408728aa81e5a1e6d63307a3c0b85174e2ff2", + "sha256": "29ed43abaf5451a8514dff2233ba02f44c1d3839e72035ec5711d4edf060b8f9", + "bytes": 9424, + "usage": "Frozen exact main bytes; source data only, no predecessor implementation execution." + }, + { + "path": "source/SELECTED-RECORD.json", + "source_path": "certificates/selected-result.json", + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "repository": "CrocSwap/integer-mult-bounds", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "bytes": 6419, + "usage": "Frozen exact main bytes; source data only, no predecessor implementation execution." + }, + { + "path": "source/SELECTED-CLAIM.json", + "source_path": "certificates/frontier5599/CLAIM.json", + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "repository": "CrocSwap/integer-mult-bounds", + "git_blob": "3a8673160d129f0bec6aacf3ff2c2cf693839221", + "sha256": "66fbb5b21f32f1c4ba544c20d5a44ebcdfd11bce2bfa2d609c656ae520d3b21e", + "bytes": 1460, + "usage": "Frozen exact main bytes; source data only, no predecessor implementation execution." + } + ], + "source_binding_scope": "Complete main byte provenance for the fixed unpooled host and price definition, historical transfer text and current selected metadata. Not a source-word/pooled/native/physical replay." +} diff --git a/research/r437-unpooled-budget-obstruction/TASK.json b/research/r437-unpooled-budget-obstruction/TASK.json new file mode 100644 index 0000000000..740092ac9a --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "r437-carrier-integration", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "r437-carrier-integration", + "question": "Can the paid R437 two-window carrier improvement be admitted by the actual pooled compiler and physical caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/r437-two-window-carrier/README.md", + "research/r437-reverse-row-coefficient/README.md" + ], + "methods": [ + "Close one compiler/request, caller or precision/stock implication for the pinned paid exchange.", + "Falsify that exact interface with an arbitrary-dirty-state or chronology counterexample." + ], + "acceptance_gate": "Pin the complete source and destination contracts, exact paid and scalar deltas, and all remaining assumptions. A local moment gain is not a physical or all-size supplier admission.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Choose one unclaimed obligation: pooled compiler codebook/request alignment, actual physical caller, or precision/stock envelope using the already reported reverse coefficient. Pin the input and receiver, preserve dirty/source windows, and test one binding with a rejection control. Stop at unresolved dependencies; do not rederive the coefficient or quote the local moment as a completed bound.", + "bottleneck_link": "The exchange changes the paid profile; integration must establish that its gain survives the complete caller.", + "allowed_variations": [ + "One compiler rebind, one actual caller boundary, or one precision/stock implication." + ], + "scope_change_triggers": [ + "Ignoring added ADDs, retaining an obsolete reverse coefficient, or declaring global admission from the local histogram." + ], + "overlap_terms": [ + "R437", + "two-window carrier", + "4067", + "4147", + "pooled compiler", + "request alignment", + "reverse row coefficient" + ], + "existing_checks": [ + { + "scope": "PR #4067: source-bound two-window carrier with (2,2) to (1,3) paid exchange and fixed OQ4 host.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Pooled compiler/request rebind, physical caller and precision/stock admission.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4147: reverse row coefficient follow-up.", + "evidence": "research/r437-reverse-row-coefficient/README.md", + "remaining": "Use the exact coefficient in a caller-bound precision/stock proof rather than repeat the arithmetic.", + "status": "author-checked", + "source_commit": "72e7bb797adf82aeb525a399f56ab8adbab8e93c", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact optimistic necessary-moment budget obstruction for the frozen published unpooled OQ4 host at the current admitted BIT target, under a declared retained transfer law.", + "scope_change_reason": "The current priority8 destination budget is distinct from historical c/root and whole-kappa comparisons. Audit that particular implication, preserving the different pooled model and physical integration handoffs.", + "bottleneck_link": "Determines whether the unchanged unpooled invoice can fill the retained current admitted BIT slot before further physical/stock work; no universal R437 exclusion.", + "budget_minutes": 60, + "stop_rule": "Freeze by23:11UTC, preserve15min verification. First exact rational lower-bound test; if it does not exceed1, stop/narrow without a new root search or invented failure.", + "outcome": "negative-result", + "evidence": "Exact L(17/5000)-1=18039021780054799/37112174087788800000>0, matching independent integer gap78505822786798485248. Retained fixed-unpooled moment gate only, not runtime lower bound; six primary controls, independent model/source guards and current-stage distinctions.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance, separate primary/oracle/proof-review contexts.", + "started_at": "2026-10-26T22:26:30.641324+00:00", + "science_cutoff": "2026-10-26T23:11:30.641324+00:00", + "finish_by": "2026-10-26T23:26:30.641324+00:00", + "claim_expires": "2026-10-26T23:45:00Z", + "open_questions": [ + { + "question": "Can a changed pooled caller/invoice with a complete ordinary transfer contract meet a current destination budget?", + "why_it_matters": "The fixed-unpooled necessary test cannot exclude a changed profile, normalization or transfer model.", + "first_step": "Freeze the actual pooled paid/target invoice, including all source allocation/ownership/physical/precision/stock charges, and derive its own necessary budget before optimizing.", + "blocked_by": "The cited pooled allocation is local-only; complete pooled price and physical catalogue binding remain outside this package." + } + ] +} diff --git a/research/r437-unpooled-budget-obstruction/VERIFY.json b/research/r437-unpooled-budget-obstruction/VERIFY.json new file mode 100644 index 0000000000..d715e3482e --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact raw-source/current-target/model-site binding and rational necessary-moment obstruction, six controls, complete canonical typed RESULT receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized full primary replay with explicit guards and typed receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 120, + "checks": "Independent integer common-denominator certificates, target roles and model/source controls; complete typed ORACLE receipt." + } + ] +} diff --git a/research/r437-unpooled-budget-obstruction/oracle.py b/research/r437-unpooled-budget-obstruction/oracle.py new file mode 100644 index 0000000000..5b2a1b77c6 --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/oracle.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +"""Integer common-denominator audit of the fixed unpooled moment screen. + +ToikY with substantial OpenAI Codex assistance in a separate audit context. +The R437 construction, hosting invoice and ordinary-transfer proof retain +their original authorship in NOTICE. No source or primary implementation is +imported or executed. Apache-2.0. +""" +import argparse +from fractions import Fraction +from hashlib import sha1, sha256 +import json +from math import gcd, lcm +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +PINS = { + "HOST-RESULT.json": (3594, + "000837b2b7a1e9d7e4b6b657a055c6f5f3886c7ea343239f8620f79d5d7b2ae8", + "ee0952e10f744cf1c6d9c237006ccae4ce3c36c8"), + "host.py": (10905, + "df01e61dc31a1cb6b2bf3549be1e2241f7a30829c2c98567f462271e3fc216ee", + "2cb9b22890fdfacea4ee51a75b7746dd35b78489"), + "ORDINARY-TRANSFER-PROOF.md": (9424, + "29ed43abaf5451a8514dff2233ba02f44c1d3839e72035ec5711d4edf060b8f9", + "092408728aa81e5a1e6d63307a3c0b85174e2ff2"), + "SELECTED-RECORD.json": (6419, + "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "581f8d87008354eb5b869f7ed9de1317ad837ce8"), + "SELECTED-CLAIM.json": (1460, + "66fbb5b21f32f1c4ba544c20d5a44ebcdfd11bce2bfa2d609c656ae520d3b21e", + "3a8673160d129f0bec6aacf3ff2c2cf693839221"), +} +PROFILE = {1: 380448, 2: 400288, 3: 22464, 4: 26592, 5: 29376, + 6: 17376, 7: 26496, 26: 32, 42: 384} +WIDTH, NORMALIZATION = 64, 28416 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), + allow_nan=False).encode() + + +def authenticate(name, raw): + size, digest, blob = PINS[name] + need(len(raw) == size and sha256(raw).hexdigest() == digest, + "Oracle exact source bytes: " + name) + need(sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() == blob, + "Oracle exact source Git blob: " + name) + + +def rational(numerator, denominator): + need(type(numerator) is int and type(denominator) is int and denominator > 0, + "Oracle integer rational components") + common = gcd(abs(numerator), denominator) + numerator, denominator = numerator // common, denominator // common + return str(numerator) if denominator == 1 else str(numerator) + "/" + str(denominator) + + +def fixed_model(profile, width, normalization): + need(type(width) is int and type(normalization) is int + and width == WIDTH and normalization == NORMALIZATION, + "Oracle frozen width and normalization") + need(all(type(r) is int and type(n) is int for r, n in profile.items()) + and canonical(profile) == canonical(PROFILE), "Oracle frozen unpooled profile") + + +def target_role(role): + need(role in ("admitted_BIT", "ordinary_BIT"), + "Oracle selected whole kappa is provenance, not a supplier target") + + +def lower_certificate(profile, c_numerator, c_denominator, + width=WIDTH, normalization=NORMALIZATION): + """Compute L=A+cB solely with integer sums and one common denominator.""" + need(type(c_numerator) is int and type(c_denominator) is int + and c_numerator >= 0 and c_denominator > 0, "Oracle nonnegative saving") + need(type(width) is int and width > 0 and type(normalization) is int + and normalization > 0, "Oracle positive normalization") + need(profile and all(type(r) is int and type(n) is int + and 0 < r <= width and n > 0 for r, n in profile.items()), + "Oracle positive paid profile within width") + common = lcm(*(width + r for r in profile)) + mass = sum(r * n for r, n in profile.items()) + # B has denominator width*W*common. No logarithm, exponential, root, + # floating arithmetic or predecessor interval routine occurs here. + slope_numerator = sum(n * r * 2 * (width - r) * (common // (width + r)) + for r, n in profile.items()) + base = width * normalization + numerator = mass * c_denominator * common + c_numerator * slope_numerator + denominator = c_denominator * base * common + return { + "saving": rational(c_numerator, c_denominator), + "mass": mass, "base_denominator": base, "common_log_denominator": common, + "slope_numerator": slope_numerator, + "A": rational(mass, base), "B": rational(slope_numerator, base * common), + "lower": rational(numerator, denominator), + "lower_minus_one": rational(numerator - denominator, denominator), + "integer_lower_numerator": numerator, + "integer_lower_denominator": denominator, + "integer_cross_product_gap": numerator - denominator, + } + + +def reject(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError("Oracle invalid model accepted") + + +def run(): + raw_sources = {} + for name in PINS: + raw = (HERE / "source" / name).read_bytes() + authenticate(name, raw) + raw_sources[name] = raw + host = json.loads(raw_sources["HOST-RESULT.json"]) + selected = json.loads(raw_sources["SELECTED-RECORD.json"]) + claim = json.loads(raw_sources["SELECTED-CLAIM.json"]) + code = raw_sources["host.py"].decode() + transfer = raw_sources["ORDINARY-TRANSFER-PROOF.md"].decode() + need("factor=Q(n*r,64*28416)" in code + and "pp[1]=pp.get(1,0)+Q(32*64*64*E,10**16)" in code, + "Oracle source price normalization and omitted positive fee") + need("a=c(1-c)=575/331776" in transfer and "c<1/512" in transfer, + "Oracle actual historical transfer and its stated domain") + profile = {int(r): n for r, n in host["profiles"]["new"].items()} + fixed_model(profile, WIDTH, NORMALIZATION) + need(host["mass_new"] == sum(r * n for r, n in profile.items()) == 1808352, + "Oracle source hosted mass") + need(host["new"]["forward"]["profile"] == host["new"]["reverse"]["profile"], + "Oracle equal source forward/reverse rank invoices") + admitted = Fraction(claim["admitted_BIT_saving"]) + ordinary = Fraction(claim["ordinary_BIT_saving"]) + kappa = Fraction(selected["kappa"]) + need(admitted == Fraction(17, 5000) + and ordinary == Fraction(8590884599, 2500000000000) + and Fraction(claim["kappa"]) == kappa == Fraction(62009, 20000000) + and ordinary > admitted > kappa > 0, + "Oracle distinct selected budget stages") + results = {} + for role, target in (("admitted_BIT", admitted), ("ordinary_BIT", ordinary)): + target_role(role) + value = lower_certificate(profile, target.numerator, target.denominator) + need(value["slope_numerator"] > 0 and value["integer_cross_product_gap"] > 0, + "Oracle positive necessary-moment obstruction") + results[role] = value + zero = lower_certificate(profile, 0, 1) + need(zero["integer_cross_product_gap"] < 0, "Oracle zero-saving lower bound below one") + changed = dict(profile) + moved = changed.pop(42) + changed[1] += moved + need(sum(changed.values()) == sum(profile.values()), + "Oracle changed-profile control retains total paid calls") + changed_bound = lower_certificate(changed, admitted.numerator, admitted.denominator) + need(changed_bound["integer_cross_product_gap"] < 0, + "Oracle different fixed profile changes this lower-bound sign") + guards = { + "different_profile": reject(lambda: fixed_model(changed, WIDTH, NORMALIZATION)), + "different_normalization": reject(lambda: fixed_model(profile, WIDTH, 28425)), + "negative_saving": reject(lambda: lower_certificate(profile, -1, 5000)), + "whole_kappa_as_supplier_target": reject(lambda: target_role("whole_kappa")), + "changed_source_byte": reject(lambda: authenticate("HOST-RESULT.json", + b"X" + raw_sources["HOST-RESULT.json"][1:])), + } + need(canonical({"bound": 1}) != canonical({"bound": True}) + and canonical({"bound": 1}) != canonical({"bound": 1.0}), + "Oracle receipt equality preserves numeric types") + return { + "status": "PASS_R437_UNPOOLED_BUDGET_ORACLE", + "source_sha256": {name: pin[1] for name, pin in PINS.items()}, + "width": WIDTH, "normalization": NORMALIZATION, + "profile": {str(r): n for r, n in sorted(profile.items())}, + "selected_stages": {"ordinary_BIT": str(ordinary), "admitted_BIT": str(admitted), + "whole_kappa_provenance_only": str(kappa)}, + "integer_certificates": results, + "inequalities": [ + "For x>=1, ln(x)>=2(x-1)/(x+1): the derivative gap is " + "(x-1)^2/[x(x+1)^2]>=0, and the gap vanishes at1.", + "For c>=0 and y=c*ln(x), exp(y)>=1+y; each paid weight is positive.", + "Therefore M0(c)>=L(c)=A+cB. B>0, so L(17/5000)>1 obstructs " + "every c>=17/5000 in this retained moment-certification budget.", + "Under the declared necessary ordinary bridge a<=c, reaching a>=17/5000 " + "would require such a rejected c. No physical bridge is extrapolated.", + ], + "controls": { + "zero_saving": zero, + "changed_profile_rank42_to_rank1": { + "moved_paid_jobs": moved, "total_paid_calls_unchanged": True, + "bound": changed_bound, + "meaning": "Synthetic different-profile sign control only. L<1 is " + "not a proof that its actual moment passes or that the " + "changed jobs have a physical realization.", + }, + "rejections": guards, + }, + "scope": "Fixed unpooled invoice and retained moment-certification/contraction " + "budget only; no runtime complexity lower bound or algorithmic " + "impossibility. All omitted nonnegative charges are optimistic " + "omissions, not real zero costs. The source ordinary proof fixes " + "c=1/576 within c<1/512; it does not establish physical extension to " + "17/5000. Changed pooled invoices, native action, source words, " + "compiler and full physical/stock implementation remain outside.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", + help="Print a candidate receipt without writing files") + args = parser.parse_args() + result = run() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True, allow_nan=False)) + else: + retained = json.loads((HERE / "ORACLE.json").read_bytes()) + need(canonical(retained) == canonical(result), "Oracle complete typed receipt") + print(json.dumps({"status": result["status"], + "admitted_lower": result["integer_certificates"] + ["admitted_BIT"]["lower"]}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/r437-unpooled-budget-obstruction/source/HOST-RESULT.json b/research/r437-unpooled-budget-obstruction/source/HOST-RESULT.json new file mode 100644 index 0000000000..ee0952e10f --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/source/HOST-RESULT.json @@ -0,0 +1,122 @@ +{ + "calls": 288, + "emitted_sha256": { + "new": "ed64cb293ce6051f60b73866254d4222f6121dc5465b0bb9b579e01d49a41906", + "old": "a777373994bd84681d6c2be75251ba6a04a1521580910f23afe09bb50db632b2" + }, + "events": { + "new": 7814880, + "old": 7814016 + }, + "helpers_per_call": 437, + "hosted_owner_occurrences": 125856, + "mass_new": 1808352, + "mass_old": 1808352, + "new": { + "forward": { + "adds": 24211, + "l1": 49347, + "profile": { + "1": 1321, + "2": 1342, + "3": 78, + "4": 43, + "5": 102, + "6": 11, + "7": 18 + }, + "records": 27135, + "records_sha256": "ad073729b66389fc82657bc534d4ae34b5a0e389871de71ae76603ec555f10fc", + "stream_sha256": "a5b9624f2ea6d2d00b707ab744f772d361c62dea212f07e42844ac948a06e516" + }, + "reverse": { + "adds": 24211, + "l1": 1123650, + "profile": { + "1": 1321, + "2": 1342, + "3": 78, + "4": 43, + "5": 102, + "6": 11, + "7": 18 + }, + "records": 27135, + "records_sha256": "ad073729b66389fc82657bc534d4ae34b5a0e389871de71ae76603ec555f10fc", + "stream_sha256": "73cddd64a3e861de6f29402d8c4f6bc871562999c66fd0197c0b2ee50271c185" + } + }, + "old": { + "forward": { + "adds": 24208, + "l1": 49347, + "profile": { + "1": 1320, + "2": 1344, + "3": 77, + "4": 43, + "5": 102, + "6": 11, + "7": 18 + }, + "records": 27132, + "records_sha256": "caeb2eb0e417992788c32c1f5812ada60b46d1dfdba9f4ac376299b2dede13cb", + "stream_sha256": "388e1d467c2d66408342328d671a578d3ab7fa7b2e6a3b2d5b5c16ba919debcf" + }, + "reverse": { + "adds": 24208, + "l1": 1113998, + "profile": { + "1": 1320, + "2": 1344, + "3": 77, + "4": 43, + "5": 102, + "6": 11, + "7": 18 + }, + "records": 27132, + "records_sha256": "caeb2eb0e417992788c32c1f5812ada60b46d1dfdba9f4ac376299b2dede13cb", + "stream_sha256": "386bf053e635b90f313e81d3ba02c305f8d83b0125ee612553314aefe901e650" + } + }, + "price_probe": { + "below_one": true, + "c": "1736690352456612377607/1000000000000000000000000", + "decimal": "0.0017366903524566124", + "lower": "124999999999999999999999758599016557078956933024341385519179/125000000000000000000000000000000000000000000000000000000000", + "next_c": "217086294057076547201/125000000000000000000000", + "next_lower": "1000000000000000000000001330719821031754567716547467156203341/1000000000000000000000000000000000000000000000000000000000000", + "next_upper": "62500000000000000000000083169988814484660482284217302212173/62500000000000000000000000000000000000000000000000000000000", + "old_c": "1736646042038446578551/1000000000000000000000000", + "relative_gain": "44310418165799056/1736646042038446578551", + "upper": "999999999999999999999998068792132456631655464194740763344859/1000000000000000000000000000000000000000000000000000000000000" + }, + "profiles": { + "new": { + "1": 380448, + "2": 400288, + "3": 22464, + "4": 26592, + "5": 29376, + "6": 17376, + "7": 26496, + "26": 32, + "42": 384 + }, + "old": { + "1": 380160, + "2": 400864, + "3": 22176, + "4": 26592, + "5": 29376, + "6": 17376, + "7": 26496, + "26": 32, + "42": 384 + } + }, + "replicas": 32, + "scope": "fixed unpooled OQ4 owner/idle schedule and primitive rank invoice; source/native compiler and complete physical/stock invoice remain conditional", + "status": "PASS_FIXED_OQ4_HOST_REBUILD" +} diff --git a/research/r437-unpooled-budget-obstruction/source/ORDINARY-TRANSFER-PROOF.md b/research/r437-unpooled-budget-obstruction/source/ORDINARY-TRANSFER-PROOF.md new file mode 100644 index 0000000000..092408728a --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/source/ORDINARY-TRANSFER-PROOF.md @@ -0,0 +1,165 @@ +# R437 ordinary recurrence and fixed T360 transfer + +This is a source-relative conditional implication and finite adapter audit. +It does not admit a new complete physical supplier or multiplication exponent. +Sources and original notices are retained under `sources/`; `SOURCES.json` +pins every retained byte. New analysis/code used substantial OpenAI Codex +assistance at human direction. Apache-2.0. + +## Complete recurrence and finite majorants + +Use the actual R437 histogram in `certificate.py`, dimension 64, W=28416, +epsilon=10^-16, and F=32*64^2*903456=118417784832. For f=floor(n/64), +retain the complete predecessor recurrence + + T(n,w) <= sum_r H_r/W T(r f,w) + + epsilon F/W max_(1<=j<=f) T(j,w) + C(n+w), + T(n,w) <= Cw for 01, 10^6(1-mu_(575/576))>1. + +Thus strong induction against a monotone majorant (not monotonicity of actual +runtime) gives T(n,w)<=200Cn+10^6 C n^(575/576)w. The base is immediate. +Floors only decrease the proposed child bound; the bad-class maximum is bounded +by that same majorant at f. The two strict inequalities pay Cn and Cw. +For the complete old C0 histogram the corresponding moment is strictly above +1.0000087717216952679207496066. This new passing result is not old1/576. + +## History, stock, fit and both returns + +Set w=ceil(e^(1/576)), a=c(1-c)=575/331776. Since +17/10000=0:q^j>=stock}, n=floor((e-k)/w), ell=e-k-nw. + +Indeed lcm(28416,28425)=269241600 and R437 preserves both counts, dimension, +maximum child 42 and halving depth 2. New rank34 lies within the old maximum. +A changed caller must use this complete original-width stock, not a local +request count. The inherited estimate k<=8195w log2(e)<=16390 e^c log2(e) +holds under the same cover/stock hypotheses. At e>=2^20, the decreasing +function e^(c-1)log2(e), 2^(20c)<17/16, and +32780*(17/16)*20=696575<2^20 imply 2ke^(1-c)/4-1>64. Both actual selector fit predicates eventually succeed. +No finite prefix is used to set online precision. + +Each of the two C0 calls pads genuine q^k rows to a compatible multiple of +stock by a volume factor strictly below two and restricts its own return. +Including both calls and the complete added CV(n+k+w+1) bill gives + + T_B(e)/V <= C[801n+4*10^6 n^(1-c)w+k+w+1] + <= 4283584 C e^(1-a). + +Here n<=e^(1-c), n^(1-c)w<=2^c e^(1-a)<(17/16)e^(1-a), +k<=32780e^(1-a), w<=2e^(1-a), and 1<=e^(1-a). For e<2^20, +e^a<2; elementary fallback is absorbed. The unchanged fixed-tape setup and +(1+log2 V)^4<=512V are included in C. Binary padding retains its q-dependent +constant. Therefore a conditional ordinary improvement of about 2.67813e-6 +over the refreshed public complex release coefficient is available **if the +changed C0 physical refinement/cost contract is completed**. + +## What the actual source adapter establishes + +PR3562's authenticated PR2899 export loads PR2753's exact old Catalogue and +SelectedTopology. Those enforce 661 roles, 904896 requests and an ordered +request digest. They cannot be replaced by a histogram at runtime. +`adapter.py` creates separate modules from those authenticated bytes using +exact-counted substitutions. It changes role/private width to659, selects the +actual R437 word/template/geometry, and binds the new full histogram and ordered +digest 0fb70d6838583f2f439a8704eb5dba84ce9dbd231d91f140da13440b680d73aa. +No original source or shared module is overwritten. The old geometry, +636 rational frame projectors, source charts, rank decomposition, owner routes, +COPY/discard rules and coefficient compiler are reused explicitly. + +All 7,814,016 actual literal local-call events pass the finite LocalState +chronology/frame/version/borrow guards in both orientations, across288 calls. +The new catalogue has 28233 canonical requests, including26154 MOVE,81 COPY, +1998 IDLE, multiplied by32 replicas. It has540 base and1235 chart labels. +Every residual suffix and complete invoice was separately replayed by the +pinned R437 source verifier. That fresh13-command cold replay checks659 RAW +columns, arbitrary SOURCE/helper DIRTY, H1-H5, exact rational transport, +SOURCE boundaries,9 capture/COPY windows, owners and all fallback charges. +It is executed author-verifier evidence, not independent supplier admission. + +The new rank34 IDLE at identifier27776 is consumed by the retained actual +SelectedBinding coefficient/callback engine: a parent width256 produces +child136, then restores the serialized parent on a controlled23-bit return. +Wrong parent, foreign program and wrong source controls reject before commit. +The callback gives coefficients0,2; unused stock11 is a declared reduced +fixture. It is not a full GL64 payload or full physical ordinary invocation. +The GL2 physical wrapper separately passes actual Profile(1,576), both384-column +returns, borrowed input, provenance, cleanup, reuse and binary exchange. These +two experiments are deliberately not reported as one complete cohort. + +The **first unresolved obligation** is a single production ordinary/native/ +router cohort whose authenticated compiled program and physical source binding +actually use this R437 catalogue. No complete GL64 code tuple is emitted or run. +Its uniform refinement, history/preparation/ROW and cost implication must be +checked at the changed program, rather than inferred from these finite tests. +The R437 finite ROW18355<20161, prefix177/paid192 and twolevel393/paid512 are +finite evidence; they are not uniform all-width precision theorems. + +## Joint retimed T360, both outer terms and stopping decision + +The exact PR3682 head's retained STRICT-RESULT, RESULT and PREFIX-AND-INVOICE +bind the same actual complete profile +{1:7980120,2:2345760,3:755730,4:330480,5:69930,8:25920,48:137790}, +W=322560, physical323069, calls3240 and roles1321920. Our certificate compares +these source bytes and fields; it does not rerun the expensive T360 admission. +The joint use of this complex profile and R437 remains prospective. + +For sigma=.9982695812, eta=10^-6, tau=1-a=331201/331776, +alpha=.998269582931, the full T360 normalized moment is below +.9999999997170261251179281427 and tau=2:a/=2;k+=1 + def series(z): + total=Q(0);term=z + for j in range(48):total+=2*term/(2*j+1);term*=z*z + return total,total+2*term/(97*(1-z*z)) + lo,hi=series((a-1)/(a+1));l2,h2=series(Q(1,3));lo+=k*l2;hi+=k*h2;scale=10**64 + return Q(lo.numerator*scale//lo.denominator,scale),Q(-((-hi.numerator*scale)//hi.denominator),scale) +def exp_bounds(lo,hi): + def series(x): + total=term=Q(1) + for j in range(1,23):term=term*x/j;total+=term + return total,total+(term*x/23)/(1-x/24) + return series(lo)[0],series(hi)[1] +def price(profile,c): + pp=dict(profile);E=sum(pp.values());pp[1]=pp.get(1,0)+Q(32*64*64*E,10**16) + low=high=Q(0) + for r,n in pp.items(): + l,h=log_bounds(64,r);a,b=exp_bounds(c*l,c*h);factor=Q(n*r,64*28416) + low+=factor*a;high+=factor*b + scale=10**60 + return Q(low.numerator*scale//low.denominator,scale),Q(-((-high.numerator*scale)//high.denominator),scale) +def run(): + old=v.load();new=json.loads((P/'CANDIDATE.json').read_text());dims=v.geometry(old) + baseline,bd=streams(old,dims);candidate,cd=streams(new,dims) + t=json.loads(gzip.decompress((P/'inputs/OQ4-TEMPLATE.json.gz').read_bytes())) + expected=json.loads((P/'inputs/OQ4-EXPECTED.json').read_text()) + v.need(t['local_programs']==baseline,'literal old local streams bind retained OQ4 template') + windows={};last={};local=[] + for pos,e in enumerate(t['schedule']): + if e['kind']=='local_cover_sweep':local.append((pos,e['stage'],e['pair']));last[e['pair']]=pos + elif e['kind']=='bridge':last[e['dst']]=pos;last[e['src']]=pos + elif e['kind']=='idle':windows[e['idx']]=(e['pair'],e['rank'],{s for p,s,pair in local if last.get(e['pair'],-1)=0 and off+8<=r and 0<=helper<437 and 0<=cp<222,'hosted lifetime and width') + bits=((1<<8)-1)<old_c,'retained old charged grid and positive gain') + return {'status':'PASS_FIXED_OQ4_HOST_REBUILD','calls':288,'replicas':32,'helpers_per_call':437,'hosted_owner_occurrences':288*437, + 'old':bd,'new':cd,'profiles':profiles,'emitted_sha256':digests,'events':events, + 'mass_old':sum(r*n for r,n in profiles['old'].items()),'mass_new':sum(r*n for r,n in profiles['new'].items()), + 'price_probe':{'c':str(c),'decimal':str(float(c)),'lower':str(lo),'upper':str(hi),'next_c':str(c+Q(1,10**24)),'next_lower':str(next_lo),'next_upper':str(next_hi),'old_c':str(old_c),'relative_gain':str((c-old_c)/old_c),'below_one':hi<1}, + 'scope':'fixed unpooled OQ4 owner/idle schedule and primitive rank invoice; source/native compiler and complete physical/stock invoice remain conditional'} +if __name__=='__main__': + import argparse + ap=argparse.ArgumentParser();ap.add_argument('--write');args=ap.parse_args();result=run() + if args.write:Path(args.write).write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else:v.need(json.loads(json.dumps(result))==json.loads((P/'HOST-RESULT.json').read_text()),'host receipt') + print(result['status'], 'calls=288 owners=125856 mass='+str(result['mass_new']), 'price_probe_below_one='+str(result['price_probe']['below_one'])) diff --git a/research/r437-unpooled-budget-obstruction/verify.py b/research/r437-unpooled-budget-obstruction/verify.py new file mode 100644 index 0000000000..9b7623f5c6 --- /dev/null +++ b/research/r437-unpooled-budget-obstruction/verify.py @@ -0,0 +1,222 @@ +#!/usr/bin/env python3 +"""Exact favorable-budget obstruction for one frozen unpooled R437 invoice. + +ToikY with substantial OpenAI Codex assistance. Apache-2.0. +Chris R/Clear1nsight supplied the carrier/host; retained credit is in NOTICE. +No predecessor code is executed and no source word, root or native replay runs. +""" +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha1, sha256 +from pathlib import Path +import argparse +import ast +import json + + +HERE = Path(__file__).resolve().parent +PINS = { + "HOST-RESULT.json": ("000837b2b7a1e9d7e4b6b657a055c6f5f3886c7ea343239f8620f79d5d7b2ae8", + "ee0952e10f744cf1c6d9c237006ccae4ce3c36c8"), + "host.py": ("df01e61dc31a1cb6b2bf3549be1e2241f7a30829c2c98567f462271e3fc216ee", + "2cb9b22890fdfacea4ee51a75b7746dd35b78489"), + "ORDINARY-TRANSFER-PROOF.md": ("29ed43abaf5451a8514dff2233ba02f44c1d3839e72035ec5711d4edf060b8f9", + "092408728aa81e5a1e6d63307a3c0b85174e2ff2"), + "SELECTED-RECORD.json": ("2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "581f8d87008354eb5b869f7ed9de1317ad837ce8"), + "SELECTED-CLAIM.json": ("66fbb5b21f32f1c4ba544c20d5a44ebcdfd11bce2bfa2d609c656ae520d3b21e", + "3a8673160d129f0bec6aacf3ff2c2cf693839221"), +} +PROFILE = {1: 380448, 2: 400288, 3: 22464, 4: 26592, 5: 29376, + 6: 17376, 7: 26496, 26: 32, 42: 384} + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False).encode() + + +def compare_receipt(actual, expected): + need(canonical(actual) == canonical(expected), "canonical typed receipt mismatch") + + +def authenticate(name, raw): + expected_sha, expected_blob = PINS[name] + need(sha256(raw).hexdigest() == expected_sha, "raw source authentication: " + name) + blob = sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + need(blob == expected_blob, "Git blob authentication: " + name) + return {"path": "source/" + name, "bytes": len(raw), + "sha256": expected_sha, "git_blob": blob} + + +def syntax(expression): + return ast.dump(ast.parse(expression, mode="eval").body, include_attributes=False) + + +def model_from_price(source): + """Inspect the authenticated price AST without evaluating any source code.""" + tree = ast.parse(source) + functions = [node for node in tree.body if isinstance(node, ast.FunctionDef) and node.name == "price"] + need(len(functions) == 1, "one retained price definition") + price = functions[0] + need([argument.arg for argument in price.args.args] == ["profile", "c"], "price arguments") + factors = [node.value for node in ast.walk(price) if isinstance(node, ast.Assign) + and any(isinstance(target, ast.Name) and target.id == "factor" for target in node.targets)] + need(len(factors) == 1, "one price normalization factor") + factor = factors[0] + need(isinstance(factor, ast.Call) and isinstance(factor.func, ast.Name) + and factor.func.id == "Q" and len(factor.args) == 2 + and ast.dump(factor.args[0], include_attributes=False) == syntax("n*r"), + "price rank-weight numerator") + denominator = factor.args[1] + need(isinstance(denominator, ast.BinOp) and isinstance(denominator.op, ast.Mult) + and isinstance(denominator.left, ast.Constant) and isinstance(denominator.right, ast.Constant) + and type(denominator.left.value) is type(denominator.right.value) is int, + "price productive normalization") + dimension, width = denominator.left.value, denominator.right.value + calls = [node for node in ast.walk(price) if isinstance(node, ast.Call) + and isinstance(node.func, ast.Name)] + logs = [node for node in calls if node.func.id == "log_bounds"] + exponentials = [node for node in calls if node.func.id == "exp_bounds"] + need(len(logs) == len(exponentials) == 1 and len(logs[0].args) == 2 + and ast.dump(logs[0].args[0], include_attributes=False) == syntax(str(dimension)) + and ast.dump(logs[0].args[1], include_attributes=False) == syntax("r") + and [ast.dump(arg, include_attributes=False) for arg in exponentials[0].args] + == [syntax("c*l"), syntax("c*h")], "price exponential saving convention") + required_surcharge = ast.dump(ast.parse( + "pp[1]=pp.get(1,0)+Q(32*64*64*E,10**16)").body[0], include_attributes=False) + need(any(ast.dump(node, include_attributes=False) == required_surcharge for node in ast.walk(price)), + "nonnegative retained rank-one surcharge") + return dimension, width, { + "dimension": dimension, "productive_width": width, + "price_ast_sha256": sha256(ast.dump(price, include_attributes=False).encode()).hexdigest(), + "checked_sites": ["factor=Q(n*r,64*28416)", "log_bounds(64,r)", + "exp_bounds(c*l,c*h)", "nonnegative rank-one surcharge"], + "scope": "Static model-site binding; no predecessor implementation execution", + } + + +def check_contract(profile, dimension, width): + need(dimension == 64 and width == 28416, "fixed productive normalization") + need(profile == PROFILE, "fixed unpooled paid profile") + need(all(type(rank) is int and 0 < rank < dimension and type(count) is int and count > 0 + for rank, count in profile.items()), "positive proper-rank invoice") + + +def bound(profile, dimension, width, saving): + """L(c)=A+cB <= the optimistic moment; this is not a root enclosure.""" + need(0 <= saving < 1, "saving in relaxed moment range") + base = slope = Q(0) + terms = [] + for rank, count in sorted(profile.items()): + need(type(rank) is int and 0 < rank <= dimension and type(count) is int and count > 0, + "bound positive rank/count") + weight = Q(count * rank, dimension * width) + log_lower = Q(2 * (dimension - rank), dimension + rank) + term = weight * (1 + saving * log_lower) + base += weight + slope += weight * log_lower + terms.append({"rank": rank, "count": count, "rank_weight": str(weight), + "log_lower": str(log_lower), "linear_term": str(term)}) + return base, slope, base + saving * slope, terms + + +def target(claim, role="admitted_BIT_saving"): + need(role == "admitted_BIT_saving", "target role must be admitted BIT saving") + admitted, ordinary = Q(claim[role]), Q(claim["ordinary_BIT_saving"]) + need(admitted == Q(17, 5000) and ordinary == Q(8590884599, 2500000000000) + and 0 < admitted <= ordinary < 1, "current ordinary/admitted target binding") + return admitted, ordinary + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="emit candidate only; never writes files") + args = parser.parse_args() + raw = {name: (HERE / "source" / name).read_bytes() for name in PINS} + authenticated = [authenticate(name, value) for name, value in raw.items()] + host = json.loads(raw["HOST-RESULT.json"]) + selected, claim = (json.loads(raw[name]) for name in ("SELECTED-RECORD.json", "SELECTED-CLAIM.json")) + need(selected["certificate_sha256"] == PINS["SELECTED-CLAIM.json"][0] + and selected["kappa"] == claim["kappa"], "current selected claim provenance") + profile = {int(rank): count for rank, count in host["profiles"]["new"].items()} + dimension, width, model = model_from_price(raw["host.py"]) + check_contract(profile, dimension, width) + need(sum(rank * count for rank, count in profile.items()) == host["mass_new"] == 1808352 + and "fixed unpooled OQ4" in host["scope"], "retained host profile scope") + transfer = raw["ORDINARY-TRANSFER-PROOF.md"].decode() + need("a=c(1-c)=575/331776" in transfer and "17/10000 0 and lower > 1, "first discriminating linear lower bound") + controls = [] + + def reject(name, reason, action, **evidence): + try: + action() + except ValueError as error: + need(str(error) == reason, "control rejected for unintended reason: " + name) + controls.append({"name": name, "reason": str(error), "rejected": True, **evidence}) + else: + raise ValueError("control accepted: " + name) + + dropped = dict(profile) + del dropped[2] + moved = dict(profile) + moved[1] += moved.pop(42) + for name, changed in (("dropped_rank_two_bin", dropped), ("moved_rank_42_bin_to_rank_one", moved)): + changed_lower = bound(changed, dimension, width, admitted)[2] + need(changed_lower < 1, "changed-model control is not discriminating") + reject(name, "fixed unpooled paid profile", lambda changed=changed: check_contract(changed, dimension, width), + recomputed_changed_model_lower=str(changed_lower), + interpretation="Changed invoice; original exclusion must not be transferred. This is not a candidate admission.") + reject("physical_width_as_productive_width", "fixed productive normalization", + lambda: check_contract(profile, dimension, 28425)) + wrong_slot_lower = bound(profile, dimension, width, Q(claim["kappa"]))[2] + need(wrong_slot_lower <= 1, "wrong-slot control must lose this lower-bound exclusion") + reject("whole_kappa_as_target", "target role must be admitted BIT saving", lambda: target(claim, "kappa"), + recomputed_wrong_slot_lower=str(wrong_slot_lower), + interpretation="This lower bound is inconclusive at the wrong slot; it is not an actual-moment pass.") + reject("changed_source_bytes", "raw source authentication: HOST-RESULT.json", + lambda: authenticate("HOST-RESULT.json", raw["HOST-RESULT.json"] + b" ")) + result = { + "schema": "r437-unpooled-budget-obstruction/1", "sources": authenticated, + "model": model, "profile": {str(rank): count for rank, count in sorted(profile.items())}, + "paid_children": sum(profile.values()), "rank_mass": host["mass_new"], + "ordinary_saving": str(ordinary), "admitted_saving": str(admitted), + "target_role": "weaker admitted BIT saving; ordinary saving is larger", + "selected_whole_kappa_provenance_only": claim["kappa"], + "optimistic_moment": "M0(c)=sum_r n_r*r/(64*28416)*exp(c*log(64/r))", + "linear_lower_bound": {"formula": "L(c)=A+c*B <= M0(c)", "A": str(base), "B": str(slope), + "target": str(admitted), "L": str(lower), "L_minus_one": str(lower - 1), + "terms": terms}, + "proof": ["For 1<=r<=64, log(64/r)>=2*(64-r)/(64+r).", + "For nonnegative u, exp(u)>=1+u; summing positive rank weights gives L(c)<=M0(c).", + "B>0, so every relaxed c>=admitted target has L(c)>=L(target)>1.", + "The declared bridge a=c*(1-c)<=c makes c>=a>=admitted a necessary condition.", + "All omitted bad-event or added costs are nonnegative under this fixed model."], + "excluded_retained_moment_contraction_budget": True, + "positive_control_zero_saving": {"L_at_zero": str(base), "strictly_below_one": base < 1}, + "relaxation": "All nonnegative extra charges omitted optimistically; not asserted zero in the real caller", + "scope": "Only the frozen unpooled invoice and declared moment-certification budget requiring M<=1; not a runtime lower bound or exclusion of other analyses", + "bridge_limit": "Historical transfer is stated at c=1/576 with c<1/512; dropping that range is only an optimistic moment relaxation, not an extension of its physical theorem", + "remaining": "Different pooled invoice, changed receiver/model, physical compiler/native/stock/precision admission and all-R437 exclusion are outside scope; selected frontier unchanged", + "failure_controls": controls, + } + alias = deepcopy(result) + alias["excluded_retained_moment_contraction_budget"] = 1 + reject("boolean_integer_receipt_alias", "canonical typed receipt mismatch", + lambda: compare_receipt(result, alias)) + if not args.emit: + compare_receipt(result, json.loads((HERE / "RESULT.json").read_text(encoding="utf-8"))) + print(json.dumps(result, sort_keys=True, indent=2, allow_nan=False)) + print("PASS_R437_UNPOOLED_BUDGET_OBSTRUCTION") + + +if __name__ == "__main__": + main()