Certify a complete tariff barrier for staged544 terminal-only extensions

research/staged544-terminal-extension-budget/.gitattributes

@@ -0,0 +1 @@
+* -text

research/staged544-terminal-extension-budget/.gitignore

@@ -0,0 +1,2 @@
+__pycache__/
+*.pyc

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"
+  }
+}

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"
+}

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."
+}

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
+    ]
+  ]
+}

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<s<1, h is
+concave and its discrete increments decrease. For0<=r<r+d<=9,
+
+    h(r+d)-h(r) >= 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.