Conditional κ = 0.001673619538656538 from a verified two-role T16 swap

research/t16-two-role-moment-swap/PROOF.md

@@ -0,0 +1,139 @@
+# Two-role construction, strict gain and scope
+
+## The literal change
+
+In PR3308's authenticated owner map, row 1514 is width 4, helper 74,
+call `(stage=0, replica=9, time=3)`, hosted in bin `(9,6,50)`.
+Row 1863 is width 5, helper 423, the same call, hosted in bin `(0,2,33)`.
+The first bin has capacity 32 and free rank 1. The second has capacity 16
+and free rank 2. Exchange their entire physical placements and compact each
+bin's occupied prefix in stable old-offset order. `exchange()` preserves
+stage, replica, time, helper and width for every row. Six rows differ, only
+two of them in their hosting placement.
+
+The resulting free ranks are 0 and 3. Actual source-event windows, active-pair
+exclusion, one-helper-per-family-per-call, disjoint slices and prefix occupancy
+are checked on all 69,120 roles by the retained source auditor and independently
+by unchanged strict T16 admission. The actual chart count is derived as 10,008.
+There is no assumed zero-cost new gate, source read, restoration or adapter.
+This invokes exactly the inherited whole-helper hosting contract.
+
+## Strict moment improvement
+
+Let `p` lie strictly between zero and one. For positive `x,y`, strict
+concavity of `t^p`, with its continuous value zero at zero, gives
+`(x+y)^p < x^p+y^p`. Apply this with `x=1,y=2`. The replaced recursive
+contribution is therefore strictly smaller:
+
+```text
+(3/73)^p + (0/73)^p < (2/73)^p + (1/73)^p.
+```
+
+Every other recursive child and paid charge is unchanged. Both moments retain
+the same normalizing role count. This proves a strict complete complex moment
+decrease without using a floating-point surrogate. It does not by itself give
+the final headline; the exact supplier endpoints and outer witness do that.
+
+For completeness of the bounded census, orient a swap so its first role has
+width `wa > wb` and put `d=wa-wb`. If the original free ranks are `fa,fb`,
+the new pair is `fa+d,fb-d`; feasibility requires `fb>=d`. Equal pair sums
+and strict concavity show strict improvement exactly when `fa+d>fb`.
+A full first bin has `fa=0` and cannot meet both conditions. Empty bins have
+no role to exchange. Thus only occupied partial bins need be enumerated.
+The implementation checks all such width/free-rank pairs, then every row pair
+of different physical capacities, and tests the actual chronological and family
+constraints. Equal-width swaps cannot change the paid profile. The 19,372
+candidate pairs include eight legal choices. This proves only that named
+finite domain on PR3308's map, not optimality among arbitrary owner maps.
+
+## Full paid ledger
+
+The actual eleven-stage replay, not the two-bin argument, supplies construction
+admission. It checks 144 complete invocations and 69,120 helpers, native provider
+content bindings, owners, parent lift, emitted controller, physical/prefix
+invoice, both exact moment engines, both seven-step bootstraps and all 47
+strict outer inequalities on each tariff path. The controls remain
+69 admission, 12 bit, 6 independent T16 and 15 controller mutations.
+The separately authored owner auditor adds its 11 controls.
+
+The complete selected invoice object must match, including unknown future keys,
+after excluding only `template_sha256`, `owner_audit_sha256` and
+`controller_audit_sha256`. Those three identifiers bind the newly emitted
+artifacts. Prefix 397 is paid at 512. The row coefficient stays 16,469 below
+20,161. Actual physical stock stays 14,826 = 14,336 data/owner families + 480
+helpers + 8 private centres + 2 coefficient fields. The independent T16
+receipt's 14,850 is its conservative 504-helper allowance, not a conflicting
+actual stock count. Copy, cleanup, restoration, compiler and coefficient charges
+are retained in the whole-object comparison, never inferred from this short list.
+
+The exact native complex endpoint is
+`419106309171938950571/250000000000000000000000`.
+The unchanged bit endpoint is
+`1733427039589844234749/1000000000000000000000000`.
+The complex side binds. The retained outer construction gives
+`κ=836809769328269/500000000000000000`, strictly exceeding both selected
+PR1094 and PR3308. The conservative complex surcharge control also improves.
+`RESULT.json` records their exact differences and cap comparisons.
+
+## Exact transport of generated receipt hashes
+
+The hosted arithmetic report exposed two changed raw references: the full invoice
+SHA256 and the dependent assembly SHA256. Every arithmetic report value and the
+other five input hashes matched. Arithmetic success alone did not admit those
+changed references. The original failing reports and immutable v3 evidence stay
+unchanged. Actual hosted witnesses from run `39075529422` then proved that the
+entire typed invoice object is identical. The literal byte difference is only
+the ordering of ten `providers.gauge44.artifacts` mapping entries. The dependent
+assembly differs only at its raw invoice reference. No gzip or decimal
+portability assumption is used.
+
+`transport.attest()` permits a serialization difference only after the ENTIRE
+actual invoice equals the frozen invoice as typed canonical JSON, with no omitted
+keys or values and with array order retained. Actual owner and controller bytes
+must remain exactly fixed and match their declared live hashes. The ENTIRE actual
+assembly must then equal the frozen assembly after replacing only
+`input_sha256.fresh_invoice` by the independently recomputed actual invoice SHA256.
+Every cost, cap, inequality, control, scope string and other input hash remains.
+
+Only after these whole-input checks may the expected score rebind its two named
+raw references. The construction report can rebind only its assembly/invoice
+artifact references. The fresh immutable invoice reviewer runs on the actual
+fresh score and copied scorer source. Its expected report rebinds only its two
+top-level raw references and the three corresponding score-binding references.
+The fresh reports still have to match those explicitly derived expected bytes.
+No generic hash ignore or arbitrary hash replacement exists.
+
+The registered run emits lossless bounded actual invoice, assembly, owner and
+controller witnesses plus `TRANSPORT.json`. Unknown keys, changed charges or
+inequalities, type changes, unrelated hashes, forged bindings and bad score or
+review fields reject in normal and optimized tests. This is an integration
+transport rule, not a new scientific supplier premise.
+
+## Inherited obligations and engineering limits
+
+The selected conditional scope remains intact. Source-bound reuse of selected
+native artifacts is not a fresh full cold rebuild. All-size/compiler,
+common-label/mutable-source realization, whole-call hosting, precision/tape,
+exact recovery, analytic transfer and bit H1-H5 assumptions remain inherited.
+No selected-frontier update, unconditional theorem or Lean proof is asserted.
+
+The new Python loops have fixed role, source, archive and pair-count bounds.
+Pair exhaustion fails closed; it cannot become an incomplete census success.
+Input and decompressed JSON sizes are bounded. The full unchanged admission
+subprocess has a 300-second timeout. Checks use exceptions and survive Python
+optimization, except the unchanged strict predecessor intentionally requires
+assertions enabled. Tests run the new construction controls in both modes.
+
+Power-of-Ten deviations are limited to Python's managed allocation, the fixed
+source-authenticated module loader, and unittest's bounded test dispatch. Their
+live inputs are bounded; the loaders have fixed canonical paths checked before
+execution. The retained predecessor modules are byte-identical and retain their
+existing internal allocation and loop structure. Rewriting those frozen proofs
+would expand the task and invalidate their evidence. Follow-up changes to those
+modules need separate replay and repinning; this package does not weaken them.
+The immutable v3 scorer also retains one unused `sys` import, reported by Ruff
+F401. Its source must stay byte-identical to the independently checked digest,
+so this nonbehavioral warning is recorded rather than hidden or silently edited.
+All new integration/construction code passes the repository Ruff checks. The
+scorer's next independently versioned release can remove that import and rerun
+its source-bound reports; no such optional source churn is part of this freeze.

