diff --git a/research/staged544-terminal-extension-budget/.gitattributes b/research/staged544-terminal-extension-budget/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/staged544-terminal-extension-budget/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/staged544-terminal-extension-budget/.gitignore b/research/staged544-terminal-extension-budget/.gitignore new file mode 100644 index 0000000000..7a60b85e14 --- /dev/null +++ b/research/staged544-terminal-extension-budget/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.pyc diff --git a/research/staged544-terminal-extension-budget/EXTERNAL-SOURCES.json b/research/staged544-terminal-extension-budget/EXTERNAL-SOURCES.json new file mode 100644 index 0000000000..cf24cf8f81 --- /dev/null +++ b/research/staged544-terminal-extension-budget/EXTERNAL-SOURCES.json @@ -0,0 +1,8 @@ +{ + "head": "91f81d131252db704f945891da1ea54e29d46b8b", + "base_url": "https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/91f81d131252db704f945891da1ea54e29d46b8b/research/staged544-terminal-gap-fill/owner/", + "files": { + "FILL.json.gz": "430233230c9194a52bda171afd21713351fdd02e0054230012109e44047c4c55", + "inputs/TEMPLATE.json.gz": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + } +} diff --git a/research/staged544-terminal-extension-budget/FROZEN.json b/research/staged544-terminal-extension-budget/FROZEN.json new file mode 100644 index 0000000000..00466cdc0c --- /dev/null +++ b/research/staged544-terminal-extension-budget/FROZEN.json @@ -0,0 +1,8 @@ +{ + "frozen/audit_core.py": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951", + "frozen/PR3890-PROOF.md": "27a4519a6b75d06f0203c3fc28a60ad95408b726724793e7b8a9774184b6ef9b", + "frozen/PROFILE.json": "64b85c791a331e79ddc18f047b672240c008900b8c004d37cf6d925067373228", + "frozen/WORD-extra.json.gz": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "frozen/WORD-base.json.gz": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "frozen/SOURCE-CREDITS.md": "d4a13d8b8ed9cdb594f00efb3d1a336e09d934423330f02a1514308a720c278b" +} diff --git a/research/staged544-terminal-extension-budget/LEDGER.json b/research/staged544-terminal-extension-budget/LEDGER.json new file mode 100644 index 0000000000..44989fdf4f --- /dev/null +++ b/research/staged544-terminal-extension-budget/LEDGER.json @@ -0,0 +1,37 @@ +{ + "status": "COMPLETE_SCOPED_TARIFF_OBLIGATION_LEDGER", + "no_candidate_emitted": true, + "baseline_local_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "baseline_complete_profile": { + "1": 8041680, + "2": 2306880, + "3": 729648, + "4": 353160, + "5": 69120, + "8": 25920, + "48": 137952 + }, + "local_terminal_surcharge": "proved lower bound D*(9^s-8^s), every intermediate paid frame fixed; binary terminal rank at most9", + "local_interior_cost": "fixed by theorem; any savings from interior refit are outside its class and must exceed0.006843664113335406486182D before repacking could pay", + "owner_idle_credit": "proved upper bound qD from all841 exact dual inequalities; permits any clock-free fractional reassignment", + "baseline_owner_binding": "all1321920 rows/725760 bins regenerated from immutable external files in full mode; exact aggregate proof checked in default mode", + "actual_new_chronology": "no new assignment constructed; relaxation discards chronology and family restrictions, so rejection also covers their constrained subset", + "fixed_identity_capacity": "proved zero nonnegative extension cone using terminal rank plus actual per-bin capacity", + "dirty_state_and_restoration": "no changed circuit claimed. Frozen words preserve predecessor's91 protected buffers and cleanup; PR3969 exact arbitrary-dirty scalar/permutation identity inherited, not independently replayed here", + "native_phase": "inherited/unverified here, not zero; interior/native recipes fixed in theorem", + "scalar_coefficients": "no scalar coefficient changes; finite4-bit source bound inherited, no uniform precision/tape coefficient derived", + "physical_hosting": "finite capacity certificate fresh, universal physical implementation assumptions inherited/unverified", + "uniform_precision_stock_tape_recovery": "unknown/inherited, not zero", + "all_size_compiler": "unknown/inherited, not zero", + "outer_supplier_release": "unrun; fixed claimed3945 endpoint used only as exact tariff parameter, no root/admission recertification", + "analytic_BIT": "inherited/unverified, not zero", + "scope_limit": "This is a complete local-plus-idle tariff rejection under the explicitly fixed comparison model. It is not a lower bound on every possible multiplication algorithm or on unrelated costs. Other shrinking/extension combinations beyond the17direct refunds, and changed internal frames/templates/entrances remain outside.", + "direct_terminal_refunds": "Exactly17 protected width5->4 direct refunds per provider: savedH1 is canceled by a proved+H1 idle lower bound; all2551patterns checked. Mixed direct refunds plus terminal-only extensions still lose the same positive gap." +} diff --git a/research/staged544-terminal-extension-budget/OWNER-PATTERNS.json b/research/staged544-terminal-extension-budget/OWNER-PATTERNS.json new file mode 100644 index 0000000000..858a0225ca --- /dev/null +++ b/research/staged544-terminal-extension-budget/OWNER-PATTERNS.json @@ -0,0 +1,137 @@ +{ + "derivation": "All1321920 literal FILL rows; run --source-root to reconstruct. All unoccupied bins counted.", + "patterns": [ + [ + 8, + [ + 0, + 0, + 0, + 1, + 0 + ], + 0, + 241920 + ], + [ + 16, + [ + 0, + 0, + 0, + 2, + 0 + ], + 0, + 2233 + ], + [ + 16, + [ + 0, + 0, + 1, + 0, + 1 + ], + 0, + 159047 + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 3 + ], + 5, + 4320 + ], + [ + 32, + [ + 0, + 0, + 0, + 4, + 0 + ], + 0, + 224 + ], + [ + 32, + [ + 0, + 0, + 1, + 2, + 1 + ], + 0, + 2719 + ], + [ + 32, + [ + 0, + 0, + 2, + 0, + 2 + ], + 0, + 4977 + ], + [ + 32, + [ + 0, + 1, + 0, + 1, + 2 + ], + 0, + 58320 + ], + [ + 32, + [ + 1, + 0, + 0, + 0, + 3 + ], + 0, + 90720 + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0 + ], + 48, + 137952 + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 5 + ], + 3, + 23328 + ] + ] +} diff --git a/research/staged544-terminal-extension-budget/PROOF.md b/research/staged544-terminal-extension-budget/PROOF.md new file mode 100644 index 0000000000..5c198d90c2 --- /dev/null +++ b/research/staged544-terminal-extension-budget/PROOF.md @@ -0,0 +1,156 @@ +# Terminal-only extension requires a strictly positive interior saving + +Chris R / Clear1nsight, substantial OpenAI Codex assistance. Apache-2.0. + +## Exact contract and claim + +Let k = 1730663236534549309146/10^24, s=1-k, and h(r)=r^s for r>0, +h(0)=0. This is the lower endpoint of the root enclosure claimed in PR3945; +its source moment is sum n_r r(73/r)^k. Comparing sum n_r h(r) is equivalent, +since the common positive factor73^k and the normalizer remain unchanged. +The endpoint is a source pin, not a new root or supplier validation. + +Keep either pinned PR3945 word's helper entrances and every paid interior +scalar/native frame unchanged. Enlarge any chosen terminal subspaces by +nonnegative dimensions. They need not be coordinate extensions, uniform +across calls, or equal between providers. Keep the ambient binary dimension9, +helper identities and the bin inventory at T360. Permit an arbitrary new owner +assignment; for the lower bound, drop all time-window and family restrictions, +and even permit fractional packing. Each helper remains whole in one bin and +each unused remainder is paid as one recursive child. + +If D>0 is the total number of added helper dimensions over all calls, the new +complete local-plus-idle tariff exceeds the incumbent by more than + + 0.006843664113335406486182 D. + +Thus terminal-only enlargement cannot improve the complete tariff even with +unrestricted repacking in this relaxed model. If an actual implementation adds +other costs, they cannot repair this deficit. If interior repricing introduces +savings, it must supply more than this amount to beat the incumbent; this +necessary allowance is not a sufficient construction. Mixed shrink/enlarge +moves and changed helper entrances are outside the theorem. + +## Credited packing dual, newly checked at the changed endpoint + +The dual form is from Erwan Secousses / ChaloupeMusic PR3815, Sagar Thakrar +PR3862 and ToikY PR3890. We do not claim to discover it. PR3890's frozen proof +is retained with its original attribution. Its exponent was the earlier +3815 endpoint; here every inequality is checked afresh at the3945 endpoint. +The new result is the terminal-cost implication and binding to the actual +changed3945 inventory and literal allocation. + +For widths5..9 put + + q=(h(48)-h(3)-5h(5))/20, + pi(w)=-h(5)-(w-5)q, + mu(8)=-pi(8), mu(16)=-2pi(8), mu(32)=-4pi(8), mu(48)=h(48). + +For any capacity c and count vector n of widths5..9, with remainder +l=c-sum w*n_w>=0, the dual condition is + + h(l) - mu(c) - sum pi(w)*n_w >=0. + +The checker enumerates all841 patterns:11 symbolic identities and830 strict +inequalities. Exact rational outward bounds certify every strict inequality +(the minimum exceeds0.007594638501835091171332). It does not use a numerical +optimizer or a floating tolerance. Symbolic zero vectors are checked before +interval evaluation. Bin capacities are8,16,32,48; their counts are +241920,161280,161280,161280. The true local inventories yield widths +5:90720,6:58320,7:171720,8:311040,9:690120 across3240 calls. + +All actual incumbent patterns are dual-tight. This is checked both on the +small complete integer pattern certificate and, in the explicit external +replay, by reading all1321920 literal roles and all725760 bins from immutable +source FILL/TEMPLATE data. Therefore the incumbent idle cost equals its dual +lower bound, not merely some unattained estimate. + +Weak duality gives, for every new packing, idle_new>=dual_new. Since the +incumbent attains its dual, idle_new-idle_old>=sum delta_n_w*pi(w). Total role +count is fixed. The affine helper prices make this last expression exactly +-qD, even if width changes differ per call. Hence the best possible idle +credit is at most qD. It is not necessary that the changed inventory can +actually attain this bound: a lower bound is enough for rejection. + +## Local rank function and the full budget + +A terminal frame is a subspace of F_2^9. If its last paid climb had dimension +r and the terminal extends by d while the preceding frame is fixed, the new +charge is h(r+d) instead of h(r). The Grassmann rank identity gives this +increase independently of the extension's orientation. Because0= d*(h(9)-h(8)). + +This is also checked as nine exact inequalities. Summing all roles gives a +local surcharge at least mD, m=h(9)-h(8). The finite certificate encloses + + 0.987736182658129815011783 < q < 0.987736182658129815011784, + 0.994579846771465221497966 < m < 0.994579846771465221497967, + 0.006843664113335406486182 < m-q < 0.006843664113335406486183. + +Adding the local and idle inequalities proves the stated complete deficit. +No dirty-state or phase relaxation is used to assert a new working circuit: +this is a necessary-cost rejection of a broader relaxed class, so proving +some candidate semantically valid could only shrink that class. + +## Sharper fixed-identity zero-feasibility certificate + +Retaining actual owner/time/child/port identities is even more restrictive. +For each role a nonnegative increment d obeys both + + d <= 9-dim(terminal), + sum_{roles in bin} d <= capacity - occupied width. + +Every occupied bin with positive residual capacity has only width9 roles, +whose terminal dimension is9. There are23328 bins with five width9 roles and +slack3, and4320 bins with three width9 roles and slack5. Every other occupied +bin is saturated. The137952 empty rank48 bins contain no retained role. +Consequently every d is zero. This is a rank-capacity certificate, not a +failed enumeration of frame orientations. It covers call-specific increments. +A proposed role reassignment invalidates this sharper premise, but is still +covered by the more permissive tariff theorem above. + +## Dirty state, controls and limits + +No candidate word is emitted or admitted. The exact pinned words are retained; +the credited audit core freshly computes their frame invoices and role +entrance/terminal dimensions. Previous PR3969 established relative arbitrary +dirty scalar/permutation identity and the literal owner bridge. Native phases +and universal physical/precision/stock/tape assumptions are not re-audited. +These obligations are unknown/inherited, never zero. The original3945 gain +jointly reprices interior frames and lies outside our rejected class. + +Controls include a genuine positive rank1-gap absorption fixture (h(2)-2<0), +noncoordinate subspace rank, omission of local cost falsely creating a gain, +and actual optimized production CLI mutations of dual, capacity, empty-bin +coverage and source bytes. The positive fixture explains why the gate is a +complete-budget test rather than a universal anti-extension assertion. + +## Bounded pivot: the17 direct rank-one refunds cannot finance an extension + +There is a concrete terminal-only shrinking option, so we priced it rather +than interpreting the one-sided theorem as an obstruction to every change. +Both frozen providers have exactly17 protected width5 helpers whose last +terminal climb has rank1. Their preceding frame is the unique legal terminal +of one less dimension. The other74 protected terminals have zero last climb, +so cannot shrink with the preceding frames fixed. The unprotected helpers +retain FULL terminals under the inherited cleanup contract; adding new private +buffers is outside this scope. + +Extend the credited dual to width4 by pi(4)=1-h(5). The supplementary checker +examines all2551 patterns in widths4..9 at the same exact3945 endpoint. It finds +12 symbolic tight and2539 strictly positive inequalities. The original actual +packing still attains the bound. Therefore every width5->4 refund raises the +best possible idle tariff by at least pi(4)-pi(5)=1, exactly canceling its +saved terminal rank1 child. Such a refund can tie, but cannot pay by itself. + +For simultaneous direct refunds on R roles and terminal extensions adding D +other dimensions, the idle change is at least R-qD while the local change is +at least -R+mD. The same positive (m-q)D deficit remains. For D=0 the complete +change is nonnegative. This rejects that concrete mixed pivot before any +relocation search. Equal-dimension frame rotations are tariff-neutral here; +changing interior frames, entrances or the protected-buffer set remains open. +No larger terminal search or unpriced new native module is justified by this +pivot. The supplementary code shares the main exact power routine and is not +claimed as an independent numerical implementation. diff --git a/research/staged544-terminal-extension-budget/README.md b/research/staged544-terminal-extension-budget/README.md new file mode 100644 index 0000000000..cd6cbf9355 --- /dev/null +++ b/research/staged544-terminal-extension-budget/README.md @@ -0,0 +1,92 @@ +# A complete tariff barrier for terminal-only extensions of staged544 + +At PR3945's pinned endpoint, every positive terminal-only enlargement loses +more than **0.006843664113335406486182 tariff units per added dimension**, even +when owner placement is relaxed to arbitrary fractional repacking. A joint +interior refit must beat this deficit before its construction is worth expanding. +This is a scoped necessary-cost theorem, not a new supplier or kappa. + +The mathematical pairing is binary subspace rank/flag geometry with +capacitated packing and linear-program duality. The credited3815/3862/3890 +dual supplies a global owner-credit bound; rank concavity supplies the smallest +possible added terminal invoice. Their sum closes a construction route which +a local terminal/frame search alone cannot assess. The dual itself is prior +work; the new contribution is this exact terminal-cost implication, at the +changed3945 endpoint and with actual owner/source binding. + +Keep helper entrances and every paid interior scalar/native frame fixed; +enlarge arbitrary terminal subspaces in F_2^9, independently per call if desired. +Allow any new owner assignment under the same rank8/16/32/48 bin inventory. +At k=1730663236534549309146/10^24, with h(r)=r^(1-k), the maximum possible +idle credit per added dimension is less than0.987736182658129815011784. +The minimum terminal surcharge is greater than0.994579846771465221497966. +The difference is strictly positive. This rejects noncoordinate as well as +coordinate extensions and does not depend on finding a feasible new allocation. + +The current literal allocation also has a sharper obstruction: every occupied +bin with slack contains only helpers already at dimension9. Thus retaining +owner/time/child/port identities permits zero positive terminal increments. +The exact external audit covers1321920 roles and725760 bins. Both frozen +provider words freshly yield the complete baseline profile +`{1:8041680,2:2306880,3:729648,4:353160,5:69120,8:25920,48:137952}`. + +The successful PR3945 changes interior scalar/native frames jointly. It is +outside this theorem. A bounded mixed case is also closed: exactly17 direct protected terminal refunds +5->4 per provider save one rank1 child each, but the full width4..9 dual charges +exactly one idle child back. All2551 patterns are certified; these refunds cannot +finance a positive extension. More general shrinking/enlarging, changed entrances, changed +recursive templates and other paid-interior rewrites also remain open. No +selected-frontier or native-phase admission is asserted. + +## Reproduce + +Standard library Python3.12; no solver or downloads during the default replay: + +```sh +python3 -B scripts/research_package.py --package research/staged544-terminal-extension-budget +``` + +This checks all841 packing patterns (11 symbolic tight,830 strictly positive), +both frozen frame invoices, the full integer aggregate owner certificate, +complete local-plus-idle budget, the2551-pattern refund corollary, and actual optimized CLI mutations. The +credited audit_core.py computes frame bills; it is explicitly reused, not +presented as independently implemented. The dual/interval/budget code is new. +The optional full literal row check uses two byte-pinned external owner inputs: + +```sh +python3 research/staged544-terminal-extension-budget/fetch_sources.py --output /tmp/terminal-owner-sources +python3 -B research/staged544-terminal-extension-budget/verify.py --source-root /tmp/terminal-owner-sources +``` + +The destination must be fresh. This full mode reconstructs the small owner +pattern certificate from every original row and all empty bins. It verifies +capacity/role identity/prefix offsets; chronology and physical-family checks +were independently performed in PR3969 and are inherited here. See VALIDATION +for exactly which modes were executed. Ordinary verification never writes +inside the package. `--emit` requires an explicit external destination. + +## Sources and credit + +- Dugongue PR3945 `91f81d131252db704f945891da1ea54e29d46b8b`: changed local/native + terminal construction and complete owner input. +- PR3969 `6ff67539f1131a287eb9a9a98bf1e94a02eecba7`: independent local/owner bridge. +- Erwan Secousses / ChaloupeMusic PR3815, Sagar Thakrar PR3862, ToikY PR3890 + `772953c9bda6d41db7b89e4cd6bae3dc05d7636e`: packing model, dual, exact face and + width-price formula. The new endpoint check does not overwrite their pins. +- dataisfire PR3734, zxv PR3682, Ross Richardson PR3605, hexapode PR3802/3875, + Jeremy Kothe, Thakrar PR3687, roger-sato PR3693, Arham Tahir, and the complete + source/native/owner lineage retained in frozen/SOURCE-CREDITS.md. + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. +No independent human or proof-kernel verification is claimed. + +## Open next questions + +Find one coordinated interior frame change with exact savings above +0.006843664113335406486182 per added terminal dimension, plus a literal owner +reassignment. Start by displaying its changed before/after paid frame climbs +and actual subspace containments; only then seek chronological placement. +Native phase, arbitrary-dirty cleanup, physical hosting and uniform costs must +be accounted for before supplier admission. A dimension-only packing solution +is insufficient. A mixed shrink/extend move may escape this theorem, but needs +its own complete bill rather than borrowing the one-sided bound. diff --git a/research/staged544-terminal-extension-budget/REFUND-RESULT.json b/research/staged544-terminal-extension-budget/REFUND-RESULT.json new file mode 100644 index 0000000000..3b1bc6cb3d --- /dev/null +++ b/research/staged544-terminal-extension-budget/REFUND-RESULT.json @@ -0,0 +1,59 @@ +{ + "conclusion": "Any subset of these rank1 refunds ties at best under arbitrary repacking; combining them with positive terminal-only extensions still loses more than the main theorem gap times total added dimensions. Interior changes excluded.", + "minimum_positive_reduced_cost": { + "denominator": 1000000000000000000000000, + "lower_numerator": 4054784837799773772952, + "upper_numerator": 4054784837799773772953 + }, + "patterns": 2551, + "providers": { + "base": { + "protected_without_refund": 74, + "refundable_registers": [ + 277, + 307, + 323, + 325, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 378, + 385, + 387, + 389, + 394 + ] + }, + "extra": { + "protected_without_refund": 74, + "refundable_registers": [ + 277, + 307, + 323, + 325, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 378, + 385, + 387, + 389, + 394 + ] + } + }, + "refund_idle_price_minus_terminal_saving": "0 exactly", + "status": "PASS_REFUND_EXTENDED_BUDGET", + "strict": 2539, + "symbolic_tight": 12 +} diff --git a/research/staged544-terminal-extension-budget/RESULT.json b/research/staged544-terminal-extension-budget/RESULT.json new file mode 100644 index 0000000000..4d5027da99 --- /dev/null +++ b/research/staged544-terminal-extension-budget/RESULT.json @@ -0,0 +1,2691 @@ +{ + "controls": [ + "dual RHS perturbation rejected", + "rank1 absorption positive fixture", + "omitted local charge fake gain exposed", + "capacity mutation exposes false allowance", + "noncoordinate dimension fixture" + ], + "dual": { + "idle_credit_per_dimension": { + "denominator": 1000000000000000000000000, + "lower_numerator": 987736182658129815011783, + "upper_numerator": 987736182658129815011784 + }, + "mandatory_interior_saving_per_dimension": { + "denominator": 1000000000000000000000000, + "lower_numerator": 6843664113335406486182, + "upper_numerator": 6843664113335406486183 + }, + "minimum_strict_reduced_cost": { + "denominator": 1000000000000000000000000, + "lower_numerator": 7594638501835091171332, + "upper_numerator": 7594638501835091171333 + }, + "minimum_terminal_charge_per_dimension": { + "denominator": 1000000000000000000000000, + "lower_numerator": 994579846771465221497966, + "upper_numerator": 994579846771465221497967 + }, + "patterns": 841, + "strict_patterns": 830, + "tight_patterns": [ + [ + 8, + [ + 0, + 0, + 0, + 1, + 0 + ], + 0 + ], + [ + 16, + [ + 0, + 0, + 0, + 2, + 0 + ], + 0 + ], + [ + 16, + [ + 0, + 0, + 1, + 0, + 1 + ], + 0 + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 3 + ], + 5 + ], + [ + 32, + [ + 0, + 0, + 0, + 4, + 0 + ], + 0 + ], + [ + 32, + [ + 0, + 0, + 1, + 2, + 1 + ], + 0 + ], + [ + 32, + [ + 0, + 0, + 2, + 0, + 2 + ], + 0 + ], + [ + 32, + [ + 0, + 1, + 0, + 1, + 2 + ], + 0 + ], + [ + 32, + [ + 1, + 0, + 0, + 0, + 3 + ], + 0 + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0 + ], + 48 + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 5 + ], + 3 + ] + ] + }, + "kappa": "865331618267274654573/500000000000000000000000", + "local": { + "base": { + "frozen_word_sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "local_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "registers": [ + 224, + 225, + 226, + 227, + 228, + 229, + 230, + 231, + 232, + 233, + 234, + 235, + 236, + 237, + 238, + 239, + 240, + 241, + 242, + 243, + 244, + 245, + 246, + 247, + 248, + 249, + 250, + 251, + 252, + 253, + 254, + 255, + 256, + 257, + 258, + 259, + 260, + 261, + 262, + 263, + 264, + 265, + 266, + 267, + 268, + 269, + 270, + 271, + 272, + 273, + 274, + 275, + 276, + 277, + 278, + 279, + 280, + 281, + 282, + 283, + 284, + 285, + 286, + 287, + 288, + 289, + 290, + 291, + 292, + 293, + 294, + 295, + 296, + 297, + 298, + 299, + 300, + 301, + 302, + 303, + 304, + 305, + 306, + 307, + 308, + 309, + 310, + 311, + 312, + 313, + 314, + 315, + 316, + 317, + 318, + 319, + 320, + 321, + 322, + 323, + 324, + 325, + 326, + 327, + 328, + 329, + 330, + 331, + 332, + 333, + 334, + 335, + 336, + 337, + 338, + 339, + 340, + 341, + 342, + 343, + 344, + 345, + 346, + 347, + 348, + 349, + 350, + 351, + 352, + 353, + 354, + 355, + 356, + 357, + 358, + 359, + 360, + 361, + 362, + 363, + 364, + 365, + 366, + 367, + 368, + 369, + 370, + 371, + 372, + 373, + 374, + 375, + 376, + 377, + 378, + 379, + 380, + 381, + 382, + 383, + 384, + 385, + 386, + 387, + 388, + 389, + 390, + 391, + 392, + 393, + 394, + 395, + 396, + 397, + 398, + 399, + 400, + 401, + 402, + 403, + 404, + 405, + 406, + 407, + 408, + 409, + 410, + 411, + 412, + 413, + 414, + 415, + 416, + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 425, + 426, + 427, + 428, + 429, + 430, + 431, + 432, + 433, + 434, + 435, + 436, + 437, + 438, + 439, + 440, + 441, + 442, + 443, + 444, + 445, + 446, + 447, + 448, + 449, + 450, + 451, + 452, + 453, + 454, + 455, + 456, + 457, + 458, + 459, + 460, + 461, + 462, + 463, + 464, + 465, + 466, + 467, + 468, + 469, + 470, + 471, + 472, + 473, + 474, + 475, + 476, + 477, + 478, + 479, + 480, + 481, + 484, + 485, + 486, + 487, + 488, + 489, + 490, + 491, + 492, + 493, + 496, + 497, + 498, + 499, + 500, + 501, + 502, + 503, + 504, + 505, + 506, + 508, + 509, + 510, + 511, + 512, + 513, + 514, + 515, + 516, + 517, + 518, + 520, + 521, + 522, + 523, + 524, + 525, + 526, + 527, + 528, + 529, + 530, + 531, + 532, + 533, + 534, + 535, + 536, + 537, + 538, + 539, + 540, + 541, + 542, + 543, + 544, + 545, + 546, + 547, + 548, + 549, + 550, + 551, + 552, + 553, + 554, + 555, + 556, + 557, + 558, + 559, + 560, + 561, + 562, + 563, + 564, + 565, + 566, + 567, + 568, + 569, + 570, + 571, + 572, + 573, + 574, + 575, + 576, + 577, + 578, + 579, + 580, + 581, + 582, + 583, + 584, + 585, + 586, + 587, + 588, + 589, + 590, + 591, + 592, + 593, + 594, + 596, + 600, + 601, + 602, + 604, + 608, + 609, + 610, + 612, + 616, + 617, + 618, + 620, + 624, + 625, + 626, + 628, + 632, + 633, + 634, + 636, + 640, + 641, + 642, + 644, + 648, + 649, + 650, + 652, + 656, + 657, + 658, + 660, + 664, + 665, + 666, + 668, + 670, + 671, + 672, + 673, + 674, + 676 + ], + "terminal_climb_histogram": { + "0": 74, + "1": 240, + "2": 40, + "3": 54 + }, + "terminal_dimensions": [ + 9, + 9, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 7, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 5, + 9, + 5, + 9, + 8, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 5, + 9, + 5, + 9, + 8, + 9, + 9, + 5, + 7, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 8, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 7, + 7, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 9, + 9, + 9, + 9, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 7, + 7, + 7, + 7, + 8, + 8, + 7, + 8, + 7, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "widths": [ + 9, + 9, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 7, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 5, + 9, + 5, + 9, + 8, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 5, + 9, + 5, + 9, + 8, + 9, + 9, + 5, + 7, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 8, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 9, + 8, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 7, + 7, + 7, + 7, + 8, + 9, + 8, + 9, + 6, + 6, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 6, + 6, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 7, + 6, + 6, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 7, + 7, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 7, + 7, + 6, + 6, + 9, + 8, + 9, + 8, + 8, + 8, + 8, + 8, + 7, + 7, + 9, + 8, + 9, + 8, + 7, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 6, + 7, + 6, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 7, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 7, + 8, + 8, + 8, + 8, + 5, + 5, + 8, + 8, + 8, + 8 + ] + }, + "extra": { + "frozen_word_sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + }, + "local_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "registers": [ + 224, + 225, + 226, + 227, + 228, + 229, + 230, + 231, + 232, + 233, + 234, + 235, + 236, + 237, + 238, + 239, + 240, + 241, + 242, + 243, + 244, + 245, + 246, + 247, + 248, + 249, + 250, + 251, + 252, + 253, + 254, + 255, + 256, + 257, + 258, + 259, + 260, + 261, + 262, + 263, + 264, + 265, + 266, + 267, + 268, + 269, + 270, + 271, + 272, + 273, + 274, + 275, + 276, + 277, + 278, + 279, + 280, + 281, + 282, + 283, + 284, + 285, + 286, + 287, + 288, + 289, + 290, + 291, + 292, + 293, + 294, + 295, + 296, + 297, + 298, + 299, + 300, + 301, + 302, + 303, + 304, + 305, + 306, + 307, + 308, + 309, + 310, + 311, + 312, + 313, + 314, + 315, + 316, + 317, + 318, + 319, + 320, + 321, + 322, + 323, + 324, + 325, + 326, + 327, + 328, + 329, + 330, + 331, + 332, + 333, + 334, + 335, + 336, + 337, + 338, + 339, + 340, + 341, + 342, + 343, + 344, + 345, + 346, + 347, + 348, + 349, + 350, + 351, + 352, + 353, + 354, + 355, + 356, + 357, + 358, + 359, + 360, + 361, + 362, + 363, + 364, + 365, + 366, + 367, + 368, + 369, + 370, + 371, + 372, + 373, + 374, + 375, + 376, + 377, + 378, + 379, + 380, + 381, + 382, + 383, + 384, + 385, + 386, + 387, + 388, + 389, + 390, + 391, + 392, + 393, + 394, + 395, + 396, + 397, + 398, + 399, + 400, + 401, + 402, + 403, + 404, + 405, + 406, + 407, + 408, + 409, + 410, + 411, + 412, + 413, + 414, + 415, + 416, + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 425, + 426, + 427, + 428, + 429, + 430, + 431, + 432, + 433, + 434, + 435, + 436, + 437, + 438, + 439, + 440, + 441, + 442, + 443, + 444, + 445, + 446, + 447, + 448, + 449, + 450, + 451, + 452, + 453, + 454, + 455, + 456, + 457, + 458, + 459, + 460, + 461, + 462, + 463, + 464, + 465, + 466, + 467, + 468, + 469, + 470, + 471, + 472, + 473, + 474, + 475, + 476, + 477, + 478, + 479, + 480, + 481, + 484, + 485, + 486, + 487, + 488, + 489, + 490, + 491, + 492, + 493, + 496, + 497, + 498, + 499, + 500, + 501, + 502, + 503, + 504, + 505, + 506, + 508, + 509, + 510, + 511, + 512, + 513, + 514, + 515, + 516, + 517, + 518, + 520, + 521, + 522, + 523, + 524, + 525, + 526, + 527, + 528, + 529, + 530, + 531, + 532, + 533, + 534, + 535, + 536, + 537, + 538, + 539, + 540, + 541, + 542, + 543, + 544, + 545, + 546, + 547, + 548, + 549, + 550, + 551, + 552, + 553, + 554, + 555, + 556, + 557, + 558, + 559, + 560, + 561, + 562, + 563, + 564, + 565, + 566, + 567, + 568, + 569, + 570, + 571, + 572, + 573, + 574, + 575, + 576, + 577, + 578, + 579, + 580, + 581, + 582, + 583, + 584, + 585, + 586, + 587, + 588, + 589, + 590, + 591, + 592, + 593, + 594, + 596, + 600, + 601, + 602, + 604, + 608, + 609, + 610, + 612, + 616, + 617, + 618, + 620, + 624, + 625, + 626, + 628, + 632, + 633, + 634, + 636, + 640, + 641, + 642, + 644, + 648, + 649, + 650, + 652, + 656, + 657, + 658, + 660, + 664, + 665, + 666, + 668, + 670, + 671, + 672, + 673, + 674, + 676 + ], + "terminal_climb_histogram": { + "0": 74, + "1": 240, + "2": 40, + "3": 54 + }, + "terminal_dimensions": [ + 9, + 9, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 7, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 5, + 9, + 5, + 9, + 8, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 5, + 9, + 5, + 9, + 8, + 9, + 9, + 5, + 7, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 8, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 7, + 7, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 7, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 9, + 9, + 9, + 9, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 7, + 7, + 7, + 7, + 8, + 8, + 7, + 8, + 7, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "widths": [ + 9, + 9, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 7, + 9, + 7, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 7, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 5, + 9, + 5, + 9, + 8, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 5, + 9, + 5, + 9, + 8, + 9, + 9, + 5, + 7, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 8, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 9, + 9, + 9, + 9, + 9, + 9, + 5, + 9, + 5, + 9, + 5, + 9, + 9, + 9, + 9, + 5, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 6, + 9, + 8, + 8, + 9, + 8, + 9, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 8, + 8, + 7, + 7, + 7, + 7, + 8, + 9, + 8, + 9, + 6, + 6, + 7, + 7, + 7, + 7, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 6, + 6, + 8, + 8, + 8, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 7, + 6, + 6, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 8, + 7, + 7, + 8, + 9, + 9, + 9, + 9, + 8, + 8, + 8, + 8, + 7, + 7, + 6, + 6, + 9, + 8, + 9, + 8, + 8, + 8, + 8, + 8, + 7, + 7, + 9, + 8, + 9, + 8, + 7, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 7, + 7, + 7, + 7, + 7, + 7, + 6, + 7, + 6, + 7, + 7, + 7, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 7, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 7, + 8, + 8, + 8, + 8, + 5, + 5, + 8, + 8, + 8, + 8 + ] + } + }, + "owner": { + "all_actual_patterns_dual_tight": true, + "bins": 725760, + "calls": 3240, + "complete_profile": { + "1": 8041680, + "2": 2306880, + "3": 729648, + "4": 353160, + "5": 69120, + "8": 25920, + "48": 137952 + }, + "fixed_identity_feasible_nonnegative_extensions": 0, + "idle_profile": { + "3": 23328, + "5": 4320, + "48": 137952 + }, + "occupied_bins": 587808, + "roles": 1321920 + }, + "source_root_endpoint": "0.001730663236534549309146", + "status": "PASS_EXACT_TERMINAL_EXTENSION_BUDGET" +} diff --git a/research/staged544-terminal-extension-budget/SOURCES.json b/research/staged544-terminal-extension-budget/SOURCES.json new file mode 100644 index 0000000000..662708c006 --- /dev/null +++ b/research/staged544-terminal-extension-budget/SOURCES.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "external_snapshot": { + "manifest": "EXTERNAL-SOURCES.json", + "head": "91f81d131252db704f945891da1ea54e29d46b8b", + "relation": "Immutable external source snapshot, not asserted ancestor. Frozen words/audit core and full owner data pin bytes inFROZEN/EXTERNAL-SOURCES. Credited dual proof PR3890head772953c9bda6d41db7b89e4cd6bae3dc05d7636e retained." + } +} diff --git a/research/staged544-terminal-extension-budget/TASK.json b/research/staged544-terminal-extension-budget/TASK.json new file mode 100644 index 0000000000..5e3e3467c1 --- /dev/null +++ b/research/staged544-terminal-extension-budget/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "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": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "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.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "New complete-budget obstruction for terminal-only monotone subspace enlargement beyond3945, including arbitrary fractional owner repacking at its pinned endpoint; exact fixed-owner rank-capacity certificate.", + "scope_change_reason": "Assigned contrasting subspace rank and capacitated-flow/duality approach to changed-boundary construction. The optimistic full bill rejects terminal-only extension, so stop construction and preserve the exact new implication.", + "bottleneck_link": "A local terminal gain is useful only if every changed dimension fits an actual chronological owner and its complete recursive bill is paid.", + "budget_minutes": 60, + "stop_rule": "Stop after exact full-budget dual+terminal charge rejection. Interior refits, shrink/enlarge exchanges and new source interfaces require a separately priced allowance.", + "outcome": "completed", + "evidence": "RESULT.json, OWNER-PATTERNS.json, LEDGER.json, PROOF.md and VALIDATION.json", + "author": "Chris R / Clear1nsight with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; one agent independently implemented checker while root coordinated overlap/publication.", + "open_questions": [ + { + "question": "Which coordinated interior-frame refit saves more than0.006843664113335406486182 per added terminal dimension at the3945 endpoint?", + "why_it_matters": "Any terminal-only extension loses even with optimistic global repacking.", + "first_step": "Produce one exact changed interior frame invoice plus actual rank-preserving/raising terminal subspaces, then price its complete owner reassignment.", + "blocked_by": "Needs literal compatible frames, arbitrary-dirty restoration, native recipe and actual chronological owner placement; no favorable module has yet been supplied." + } + ], + "expansion_decision": "NARROW then STOP terminal-only expansion: exact full-bill allowance is negative.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3945#issuecomment-6262411007", + "bounded_pivot": "Exact full-width4..9dual rejects financing extensions with any subset of17direct protected rank1terminal refunds; no relocationsearch launched." +} diff --git a/research/staged544-terminal-extension-budget/VALIDATION.json b/research/staged544-terminal-extension-budget/VALIDATION.json new file mode 100644 index 0000000000..828b66b5fe --- /dev/null +++ b/research/staged544-terminal-extension-budget/VALIDATION.json @@ -0,0 +1,31 @@ +{ + "status": "PASS_FROZEN_REGISTERED_AND_FULL_OWNER", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "registered": { + "seconds": 45.05938835699999, + "returncode": 0, + "command": "python3 -B scripts/research_package.py --package research/staged544-terminal-extension-budget", + "scope": "841pattern theorem;2551pattern refund corollary; both provider frame invoices; all integer aggregate bins; production optimized CLI mutations" + }, + "full_owner": { + "normal": "PASS initial full source run; runtime not instrumented", + "optimized_seconds": 35.10517586499918, + "optimized_returncode": 0, + "command": "python3 -O -B research/staged544-terminal-extension-budget/verify.py --source-root ", + "coverage": "1321920 literal rows and725760bins, capacities/prefixes/role indexing and exact pattern equality; chronology/family re-audit not claimed" + }, + "code_freeze": { + "refund_corollary.py": "58c0ae2c5bc7d66db8cf60089a373010d822c50c6ae7b29793640710e7908929", + "check_controls.py": "48d9c36fa41a71bba7f7f93479ac6c27f6fff34bfaab8dc1b31da8cdcf6c059f", + "verify.py": "7ded290b69f9f9937018096a65ed22ebf5a78909fc5c2a0589eeea97b8859e65", + "fetch_sources.py": "61f4e185c5be7d92d64edee45ca0ab24d3b92dd45aadfd41f05f644fd7b0cc1e", + "frozen/audit_core.py": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951" + }, + "source_transport": "Exact immutable compressed words and PR3890 proof bytes; proof Gitblob850fc31a4375797681031fc15f63e6162f294fcf; SHA256 manifests checked", + "unrun": [ + "No new arbitrary-dirty circuit candidate; predecessor identity inherited", + "Native phase/outer/all-size/uniform/analytic/BIT not replayed", + "No new root isolation", + "Hosted CI and committed-byte/export checks are reported at publication, not preclaimed here" + ] +} diff --git a/research/staged544-terminal-extension-budget/VERIFY.json b/research/staged544-terminal-extension-budget/VERIFY.json new file mode 100644 index 0000000000..7b270321a4 --- /dev/null +++ b/research/staged544-terminal-extension-budget/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact841pattern dual, both provider frame invoices, incumbent integer pattern equality and complete tariff deficit. Full literal owner rows require explicit external sources." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/refund_corollary.py" + ], + "timeout_seconds": 240, + "checks": "All2551width4..9patterns at3945endpoint;17direct rank1 refunds per provider cannot finance any terminal-only extension." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/check_controls.py" + ], + "timeout_seconds": 360, + "checks": "Four actual optimized production CLI mutations reject." + } + ] +} diff --git a/research/staged544-terminal-extension-budget/check_controls.py b/research/staged544-terminal-extension-budget/check_controls.py new file mode 100644 index 0000000000..3dd9630516 --- /dev/null +++ b/research/staged544-terminal-extension-budget/check_controls.py @@ -0,0 +1,29 @@ +"""Real optimized-CLI mutations of the production checker; standard library.""" +from pathlib import Path +import hashlib,json,shutil,subprocess,sys,tempfile +ROOT=Path(__file__).resolve().parent + +def need(ok,why): + if not ok:raise ValueError(why) +def main(): + cases=[] + with tempfile.TemporaryDirectory(prefix='terminal-budget-controls-') as d: + for name in ['dual','capacity','missing_empty_bin','source_bytes']: + p=Path(d)/name;shutil.copytree(ROOT,p) + for f in p.rglob('*'): + if f.is_file():f.chmod(0o600) + if name=='dual': + f=p/'verify.py';s=f.read_text();needle='48:Q(1,20),3:Q(-1,20),5:Q(-1,4)';need(s.count(needle)==1,'dual mutation anchor');f.write_text(s.replace(needle,'48:Q(1,10),3:Q(-1,20),5:Q(-1,4)')) + elif name in ('capacity','missing_empty_bin'): + f=p/'OWNER-PATTERNS.json';v=json.loads(f.read_text()) + if name=='capacity':v['patterns'][0][0]+=1 + else:v['patterns']=[r for r in v['patterns'] if any(r[1])] + f.write_text(json.dumps(v)) + else: + f=p/'frozen/PROFILE.json';f.write_bytes(f.read_bytes()+b' ') + r=subprocess.run([sys.executable,'-O','-B',str(p/'verify.py')],capture_output=True,text=True,timeout=180) + need(r.returncode!=0,'mutation accepted '+name) + expected={'dual':'dual infeasibility','capacity':'pattern capacity','missing_empty_bin':'complete bin counts','source_bytes':'frozen source'}[name] + need(expected in r.stderr,'wrong rejection '+name+': '+r.stderr[-1000:]);cases.append(name) + print(json.dumps({'status':'PASS_PRODUCTION_CLI_MUTATIONS','rejected':cases})) +if __name__=='__main__':main() diff --git a/research/staged544-terminal-extension-budget/fetch_sources.py b/research/staged544-terminal-extension-budget/fetch_sources.py new file mode 100644 index 0000000000..4c0caa7ea7 --- /dev/null +++ b/research/staged544-terminal-extension-budget/fetch_sources.py @@ -0,0 +1,15 @@ +"""Explicit immutable owner-source fetch; writes only to a new external folder.""" +from pathlib import Path +import argparse,hashlib,json,urllib.request +ROOT=Path(__file__).resolve().parent + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--output',type=Path,required=True);a=ap.parse_args();p=a.output.resolve() + if p.exists() or p.is_relative_to(ROOT):raise ValueError('fresh external directory required') + pins=json.loads((ROOT/'EXTERNAL-SOURCES.json').read_text());p.mkdir(parents=True) + for rel,digest in pins['files'].items(): + data=urllib.request.urlopen(pins['base_url']+rel,timeout=120).read() + if hashlib.sha256(data).hexdigest()!=digest:raise ValueError('immutable source digest '+rel) + q=p/rel;q.parent.mkdir(parents=True,exist_ok=True);q.write_bytes(data) + print('PASS_FETCHED_IMMUTABLE_OWNER_SOURCES') +if __name__=='__main__':main() diff --git a/research/staged544-terminal-extension-budget/frozen/PR3890-PROOF.md b/research/staged544-terminal-extension-budget/frozen/PR3890-PROOF.md new file mode 100644 index 0000000000..850fc31a43 --- /dev/null +++ b/research/staged544-terminal-extension-budget/frozen/PR3890-PROOF.md @@ -0,0 +1,170 @@ +# Complete sharp-price region in the frozen ideal + +All statements here use the fixed exponent +`a = 1730578437266246818741/10^24` and `h(l)=l^(1-a)`, with `h(0)=0`. +This is the upper endpoint used by Erwan Secousses in PR3815 and Sagar Thakrar +in PR3862. It is not a new root enclosure or a new kappa. + +## Model and exact dual face + +Per owner replica, demands for widths `(4,5,6,7,8,9)` are +`(234,18,162,477,864,1917)` and bin counts for capacities `(8,16,32,48)` are +`(672,448,448,448)`. Each helper fits wholly in one bin; the remainder is +paid as one child. Counts may be fractional. No clock, per-call collision, +restoration or physical staging condition is imposed in this relaxation. + +The objective is the sum of `h(remainder)` over all bins. The local paid +profile and live normalizer stay outside this objective and must be added +when pricing any real change. The model is retained from PR3815, following +dataisfire's PR3734 and zxv's PR3682. + +The ten columns of `MODEL.json` form an invertible matrix A: six helper +count rows followed by four bin count rows. The basis dual is the unique +solution `A^T lambda = h(remainders)`. Its closed form is independently +reconstructed in `independent.py`. Equivalently, with helper prices pi: + +``` +pi9 = (h(3)-h(48))/5 +pi8 = (3*pi9-h(5))/4 +pi7 = 2*pi8-pi9; pi6 = 3*pi8-2*pi9 +pi5 = -h(5); pi4 = 1-h(5) +mu8 = -pi8; mu16 = -2*pi8; mu32 = -4*pi8; mu48 = h(48) +``` + +For every feasible pattern p in a bin c its reduced cost is +`h(c-w.p)-pi.p-mu_c`. Both checkers enumerate all 2,551 integer count +patterns of widths 4..9 in these bins. Exactly twelve have identically zero +symbolic reduced cost: the ten basis columns plus `[8,8]@16` and +`[8,8,8,8]@32`. Every other pattern has a strictly positive outward rational +lower bound at this fixed exponent (minimum exceeds 0.0040545). This proves +both dual feasibility and completeness of this tight face. The check uses +symbolic identities for the zero cases, never a floating tolerance. + +PR3815/3862 solve a dual for outward rational lower approximations to h. +Here the symbolic dual uses the exact function h and interval arithmetic +certifies its inequalities. Its prices are consistent with their enclosures; +we do not claim bit-identical rational proxy prices or re-certify their root. + +The primary checker uses rational matrix elimination, Cartesian count-vector +enumeration and alternating negative-exponential bounds. The second uses +closed-form dual coordinates, ascending multisets and positive exponential +series followed by reciprocals. Neither imports or executes predecessor +code or the other checker. Logarithms use reduced atanh series with explicit +geometric tails; all rounding is outward. No numerical optimizer is needed. + +By weak duality, the common dual gives a lower bound for every packing of +any changed inventory with these bins. Equality occurs exactly when all +positive-count patterns belong to these twelve. Therefore feasibility on this +face is necessary and sufficient for the common price to be attained. + +## Eliminate the two extra columns + +For a changed demand vector d, let `y=A^-1(d,B)`. The extra `[8,8]@16` +column has basis coordinates `(0,1,0,0,0,1,0,-1,0,0)` and the extra +`[8,8,8,8]@32` column has coordinates `(0,0,0,0,0,2,0,-1,0,0)`. +If their counts are z1,z2, the basic counts are `y-D1*z1-D2*z2`. +All y coordinates except indices 1,5,7 must be nonnegative. The remaining +conditions are + +``` +z1,z2 >= 0; z1 <= y1; z1+2*z2 <= y5; y7+z1+z2 >= 0. +``` + +They are feasible exactly when +`y1>=0`, `y5>=0`, `y7+y5>=0`, `2*y7+y1+y5>=0`. +For sufficiency put `L=max(0,-y7)`, `z1=min(L,y1)`, `z2=L-z1`. +The last two inequalities respectively give `L<=y5` and `2L<=y1+y5`, +which imply `z1+2*z2<=y5`. This supplies an explicit rational packing. +Necessity follows by adding the displayed inequalities. The independent +checker eliminates the same face in a different set of direct count variables. + +## Joint adjacent inventory flows + +Let xj be the nonnegative number of helper-calls moved from width j to j-1, +for j=5,6,7,8,9, per owner replica. These are net inventory flows; if a literal +rewrite can touch each original helper only once it has additional availability +constraints. In particular x5<=18 must then be imposed separately. + +The changed demands are + +``` +(234+x5, 18-x5+x6, 162-x6+x7, 477-x7+x8, 864-x8+x9, 1917-x9). +``` + +Writing `S=x6+x7+x8+x9`, exact matrix elimination gives + +``` +y0=672; y1=448; y2=234+x5; y3=162-x6+x7; y4=18-x5+x6 +y5=15+(x6-x7-x8+x9)/2; y6=12-S/4 +y7=7-S/4+x8; y8=1916/5+S/20; y9=324/5-S/20. +``` + +Substituting into the previous feasibility conditions gives exactly + +``` +S <= 48 +x5 <= 18+x6 +x7+x8 <= 30+x6+x9 +3*x7 <= 88+x6+x8+x9. +``` + +All flows must also be nonnegative. There are no hidden additional inequalities: +the first makes y3>=114, y8>0, y9>=312/5, and +`2*y7+y1+y5=477-x7+x8>=429`. Other nontrivial conditions are exactly the +four displayed ones. The constructive formula above proves sufficiency for +every rational point, not merely the finite comparison grid. The argument +extends to real counts in the same fractional relaxation. + +If V0 is the incumbent idle cost and +`q=(h(48)-h(3)-5*h(5))/20`, throughout this region + +`V(d)-V0 = x5 + (x6+x7+x8+x9)*q`. + +Outside it no packing attains that common-dual value. The value remains a +lower bound; the model itself may also be infeasible for extreme inventories. +This is not a claim that PR3862 asserted simultaneous exactness outside its +ranges. Its single-basis ranges and global lower bound remain valid. + +## Sharp axial ranges and integral controls + +Setting all other flows to zero gives maximal xj: + +| Move | PR3862 sufficient single-basis range | Complete tight-face range | +|---|---:|---:| +| 5 to 4 | 18 | 18 | +| 6 to 5 | 28 | 48 | +| 7 to 6 | 28 | 88/3 | +| 8 to 7 | 30 | 30 | +| 9 to 8 | 28 | 48 | + +Each upper endpoint is attained by a nonnegative rational packing in +`RESULT.json`; each is forced by one of the joint inequalities, so it is +sharp for this price. At T360 all five endpoint witnesses have integer +aggregate helper and bin counts. This checks integrality of the clock-free +aggregate only, not a chronological owner assignment or per-call matching. + +## An actual coupled counterexample and a strict gap + +Take x6=x7=28, all other flows zero. Each change lies within the old individual +range, but S=56 and y6=-2. Since row 6 of A^-1 is nonnegative on every tight +column, this separates the changed demand from the whole twelve-column face. +An explicit feasible packing nevertheless exists: in 28 original +`[6,8,9,9]@32` bins shrink the 6 to 5, and in 28 `[7,9]@16` bins shrink +the 7 to 6. Both new remainders are 1. The resulting rational pattern counts +and all ten conservation equations are checked exactly; T360 clears them. + +Let delta be the certified minimum strictly positive reduced cost and M the +maximum negative magnitude of row 6 on any of the 2,551 columns. The row sum +-2 forces at least 2/M units of non-tight patterns. Consequently every feasible +packing has idle cost at least `common_dual + 2*delta/M`, strictly above the +putative linear price. `RESULT.json` supplies exact delta, M and this gap. +Thus the rejection is an objective obstruction, not a failed packing search. + +## Limits + +Only widths 4..9, fixed bins, fixed exponent and the paid-remainder objective +are certified. No all-concave or all-exponent optimality is asserted. Actual +staging signatures, circuit identities, dirty restoration, stock, source +access, chronology, collision rules, native/recursive invoices and both +supplier caps require their own admission. No full multiplication theorem, +formal proof-kernel check, selected-frontier change or new kappa is claimed. diff --git a/research/staged544-terminal-extension-budget/frozen/PROFILE.json b/research/staged544-terminal-extension-budget/frozen/PROFILE.json new file mode 100644 index 0000000000..e49ce9e7cf --- /dev/null +++ b/research/staged544-terminal-extension-budget/frozen/PROFILE.json @@ -0,0 +1,9 @@ +{ + "1": 8041680, + "2": 2306880, + "3": 729648, + "4": 353160, + "5": 69120, + "8": 25920, + "48": 137952 +} \ No newline at end of file diff --git a/research/staged544-terminal-extension-budget/frozen/SOURCE-CREDITS.md b/research/staged544-terminal-extension-budget/frozen/SOURCE-CREDITS.md new file mode 100644 index 0000000000..c054fad87e --- /dev/null +++ b/research/staged544-terminal-extension-budget/frozen/SOURCE-CREDITS.md @@ -0,0 +1,14 @@ +# Source credit and independence + +New work: dataisfire with substantial OpenAI Codex assistance, Apache-2.0. No independent human review, fresh third-party AI review or proof-kernel verification is claimed. + +The construction extends [PR3682](https://github.com/CrocSwap/integer-mult-bounds/pull/3682), head431e6c6023ef352c41696469de7fb614cd4ded8c. Its retimed word, actual T360 source clock and immutable native/parent framework are retained. The complete new source/receipt snapshot is bound by REPLAY-INPUTS.json. The new ordinary source stage is an explicit pinned record applied after the unchanged predecessor reconstruction. + +- [PR3605](https://github.com/CrocSwap/integer-mult-bounds/pull/3605), Ross Richardson, supplies the staged-entrance mechanism, literal cleanup and exact Gaussian residual-check pattern. staged_pair.py is retained; the new544 shear and its proof are separate. +- [PR3638](https://github.com/CrocSwap/integer-mult-bounds/pull/3638), head d62e1acd7518a231440383f0d0dddf54d6edf8c1, supplies the T360 source-window clock, chronological aggregate model and integral-network/literal construction, with its retained PR3605 and earlier credits. The new inventory, integer incumbent and literal fill are recomputed. No predecessor owner receipt is used as proof of the new fill. +- [PR3687](https://github.com/CrocSwap/integer-mult-bounds/pull/3687) and [PR3693](https://github.com/CrocSwap/integer-mult-bounds/pull/3693), Sagar Thakrar and roger-sato with their credited AI assistance, supply audit_core.py and the whole-word semantics adapter audit_verify.py. These bytes are retained and reused. They are independent of the current constructor in the stated interpreter scope, not a newly written independent audit or new reviewer approval. +- The coupled-word source lineage includes PR3133, PR2979, Marius-Paul Dumitrean, dcharb78, Jeremy Kothe and the retained native/owner/block-norm/outer authors. All notices and scientific engines inside the source snapshot remain intact. + +owner_audit.py is a standalone standard-library adaptation of the source-window/family/prefix/invoice predicates in PR3638's independent_literal.py. It imports no producer, optimizer or retained owner checker. Its source template, plan and actual native canonical words are authenticated inputs. Three controls mutate actual literal roles and must fail for the intended reason. It shares the credited contract interpretation; it is not evidence of independent human agreement. + +The rational finite-price enclosure is retained from the PR3682 sources. New script adapters bind it to the actual finite histogram. Native forward/backward scalar replay, wrapper/phase lowering and all-column warp recipes were freshly run for both new words; unchanged native and parent ancestry is explicitly reused. The separate new544 span(414,51) residual check includes global Gaussian phase. diff --git a/research/staged544-terminal-extension-budget/frozen/WORD-base.json.gz b/research/staged544-terminal-extension-budget/frozen/WORD-base.json.gz new file mode 100644 index 0000000000..806784bf99 Binary files /dev/null and b/research/staged544-terminal-extension-budget/frozen/WORD-base.json.gz differ diff --git a/research/staged544-terminal-extension-budget/frozen/WORD-extra.json.gz b/research/staged544-terminal-extension-budget/frozen/WORD-extra.json.gz new file mode 100644 index 0000000000..c531be7383 Binary files /dev/null and b/research/staged544-terminal-extension-budget/frozen/WORD-extra.json.gz differ diff --git a/research/staged544-terminal-extension-budget/frozen/audit_core.py b/research/staged544-terminal-extension-budget/frozen/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/staged544-terminal-extension-budget/frozen/audit_core.py @@ -0,0 +1,480 @@ +"""Independent exact semantics and binary-frame bill for the BORROW-WORD format. + +Standard library only. Nothing is imported from the audited authors' code +(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word +format and its semantic contract were read from those pinned sources and are +credited there. The frame-bill and free-word structure (point-set spans, warp +frame and lifted-frame checks, target levels keyed by register, dual symbol +naming) re-implements, without importing, Arham Tahir's +research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its +reading of the contract, so this module is not independent of that audit. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q + +V, N, H = 112, 704, 9 # sources 0..111, targets 112..223, helpers 224..703 +DUAL = 10 ** 6 # offset naming the independent dual symbols D_k = K_k^(-T) + + +class AuditFailure(Exception): + """Explicit failure; never disabled by python -O.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(' '.join(map(str, why))) + + +def is_target(r): + return V <= r < 2 * V + + +def touched(g): + return g[1:3] if g[0] == 'add' else g[1:2] + + +# ---------------------------------------------------------------------------- +# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask +# (bit x set iff x lies in the subspace). Containment is mask inclusion. +# ---------------------------------------------------------------------------- +_SPAN = {} + + +def span(vectors): + key = tuple(vectors) + mask = _SPAN.get(key) + if mask is None: + points = {0} + for u in key: + need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u) + if u not in points: + points |= {p ^ u for p in points} + mask = sum(1 << p for p in points) + _SPAN[key] = mask + return mask + + +def points(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + size = bin(mask).count('1') + need(size and size & (size - 1) == 0, 'not a subspace point set') + return size.bit_length() - 1 + + +FULL = (1 << 512) - 1 +ZERO = 1 + + +def hyperplane(port): + return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0) + + +def warp_images(columns): + """Images of all 512 vectors under the F_2-linear map with columns G e_i.""" + need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns') + images = [0] * 512 + for x in range(1, 512): + low = x & -x + images[x] = images[x ^ low] ^ columns[low.bit_length() - 1] + need(len(set(images)) == 512, 'singular warp') + return images + + +def image_mask(images, mask): + return sum(1 << images[x] for x in points(mask)) + + +def lagrangian_action_ok(images, U, E): + """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves. + + L_U={(x,x+p): x in U, p in U^perp}. This is the binary frame action only; it + is not a Clifford phase or Gaussian-product certificate. For invertible G with + G(U)=E it is implied by the frame-map check ( = ), so it is a + consistency check of the implementation, not extra evidence. + """ + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + # G^{-T} z: bit j of the result is . + git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H)) + lift = lambda x, z: (images[x], images[x] ^ git(x ^ z)) + pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + lifted = [lift(*b) for b in basis] + if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)): + return False + + def frame(mask): + us = points(mask) + perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)] + return {(u, u ^ p) for u in us for p in perp} + return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E))) + + +# ---------------------------------------------------------------------------- +# Chronological binary-frame bill (BORROW-WORD contract) +# ---------------------------------------------------------------------------- +def frame_bill(w, lagrangian=False): + rep = w['report'] + need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry') + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers') + live = [r for r in range(N) if r not in removed] + liveset = set(live) + B, warps = w['B'], w['warps'] + for k, (pos, lender, cols, U, E) in enumerate(warps, 1): + need(0 <= pos <= len(B), 'warp position', k) + need(lender in liveset and not is_target(lender), 'warp lender', k) + images = warp_images(cols) + su, se = span(U), span(E) + need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k) + need(image_mask(images, su) == se, 'warp does not map its frame', k) + if lagrangian: + need(lagrangian_action_ok(images, su, se), 'lifted frame action', k) + for name in ('A', 'B', 'restore'): + for g in w[name]: + if g[0] != 'warp': + need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g) + if g[0] == 'add' and not is_target(g[1]): + need(not is_target(g[2]), 'non-target reads a target', name, g) + need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates') + need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes') + need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target') + + ports = w['ports'] + start, end = {}, {} + for r in live: + if r < V: + start[r], end[r] = span((ports[r],)), FULL + elif r < 2 * V: + start[r], end[r] = ZERO, hyperplane(ports[r - V]) + else: + start[r], end[r] = ZERO, FULL + for q, U in w['start_extra'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q) + start[int(q)] = span(U) + for q, U in w['helper_final'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q) + end[int(q)] = span(U) + + current, bill, chain = dict(start), Counter(), {} + + def climb(r, mask, where): + need(current[r] & ~mask == 0, 'frame containment fails', where, r) + d = dim(mask) - dim(current[r]) + if d: + bill[d] += 1 + chain.setdefault(r, []).append((where, d, mask)) + current[r] = mask + + npre = w['prelude_events'] + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < npre and len(g) == 5, 'warp outside the prelude', i) + _, r, op, fr, to = g + need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i) + images = warp_images(warps[abs(op) - 1][2]) + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + images = inverse + need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i) + need(current[r] == span(fr), 'prelude warp entry frame', i, r) + current[r] = span(to) + chain.setdefault(r, []).append((('A', i), 'warp', span(to))) + else: + if i < npre: + need(is_target(g[1]), 'prelude scalar writes a non-target', i) + for r in touched(g): + climb(r, span(g[-1]), ('A', i)) + levels = {V + int(t): span(U) for t, U in w['target_levels'].items()} + need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels') + for q, U in zip(w['centers'], w['center_frames']): + U = span(U) + need(current[q] == U, 'centre entry frame', q) + served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q} + for T in sorted(served, key=lambda m: -dim(m)): + need(T & ~U == 0, 'centre descent not nested', q) + d = dim(U) - dim(T) + if d: + bill[d] += 1 + chain.setdefault(q, []).append((('centre',), d, T)) + U = T + at = {} + for k, rec in enumerate(warps, 1): + at.setdefault(rec[0], []).append(k) + for p in range(len(B) + 1): + for k in at.get(p, ()): + _, lender, _, U, E = warps[k - 1] + need(current[lender] == span(U), 'native warp entry frame', k, lender) + current[lender] = span(E) + chain.setdefault(lender, []).append((('warp', k), 'warp', span(E))) + if p < len(B): + for r in touched(B[p]): + climb(r, span(B[p][-1]), ('B', p)) + for i, g in enumerate(w['restore']): + for r in touched(g): + climb(r, span(g[-1]), ('restore', i)) + for r in live: + climb(r, end[r], ('end',)) + restored = set(map(int, w['helper_final'])) + need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low') + widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end + + +def hygiene(w): + """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access.""" + entering = set(map(int, w['start_extra'])) + restored = set(map(int, w['helper_final'])) + live = set(range(N)) - set(w['removed']) + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + for g in w[name]: + if g[0] == 'warp': + continue + q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g) + if g[0] == 'scale': + need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g) + for g in w['precondition'] + w['compensation']: + need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g) + for c in w['initial_corrections']: + word = c['operator_word'] + need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V + and c['source'] not in entering, 'correction access', c) + need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c) + q = Q(c['coefficient']) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c) + return True + + +# ---------------------------------------------------------------------------- +# Literal inverse cleanup, derived from the contract +# ---------------------------------------------------------------------------- +def ordinary_forward(w): + """Chronological non-wrapper actions whose inverse forms cleanup.""" + out = [g for g in w['A'][w['prelude_events']:]] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + out += at.get(p, []) + if p < len(w['B']): + out.append(w['B'][p]) + return out + list(w['restore']) + + +def derive_cleanup(w): + restored = set(map(int, w['helper_final'])) + buf = lambda r: r + N if r in restored else r + full = [256, 128, 64, 32, 16, 8, 4, 2, 1] + out = [] + for g in reversed(ordinary_forward(w)): + if g[0] == 'warp': + out.append(['warp', buf(g[1]), -g[2], full]) + elif is_target(g[1]): + continue + elif g[0] == 'add': + out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full]) + else: + need(g[0] == 'scale', 'unknown primitive', g) + out.append(['scale', buf(g[1]), g[3], g[2], full]) + return out + + +def same_cleanup(a, b): + norm = lambda c: [(g[:-1], span(g[-1])) for g in c] + return len(a) == len(b) and norm(a) == norm(b) + + +# ---------------------------------------------------------------------------- +# Exact free-operator semantics. A value is a dict {(input, word): Fraction}; +# word is a reduced tuple of signed operator ids (leftmost = applied last). +# ---------------------------------------------------------------------------- +def program(w, cleanup=None): + """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup.""" + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + items += at.get(p, []) + if p < len(w['B']): + items.append(w['B'][p]) + items += w['restore'] + return items, list(w['cleanup'] if cleanup is None else cleanup) + + +def dual_op(op): + return (1 if op > 0 else -1) * (abs(op) + DUAL) + + +def _left(op, word): + return word[1:] if word and word[0] == -op else (op,) + word + + +def _right(word, op): + return word[:-1] if word and word[-1] == -op else word + (op,) + + +def _axpy(dst, src, q): + for key, x in src.items(): + y = dst.get(key, 0) + q * x + if y: + dst[key] = y + else: + dst.pop(key, None) + + +def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None): + """Schrodinger pass: every register's value as a combination of initial inputs. + + Live inputs are independent symbols. Private buffers are independent symbols + when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot + callback sees the rows at the cleanup boundary. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live} + for c in restored: + rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {} + prefix, tail = program(w, cleanup) + + def apply(g): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + if dual: + t, s, q = s, t, -q + _axpy(rows[t], rows[s], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + if dual: + q = 1 / q + rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()} + elif kind == 'warp': + op = dual_op(g[2]) if dual else g[2] + rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + if dual: + src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c + else: + src, ops, dst = rows[s], list(reversed(word)), t + moved = {} + for (var, wd), x in src.items(): + for o in ops: + wd = _left(o, wd) + moved[var, wd] = x + _axpy(rows[dst], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + + for g in prefix: + apply(g) + if snapshot is not None: + snapshot(rows) + for g in tail: + apply(g) + return rows + + +def reverse_columns(w, cleanup=None, upto_cleanup=False): + """Heisenberg pull-back: process the forward program backwards. + + cols[s] = {(output, word): coefficient}: the final output register 'output' + contains coefficient*word*x_s. Words grow on the right. Every live input and + every private buffer is an independent symbol. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + regs = live + [c + N for c in restored] + cols = {r: {(r, ()): Q(1)} for r in regs} + prefix, tail = program(w, cleanup) + seq = prefix if upto_cleanup else prefix + tail + for g in reversed(seq): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + _axpy(cols[s], cols[t], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()} + elif kind == 'warp': + op = g[2] + cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + moved = {} + for (out, wd), x in cols[t].items(): + for o in word: + wd = _right(wd, o) + moved[out, wd] = x + _axpy(cols[s], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + return cols + + +def transpose(cols): + rows = {} + for s, col in cols.items(): + for (r, word), x in col.items(): + rows.setdefault(r, {})[s, word] = x + return rows + + +def endpoint_defects(w, rows, dual=False): + """Compare final rows with the contract on the zero-buffer (live-input) domain. + + Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity). + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + bad = [] + for r in live: + expect = {(r, ()): Q(1)} + if dual and r < V: + expect[r + V, ()] = Q(-1) + if not dual and is_target(r): + expect[r - V, ()] = Q(1) + got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N} + if got != expect: + bad.append(r) + dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))] + leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N}) + buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)} + for c in restored) + return bad, dirty, leaks, buffer_identity + + +def boundary_defects(w, rows): + """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated.""" + restored = set(map(int, w['helper_final'])) + out = [] + for t in range(V, 2 * V): + if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}: + out.append(('target', t)) + for c in restored: + if rows[c] != {(c, ()): Q(1)}: + out.append(('restored', c)) + for r, row in rows.items(): + if r < N and r not in restored and any(k[0] in restored for k in row): + out.append(('restored input read', r)) + return out diff --git a/research/staged544-terminal-extension-budget/refund_corollary.py b/research/staged544-terminal-extension-budget/refund_corollary.py new file mode 100644 index 0000000000..678d32b7e3 --- /dev/null +++ b/research/staged544-terminal-extension-budget/refund_corollary.py @@ -0,0 +1,43 @@ +"""Optional bounded pivot: terminal rank-one refunds cannot finance extensions. +Reuses verify's exact interval arithmetic; not a second independent implementation. +""" +from collections import Counter +from fractions import Fraction as Q +import json +import verify as v + +def check(): + q,pi,mu=v.dual();pi[4]=v.add((1,v.h(1)),(-1,v.h(5)));tight=0;strict=[] + for cap in (8,16,32,48): + def rec(w,ns,left): + if w==10: + yield tuple(ns),left;return + for n in range(left//w+1):yield from rec(w+1,ns+[n],left-w*n) + for ns,left in rec(4,[],cap): + row=v.add((1,v.h(left)),(-1,mu[cap]),*((-n,pi[w]) for w,n in zip(range(4,10),ns))) + if not row:tight+=1 + else: + ab=v.interval(row);v.need(ab[0]>0,'width4 dual infeasibility');strict.append(ab) + v.need(not v.add((1,pi[4]),(-1,pi[5]),(-1,v.h(1))),'refund exact idle price') + audit=v.audit_module();sources={} + for tag in ('base','extra'): + w=v.read(v.ROOT/f'frozen/WORD-{tag}.json.gz');bill,inventory,chain,start,end=audit.frame_bill(w) + lower=[];fixed=0 + for key in w['helper_final']: + r=int(key);charge=chain[r][-1][1];width=audit.dim(end[r])-audit.dim(start[r]) + if charge: + v.need(charge==1 and width==5,'other protected terminal refund exists') + # The previous exact frame is the unique dimension-lowering endpoint. + previous=chain[r][-2][2] if len(chain[r])>=2 else start[r] + v.need(previous & ~end[r]==0 and audit.dim(previous)==audit.dim(end[r])-1,'refund subspace') + lower.append(r) + else:fixed+=1 + v.need(len(lower)==17 and fixed==74,'refund domain') + sources[tag]={'refundable_registers':sorted(lower),'protected_without_refund':fixed} + return {'status':'PASS_REFUND_EXTENDED_BUDGET','patterns':tight+len(strict),'symbolic_tight':tight,'strict':len(strict), + 'minimum_positive_reduced_cost':v.brief((min(x[0] for x in strict),min(x[1] for x in strict))), + 'refund_idle_price_minus_terminal_saving':'0 exactly','providers':sources, + 'conclusion':'Any subset of these rank1 refunds ties at best under arbitrary repacking; combining them with positive terminal-only extensions still loses more than the main theorem gap times total added dimensions. Interior changes excluded.'} +def main(): + r=check();expected=v.read(v.ROOT/'REFUND-RESULT.json');v.need(r==expected,'refund result mismatch');print(json.dumps({'status':r['status'],'patterns':r['patterns'],'refundable_per_provider':17},sort_keys=True)) +if __name__=='__main__':main() diff --git a/research/staged544-terminal-extension-budget/verify.py b/research/staged544-terminal-extension-budget/verify.py new file mode 100644 index 0000000000..ed0cf43186 --- /dev/null +++ b/research/staged544-terminal-extension-budget/verify.py @@ -0,0 +1,160 @@ +"""Exact terminal-only extension budget; Chris R with OpenAI Codex, Apache-2.0. +The dual is credited to PR3815/3862/3890. No optimizer is used here. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path +import argparse, gzip, hashlib, importlib.util, json, math +ROOT=Path(__file__).resolve().parent +K=Q(1730663236534549309146,10**24) + +def need(ok,why): + if not ok: raise ValueError(why) +def read(p): + b=p.read_bytes();return json.loads(gzip.decompress(b) if p.suffix=='.gz' else b) +def sha(p):return hashlib.sha256(p.read_bytes()).hexdigest() +def add(*terms): + out=Counter() + for factor,v in terms: + for r,c in v.items():out[r]+=factor*c + return {r:c for r,c in out.items() if c and r} +def h(r):return {r:Q(1)} if r else {} +def log_ratio(x): + z=(x-1)/(x+1);n=50 + value=2*sum((z**(2*j+1)/Q(2*j+1) for j in range(n)),Q(0)) + tail=2*z**(2*n+1)/(Q(2*n+1)*(1-z*z)) + return value,value+tail +@lru_cache(None) +def power(r): + if r==0:return Q(0),Q(0) + j=r.bit_length()-1;l2,u2=log_ratio(Q(2));lr,ur=log_ratio(Q(r,2**j)) + a,b=K*(j*l2+lr),K*(j*u2+ur) + need(0<=a<=b<1,'exponential range') + def exp_minus(x,n):return sum(((-x)**i/Q(math.factorial(i)) for i in range(n+1)),Q(0)) + return r*exp_minus(b,19),r*exp_minus(a,20) +def interval(v): + lo=hi=Q(0) + for r,c in v.items(): + a,b=power(r);lo+=c*(a if c>=0 else b);hi+=c*(b if c>=0 else a) + return lo,hi +def brief(ab): + scale=10**24;lo,hi=ab + return {'lower_numerator':lo.numerator*scale//lo.denominator,'upper_numerator':-((-hi.numerator*scale)//hi.denominator),'denominator':scale} +def patterns(): + for cap in (8,16,32,48): + def rec(i,ns,left): + if i==5: + yield cap,tuple(ns),left;return + for n in range(left//(i+5)+1):yield from rec(i+1,ns+[n],left-n*(i+5)) + yield from rec(0,[],cap) +def dual(): + q={48:Q(1,20),3:Q(-1,20),5:Q(-1,4)} + pi={w:add((-1,h(5)),(-(w-5),q)) for w in range(5,10)} + mu={8:add((-1,pi[8])),16:add((-2,pi[8])),32:add((-4,pi[8])),48:h(48)} + return q,pi,mu +def reduced(cap,ns,left,pi,mu):return add((1,h(left)),(-1,mu[cap]),*((-n,pi[w]) for w,n in zip(range(5,10),ns))) +def dual_check(): + q,pi,mu=dual();tight=[];strict=[] + for cap,ns,left in patterns(): + v=reduced(cap,ns,left,pi,mu) + if not v:tight.append([cap,list(ns),left]) + else: + ab=interval(v);need(ab[0]>0,'dual infeasibility');strict.append(ab) + gap=interval(add((1,h(9)),(-1,h(8)),(-1,q)));need(gap[0]>Q(6,1000),'terminal budget gap') + # Independently test every discrete marginal, not only the analytic minimum. + for r in range(1,10):need(interval(add((1,h(r)),(-1,h(r-1)),(-1,q)))[0]>0,'marginal budget') + return {'patterns':len(tight)+len(strict),'tight_patterns':tight,'strict_patterns':len(strict), + 'minimum_strict_reduced_cost':brief((min(x[0] for x in strict),min(x[1] for x in strict))), + 'idle_credit_per_dimension':brief(interval(q)), + 'minimum_terminal_charge_per_dimension':brief(interval(add((1,h(9)),(-1,h(8))))), + 'mandatory_interior_saving_per_dimension':brief(gap)} +def audit_module(): + spec=importlib.util.spec_from_file_location('credited_audit',ROOT/'frozen/audit_core.py');m=importlib.util.module_from_spec(spec);spec.loader.exec_module(m);return m + +def local(): + audit=audit_module();out={};width_vectors={} + for tag in ('base','extra'): + w=read(ROOT/f'frozen/WORD-{tag}.json.gz');bill,inventory,chain,start,end=audit.frame_bill(w,lagrangian=True) + regs=sorted(r for r in end if r>=224);widths=[audit.dim(end[r])-audit.dim(start[r]) for r in regs] + need(inventory=={5:28,6:18,7:53,8:96,9:213},'inventory');need(bill=={1:2482,2:712,3:218,4:109,5:20,8:8},'local bill') + need(all(0<=chain[r][-1][1]<=9 for r in regs),'terminal climb') + need(all(end[r]==audit.FULL for r in regs if widths[regs.index(r)]==9),'width9 is full terminal') + width_vectors[tag]=widths + out[tag]={'local_profile':bill,'inventory':inventory,'registers':regs,'widths':widths, + 'terminal_dimensions':[audit.dim(end[r]) for r in regs], + 'terminal_climb_histogram':dict(sorted(Counter(chain[r][-1][1] for r in regs).items())), + 'frozen_word_sha256':sha(ROOT/f'frozen/WORD-{tag}.json.gz')} + need(width_vectors['base']==width_vectors['extra'],'provider role widths differ');need(out['base']['terminal_dimensions']==out['extra']['terminal_dimensions'],'provider terminal dimensions differ') + return out + +def owner_math(local_results): + receipt=read(ROOT/'OWNER-PATTERNS.json');q,pi,mu=dual();bins=Counter();demand=Counter();idle=Counter();total=0 + for row in receipt['patterns']: + cap,ns,left,n=row;need(type(n)is int and n>0,'pattern multiplicity') + need(sum(w*k for w,k in zip(range(5,10),ns))+left==cap,'pattern capacity') + need(not reduced(cap,ns,left,pi,mu),'incumbent not dual-tight') + bins[cap]+=n;total+=n + for w,k in zip(range(5,10),ns):demand[w]+=n*k + if left:idle[left]+=n + # Fixed identity theorem: slack implies every occupied role has width9. + need(left==0 or all(k==0 for k in ns[:4]),'extensible role has slack') + need(dict(bins)=={8:241920,16:161280,32:161280,48:161280},'complete bin counts') + need(dict(demand)=={5:90720,6:58320,7:171720,8:311040,9:690120},'complete demands') + complete=Counter({int(r):n for r,n in read(ROOT/'frozen/PROFILE.json').items()}) + lb=local_results['base']['local_profile'];derived=Counter(idle) + for r,n in lb.items():derived[r]+=3240*n + need(derived==complete,'complete local-plus-idle profile') + return {'calls':3240,'roles':sum(demand.values()),'bins':total,'occupied_bins':total-idle[48], + 'idle_profile':dict(sorted(idle.items())),'complete_profile':dict(sorted(derived.items())), + 'fixed_identity_feasible_nonnegative_extensions':0,'all_actual_patterns_dual_tight':True} + +def full_owner(source_root,local_results): + pins=read(ROOT/'EXTERNAL-SOURCES.json')['files'] + for rel,digest in pins.items():need(sha(source_root/rel)==digest,'external source hash '+rel) + fill=read(source_root/'FILL.json.gz');template=read(source_root/'inputs/TEMPLATE.json.gz') + caps={r['child']:r['rank'] for r in template['idle_children']};width=local_results['base']['widths'];dims=local_results['base']['terminal_dimensions'] + used=Counter();groups={};headroom=Counter();rows=fill['rows'] + need(len(rows)==3240*408 and fill['columns']==['time','helper','owner_replica','child','port','offset'],'literal role count') + for i,row in enumerate(rows): + need(len(row)==6 and all(type(x)is int for x in row),'literal row') + t,h,o,c,p,z=row;need((t,h)==divmod(i,408),'literal role indexing');need(0<=o<360 and c in caps and 0<=p<112,'literal bin identity') + key=o,c,p;need(z==used[key] and z+width[h]<=caps[c],'literal prefix capacity') + used[key]+=width[h];groups.setdefault(key,Counter())[width[h]]+=1 + headroom[key]+=9-dims[h] + hist=Counter();slack_headroom=0 + for o in range(360): + for c,cap in sorted(caps.items()): + for p in range(112): + key=o,c,p;left=cap-used[key];ns=groups.get(key,{}) + need(left==0 or headroom[key]==0,'actual joint rank/capacity obstruction') + hist[cap,tuple(ns.get(w,0) for w in range(5,10)),left]+=1 + derived=[[cap,list(ns),left,n] for (cap,ns,left),n in sorted(hist.items())] + need(derived==read(ROOT/'OWNER-PATTERNS.json')['patterns'],'actual owner pattern certificate') + return {'status':'PASS_ALL_LITERAL_OWNER_ROWS','roles':len(rows),'bins':sum(hist.values()),'source_hashes':pins} + +def controls(): + q,pi,mu=dual();mut_mu=dict(mu);mut_mu[8]=add((1,mu[8]),(Q(1,1000),h(1))) + need(interval(reduced(8,(0,0,0,1,0),0,pi,mut_mu))[1]<0,'perturbed dual rejected') + # Positive fixture: merge one added dimension into rank1 while absorbing rank1 idle. + need(interval(add((1,h(2)),(-2,h(1))))[1]<0,'rank1-gap absorption positive fixture') + # Failure: terminal-only dimension charge cannot be dropped as zero. + need(interval(add((-1,q)))[1]<0,'omitted-local-bill mutant would fake gain') + # Failure: changing source rank capacity from32 to33 would create false room. + need(sum((5,9,9,9))==32 and 33-sum((5,9,9,9))==1,'capacity mutation discriminates') + # Exact small rank-function example: noncoordinate extension still costs dimension. + span=lambda vs:__import__('functools').reduce(lambda S,v:S|{x^v for x in S},vs,{0}) + U=span([3,5]);E=span([3,5,8]);need(U