research/t16-two-role-moment-swap/README.md

@@ -0,0 +1,119 @@
+# A two-role T16 packing improvement
+
+The unchanged selected PR1094 word admits conditional finite saving
+`κ = 836809769328269/500000000000000000 = 0.001673619538656538`.
+This is `1.047761522e-9` above PR3308's published predecessor and
+`9.5934157962e-7` above the selected record. The selected manifest is unchanged.
+This is a packing improvement, not a new multiplication theorem or packing optimum.
+
+Two whole helpers exchange capacity-16 and capacity-32 bins in the same call.
+Their idle remainders change from `(2,1)` to `(3,0)`. Strict concavity proves
+that this reduces the complex recursive moment for every exponent between zero
+and one. The actual scalar word, 480 helper widths, 144-call order and both
+suppliers stay fixed. See [the proof and full obligations](PROOF.md).
+
+## Construction and exact evidence
+
+The source is canonical main `463113d675af7410ac91d53a4fed51ec6494eb9a`,
+priority revision 6. PR3308 head
+`8bc0555b484bf4aec4b91c680763d930d6754974` is a published, unreviewed
+source-archived predecessor, not the selected frontier. Its merge is not scientific
+admission. Its complete map is reconstructed from
+canonical `complex-t16-two-stage-cycles` data and its original 163-row delta.
+Those exact delta bytes, original README and source hashes are retained under
+`predecessor/` and `SOURCE-EXPORT.json`. No unmerged Git object is required.
+
+`swap.py` exchanges role indices 1863 and 1514, then compacts their two bins.
+Exactly two roles relocate and four more offsets change. The complete census
+on the predecessor checks all 19,372 moment-improving different-capacity
+role pairs. Eight are legal and give the same profile. The lexicographically
+last pair is the committed witness. This is a complete two-role census on that
+fixed map, not a global search or a random-seed result. Worker 2's separate
+capacity-48 evacuation search does not produce this witness.
+
+The complete paid profile is
+`{1:349719,2:60199,3:62319,4:20448,5:11808,7:2,8:1152,16:2,48:4880}`.
+Rank mass is 1,041,408 and deficit 5,120. `RESULT.json` records the exact
+native and conservative prices, actual 10,008 charts, full source/data hashes,
+11 independent owner controls and strict controls 69/12/6/15. The replay
+compares every selected invoice field, except three freshly rebound source hashes.
+
+The fixed-word relaxation gives
+`a_hi = 1690054109089/10^15` and
+`κ < 1690054109089/1001690054109089`.
+This witness realizes about 99.1949333% of that kappa cap. The cap is not an
+attainable-packing certificate. The unchanged bit endpoint is about 0.001733427;
+the complex side still binds.
+
+## Reproduce
+
+Standard-library CPython 3.12, from the repository root:
+
+```sh
+python3.12 -Werror -B scripts/research_package.py --package research/t16-two-role-moment-swap
+# Keep all generated output in one fresh directory when diagnosing a failure:
+python3.12 -Werror -B research/t16-two-role-moment-swap/verify.py --work /absolute/fresh/output
+```
+
+The registered replay reconstructs the map and PLAN/SPEC, runs the unchanged
+179-file PR1087 eleven-stage strict admission, checks source-bound selected
+native artifacts, recomputes both supplier prices and the packing cap, and
+compares the full invoice. The same replay also runs the three independent
+source-closed checks retained under `support/`: code-disjoint exact arithmetic,
+strict construction admission, and full-invoice/proof-scope continuity. All bind
+the identical OWNERS/PLAN/SPEC and actual ASSEMBLY/invoice hashes. The numerical
+bundle is explicit immutable version 3. Generated raw invoice hashes may be
+rebound only after complete typed JSON equality of the actual invoice and the
+entire assembly with its single named invoice reference. All other fields and
+fixed input hashes remain checked. Exact fresh score/reviewer bytes must then
+match the explicitly source-rebound expected reports. Actual raw witnesses and
+the closed hash-graph proof are printed for hosted review. See PROOF.md.
+Ten construction behavioral groups run
+normally and optimized; the independent scorer adds eleven groups, construction
+admission six rejection controls, and invoice review thirteen rejection controls.
+Two additional diagnostic groups preserve exact failing reports and raw inputs.
+Nine normal/optimized transport groups reject changed costs, keys, types,
+cap/inequality fields, unrelated hashes, forged bindings and bad reports.
+Their faults include one-sided moves, wrong roles, stale profiles, malformed
+inputs, predecessor corruption and exhausted census budgets. No solver is needed.
+
+Local checks used Linux x86_64 and CPython 3.12.15. A Git-free export containing
+only this package and its declared canonical inputs passes the same direct
+replay. Final hosted evidence is reported in the PR and session handoff, not
+inferred from these local checks.
+
+## Scope and remaining premises
+
+The result has the selected conditional finite-construction scope. Native local
+ancestry is reused by exact source binding, not rebuilt cold. All-size/compiler,
+common-label/mutable-source realization, whole-call hosting, precision/tape,
+exact recovery, analytic transfer and bit H1-H5 assumptions remain. No formal
+kernel or independent human review is claimed. A passed CI run checks the
+executed artifact, not those inherited universal premises.
+
+## Credit
+
+Gonzalo Mier's PR3308 map and incremental packing retain their original credit.
+Philippe Van Velzen's reviewed PR2169 supplies the canonical two-stage-cycle map
+and reconstruction/replay lineage. Rohan Arun and Jeremy Kothe supply the
+PR1050-1094 owner-packing lineage; Hao Yan supplies the T16 controller.
+Josie Elliston supplies the independent owner auditor. Sagar Thakrar supplies
+prior independent pricing work. The archived compiler, native, bit and exact
+moment sources retain all original notices. This contribution adds the literal
+two-role swap, complete deterministic swap census, proof, source-closed replay
+and failure controls. The separately scoped supporting checks retain their exact
+source manifests and attribution. New material by Nick Petalas, Apache-2.0.
+
+The prepublication refresh fetched canonical main
+`6f100d4bb5083f8c35d96fd95a539811c62f245c` at 2026-10-17 22:07 UTC.
+Selected result and priority revision stayed unchanged. All 43 live input blobs
+are identical to the frozen scientific base. The changed guidance concerns P104,
+not this packing. No global-best claim is made over unadmitted public scores.
+
+## Open next questions
+
+Can a legal exchange involving at least three occupied bins improve this new
+map without adding a physical charge? First derive its exact residual change,
+then replay one explicit cycle through the full invoice. Capacity/window and
+same-call family constraints are the blockers. The census here does not exclude
+such cycles. See the structured question in `TASK.json`.

research/t16-two-role-moment-swap/RESULT.json

@@ -0,0 +1,98 @@
+{
+  "status": "PASS_T16_TWO_ROLE_MOMENT_SWAP",
+  "kappa": "836809769328269/500000000000000000",
+  "kappa_decimal": "0.001673619538656538",
+  "complex_lower": "419106309171938950571/250000000000000000000000",
+  "bit_lower": "1733427039589844234749/1000000000000000000000000",
+  "gain_vs_selected": "47967078981/50000000000000000",
+  "gain_vs_pr3308": "523880761/500000000000000000",
+  "conservative_kappa": "1673619535803731/1000000000000000000",
+  "profile": {
+    "1": 349719,
+    "2": 60199,
+    "3": 62319,
+    "4": 20448,
+    "5": 11808,
+    "7": 2,
+    "8": 1152,
+    "16": 2,
+    "48": 4880
+  },
+  "idle": {
+    "1": 2391,
+    "2": 7,
+    "3": 111,
+    "7": 2,
+    "16": 2,
+    "48": 4880
+  },
+  "census": {
+    "counts": {
+      "family": 72,
+      "legal": 8,
+      "moment_improving_pairs": 19372,
+      "type_pairs": 3,
+      "window": 19292
+    },
+    "winners": [
+      [
+        1811,
+        1514
+      ],
+      [
+        1813,
+        1514
+      ],
+      [
+        1814,
+        1514
+      ],
+      [
+        1815,
+        1514
+      ],
+      [
+        1859,
+        1514
+      ],
+      [
+        1861,
+        1514
+      ],
+      [
+        1862,
+        1514
+      ],
+      [
+        1863,
+        1514
+      ]
+    ]
+  },
+  "roles": 69120,
+  "rank_mass": 1041408,
+  "deficit": 5120,
+  "independent_controls": 11,
+  "strict_controls": {
+    "admission": 69,
+    "bit_supplier": 12,
+    "independent_t16": 6,
+    "controller_mutations": 15
+  },
+  "actual_charts": 10008,
+  "complete_invoice_unchanged": true,
+  "prefix_bits": 397,
+  "row_coefficient": 16469,
+  "packing_a_bracket": [
+    "52814190909/31250000000000",
+    "1690054109089/1000000000000000"
+  ],
+  "packing_kappa_cap": "1690054109089/1001690054109089",
+  "fraction_of_kappa_cap": "838224023117448059262777536941/845027054544500000000000000000",
+  "source_overlay": {
+    "OWNERS.json.gz": "abb13ccd2b1f408ec6d7b759b7acd6a40a5000890ab12ae3cdf6aa973d8b8b29",
+    "PLAN.json": "670771c298200331e236575b4fcf748957875f441993b64701bd62bc4470b540",
+    "SPEC.json": "a1b553b5c144ea5faf0fcce37a4216a3d4715c0532ebce2efdc73b7c8c80756c"
+  },
+  "scope": "Conditional finite selected-word T16 admission with source-bound native ancestry reuse; inherited selected assumptions remain."
+}

research/t16-two-role-moment-swap/SOURCE-EXPORT.json

@@ -0,0 +1,27 @@
+{
+  "source_pr": 3308,
+  "source_head": "8bc0555b484bf4aec4b91c680763d930d6754974",
+  "files": [
+    {
+      "path": "predecessor/DIFF-vs-predecessor.json",
+      "source_path": "research/complex-t16-evacuation-increment/DIFF-vs-predecessor.json",
+      "git_blob": "deef1cbefab126eb87f9b078fe129ac5fa00fcf8",
+      "sha256": "83bae3bfbc6dda81c5b609833042943c6c31dfe51e48661a77834a42a60eb5cb"
+    },
+    {
+      "path": "predecessor/README.md",
+      "source_path": "research/complex-t16-evacuation-increment/README.md",
+      "git_blob": "8e9889dd3305f8ac45e0f3a571db8cd605347226",
+      "sha256": "61200e79eec2dc3d03df5a4dec96a273aeb4d5ba6a171aaf1366f58551da2912"
+    },
+    {
+      "path": "predecessor/CANDIDATE.json",
+      "source_path": "research/complex-t16-evacuation-increment/CANDIDATE.json",
+      "git_blob": "d33c7388a40c612dc249faf87d7cb0c52a847347",
+      "sha256": "bbc52fad1625b10fb49a12dc926c2a903f010446a47975143e9e51c7acd5b1e2"
+    }
+  ],
+  "predecessor_owners_sha256": "0875c29c3da8ea23a20d4d261f7f6bcdb4b1eab750547eff8a7fc12e4dfc463b",
+  "predecessor_canonical_sha256": "bb9438a7995d0d25689cfa079df9851064ff1eafd72e6a9549f480ea28dfd348",
+  "map_reconstruction": "canonical research/complex-t16-two-stage-cycles/data/OWNERS.json.gz plus byte-identical predecessor/DIFF-vs-predecessor.json; compare complete canonical JSON payload, not recompressed container"
+}