Compose clean native merge with mixed root at raw saving 0.0032868

research/clean-native-mixed-root/PROOF.md

@@ -0,0 +1,125 @@
+# Clean native merge in the mixed root
+
+This is a scoped accounting proof, conditional on the two exact predecessor
+interfaces below. It is not a new whole-algorithm kappa claim, a native replay,
+a supplier admission or a complete multiplication theorem.
+
+## Premises and substitution
+
+Rohan Arun's PR6399 at `a928a7aa5ab5b21b7cf841d6d960ab2e7efd1041`
+supplies an unchanged-input, unchanged-output replacement of the PR6375
+native interface. Its normalized main map and all independent helper targets
+are retained. Its one additional scratch lifetime is returned to zero. Those
+operator and restoration statements are cited premises here, not independently
+verified conclusions of this package. See the exact retained
+[source proof](inputs/merge-proof.md).
+
+Ali Romman's PR6398 at `dee2663ba0918be86993fd9d63c8d64b020f4c83`
+supplies a mixed root using eighteen copies of precisely that PR6375 native
+interface. Helpers from different calls remain independent, and normalization
+acts on the complete field. Its physical embedding, central normalization and
+caller identity are also premises. See the retained
+[composition proof](inputs/root-proof.md).
+
+Consequently the new abstract composition replaces each of those eighteen
+native copies by PR6399's interface. Every old helper target, caller query,
+whole idle and ordinary normalization stays in its original place. The
+replacement is private to a native call. Its additional restored scratch
+lifetime is not an additional productive target. This substitution is the new
+object; neither predecessor was priced with this combination.
+
+Let P and T denote PR6398's complete paid and productive histograms. Let
+P_local and P_clean denote the respective old and new native paid histograms.
+The retained receipts give
+
+    P_clean - P_local = -[1] - [4] + [5].
+
+The complete new invoice is therefore
+
+    T_new = T,
+    P_other = P - 18 P_local,
+    P_new = P_other + 18 P_clean.
+
+The verifier explicitly constructs the nonnegative histogram P_other. It
+does not discard the non-native jobs. It constructs every entry of P_new,
+and enumerates 13,652 productive fields and 67,132 paid jobs. The productive
+rank mass is 185,740 and the paid rank mass is 184,980, preserving surplus 760.
+The count reduction is eighteen jobs, not eighteen rank units.
+
+## Strict gain and one new funded point
+
+For 0 < t < 1, define M(T,P;t) = sum_r (T_r-P_r) r^t. The substitution gives
+
+    M(T_new,P_new;t) - M(T,P;t) = 18 (1 + 4^t - 5^t) > 0.
+
+Strict positivity follows from strict subadditivity of x^t for positive
+arguments. For example, integrate its strictly decreasing derivative over
+[4,5] and compare with the integral over [0,1]. This proves gain over the
+same root for every such tariff. It does not transfer the predecessor's
+fixed-source raw optimum to this changed source.
+
+At the exact saving C = 41085/12500000 = 0.0032868, set t = 1-C.
+The new full invoice satisfies
+
+    0.0130615 < M(T_new,P_new;t) < 0.0130617.
+
+The old invoice has strictly negative margin at this same C. These signs,
+the full histograms and tighter rational outward decimal enclosures are
+generated in RESULT.json. The exponent is an exact rational, not a binary
+floating-point input. The retained exact interval functions use an atanh
+logarithm series and outward-rounded exponential Taylor intervals. This
+package calls only their arithmetic functions; it does not run their
+historical construction replay. The elementary substitution proof and this
+fixed numerical certificate are the claims. No new root search or optimality
+claim is needed.
+
+## Ordinary allowance and remaining obligations
+
+The replacement's scalar allowance is 130,178, an increase of 508 per call.
+Its 44 local owned lifetimes replace 43; its peak owned fields remain 13.
+Using the declared PR6398 local routing envelope, including four endpoint
+charges per lifetime, gives
+
+    routes = 1000 (3458 + 1124 + 208 + 4*104 + 4*44) = 5,382,000,
+    scalar + routes = 5,512,178 < 10,000,000.
+
+Thus the added local scalar work and lifetime charges fit that declared
+ordinary envelope. The total increase in this envelope is 3,508 per native
+copy: 508 scalar units and 3,000 route units. The latter includes the saving
+of one paid job and the cost of the extra lifetime. Across eighteen copies,
+the increase is 63,144. This is an allowance calculation, not execution or
+independent validation of the physical routing theorem.
+
+The combined physical native/caller replay, a newly chosen strictification
+and compiler grid, combined precision/tape validation, and all outer
+inequalities are unrun. No whole-algorithm kappa is asserted at C. In
+particular, a passing raw margin is not a free compiler or supplier admission.
+The five inherited assumptions remain: native_all_columns, owned_erasure,
+compiler, precision_tape and analytic_recovery.
+
+## Certificate and controls
+
+The verifier binds exact predecessor receipts, proofs and notices by SHA256
+and Git blob identifiers. These are byte-equal retained snapshots, not
+handwritten extracts of predecessor counts. Their source URLs and commits
+are in SOURCES.json. They are available without pending-commit Git ancestry.
+The generic source-history check covers the main-based manifest pins; it
+does not claim to authenticate the external snapshots' publication history.
+
+Seven enumerated semantic mutations reject changed helper targets, a free
+merged query, omitted cleanup allowance, an omitted lifetime, a changed peak,
+and either wrong native multiplicity. The arithmetic control checks exact
+square-root enclosure inequalities for every integer rank 1 through 145.
+Normal and optimized Python run the same explicit checks. These controls do
+not establish independent scientific or proof-kernel acceptance.
+
+## Credit
+
+This composition and its certificate were produced by Nick Petalas.
+The clean native merge and its zero-restored scratch construction are Rohan
+Arun's PR6399. The mixed root, complete-field normalization and its original
+invoice are Ali Romman's PR6398. DreamingOfClouds supplied the PR6375
+shared-carrier lifts. Cinna Davis supplied the caller interfaces, Jacob Alan
+Sussman supplied productive recursion, and zxv supplied the retained exact
+interval engine. The unchanged source notices retain the complete
+native, helper, geometry, BIT, compiler and analytic lineage. Apache-2.0.

research/clean-native-mixed-root/README.md

@@ -0,0 +1,77 @@
+# Clean native merge in the mixed root
+
+The new composition of Rohan Arun's [PR6399 clean native merge](https://github.com/CrocSwap/integer-mult-bounds/pull/6399)
+and Ali Romman's [PR6398 mixed root](https://github.com/CrocSwap/integer-mult-bounds/pull/6398)
+has a strictly positive complete recursive margin at saving **0.0032868**.
+PR6398's original invoice has negative margin at that same saving.
+
+Claim type: a scoped accounting proof, conditional on the retained native
+and caller interfaces, with an exact finite certificate. This is a new
+composition, not an audit of either predecessor. It asserts no complete
+whole-algorithm kappa or selected-frontier change.
+
+Eighteen substitutions of `H4 + H1` by `H5` remove eighteen paid jobs while
+preserving every productive target and both rank masses. The complete new
+invoice has **13,652 productive fields and 67,132 paid jobs**. Its margin at
+`t = 1 - 0.0032868` is between `0.0130615` and `0.0130617`. The improvement is
+`18 (1 + 4^t - 5^t) > 0` for every `0 < t < 1`.
+
+The additional scratch lifetime and scalar cleanup are charged. The new local
+ordinary allowance is **5,512,178**, below the predecessor's declared
+10,000,000 envelope. This allowance comparison does not implement routing,
+precision or a compiler. [PROOF.md](PROOF.md) states the composition and all
+remaining obligations; [RESULT.json](RESULT.json) is generated by the verifier.
+
+## Reproduction
+
+From the repository root, using CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/clean-native-mixed-root/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/clean-native-mixed-root/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clean-native-mixed-root
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clean-native-mixed-root --check-source-history --check-modes
+```
+
+Use an equivalent Python 3.12 path on another machine. The verifier is
+standard-library only and writes nothing during ordinary replay. It checks
+the complete new histograms, exact interval signs, ordinary allowance, seven
+semantic rejection controls and 145 exact square-root enclosure controls.
+It regenerates the receipt in memory and compares every field. To regenerate
+an explicit receipt, pass `--write-result /absolute/scratch/RESULT.json`.
+
+The main-based exact arithmetic input is declared in VERIFY.json. Exact
+predecessor receipts, proofs and notices are retained under inputs/ with
+original URLs, commits, SHA256 and Git blob identifiers in SOURCES.json.
+They do not require pending commits in the checkout's Git history. Their
+mathematical claims remain premises. The source-history check covers the
+ordinary main-based pins, not remote publication ancestry of these snapshots.
+
+## Limitations
+
+The combined physical word/caller replay, new completion and compiler
+parameters, combined precision/tape contract and outer inequality ledger have
+not been run. All five framework assumptions remain. Neither independent
+human nor formal proof-kernel acceptance is claimed. The screen saving is
+not a certified multiplication exponent. Frozen predecessor artifacts and
+the selected result remain unchanged.
+
+## Open next questions
+
+Can the concrete replacement pass the complete eighteen-call physical
+mixed-root replay and admit a whole bound below this funded raw saving?
+Start by binding PR6399's constructor and scratch-zero check to PR6398's
+unchanged controller. Then select strict compiler/outer parameters and run
+the changed composition's complete ledger. The unresolved physical and
+framework premises are blockers. TASK.json records this question in a
+structured form. Further optimization of the raw crossing is not needed
+before that admission step.
+
+## Credit
+
+This result was produced by Nick Petalas. Rohan Arun supplied the native
+merge and explicit scratch restoration; Ali Romman supplied the mixed root
+and its complete original invoice; DreamingOfClouds supplied the shared
+carrier lifts. Cinna Davis, Jacob Alan Sussman and zxv supplied the caller,
+productive recursion and exact interval foundations. Both unchanged source
+notices retain all predecessor credit. Apache-2.0.

research/clean-native-mixed-root/RESULT.json

@@ -0,0 +1,85 @@
+{
+  "claim_type": "scoped accounting proof conditional on retained interfaces",
+  "combined_margin": {
+    "lower": "0.013061578546729933727885198969",
+    "upper": "0.013061578546729933727885198970"
+  },
+  "controls": {
+    "exact_square_root_controls": 145,
+    "rejected": [
+      "helper target debit",
+      "unpaid merged query",
+      "omitted scalar cleanup",
+      "omitted scratch lifetime",
+      "larger peak treated as unchanged",
+      "wrong native multiplicity 17",
+      "wrong native multiplicity 19"
+    ]
+  },
+  "native_copies": 18,
+  "ordinary_allowance": {
+    "additional_lifetimes": 18,
+    "local_budget": 10000000,
+    "local_ordinary_total": 5512178,
+    "local_routes": 5382000,
+    "local_scalar": 130178,
+    "peak_owned_fields": 13
+  },
+  "paid": {
+    "1": 42016,
+    "2": 8154,
+    "3": 8838,
+    "4": 1944,
+    "5": 2736,
+    "6": 144,
+    "7": 162,
+    "8": 18,
+    "16": 1872,
+    "24": 416,
+    "32": 416,
+    "56": 416
+  },
+  "paid_job_reduction": 18,
+  "paid_jobs": 67132,
+  "paid_rank_mass": 184980,
+  "predecessor_invoice_margin_at_same_saving": {
+    "lower": "-0.134452721442009416742639196431",
+    "upper": "-0.134452721442009416742639196430"
+  },
+  "productive_fields": 13652,
+  "saving_screen": "8217/2500000",
+  "signed_gain": {
+    "lower": "0.147514299988739350470524395399",
+    "upper": "0.147514299988739350470524395400"
+  },
+  "source_sha256": {
+    "inputs/merge-NOTICE": "80b7d5fa85b817e9b544be00d3197aeabecfc7aa20e0666b9e4c69fbb4a029b3",
+    "inputs/merge-proof.md": "c1b32f7b50db99871da529ed8673b31754dde327ccddb1d7d54b6310cc27b193",
+    "inputs/merge-result.json": "b208fe6b40397ddcc1c88a40fdd050628ad51f5907107867bd32014ddc0208d2",
+    "inputs/root-NOTICE": "60b778c0bfadff92601e1f158b7e0ca72af9f7c31e58a369d802376ee0adc9e6",
+    "inputs/root-proof.md": "de410dc656d11e82ee299793c2d9af40e2c83553197ed27eb60c7a60198b8ca7",
+    "inputs/root-result.json": "621c943f72f94b4fe168a1e1ad10edc637cfe7221690d131b33ecbda4601b53c",
+    "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326"
+  },
+  "status": "PASS_CLEAN_NATIVE_MIXED_ROOT_SIGNED_INVOICE",
+  "target_rank_mass": 185740,
+  "targets": {
+    "1": 356,
+    "2": 144,
+    "3": 72,
+    "4": 1926,
+    "5": 270,
+    "6": 54,
+    "7": 162,
+    "8": 684,
+    "9": 6552,
+    "17": 1872,
+    "25": 416,
+    "33": 416,
+    "57": 416,
+    "73": 208,
+    "145": 104
+  },
+  "verifier_sha256": "e364ac4458869825d29493142dac4aacbdfcf84fbfa4f3934e448b9a096a4c61",
+  "whole_algorithm_kappa_claimed": false
+}

research/clean-native-mixed-root/SOURCES.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/higher-moment-strictification/verify.py",
+      "usage": "input",
+      "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699",
+      "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326"
+    }
+  ],
+  "retained_external_snapshots": [
+    {
+      "path": "inputs/root-result.json",
+      "source_commit": "dee2663ba0918be86993fd9d63c8d64b020f4c83",
+      "source_path": "research/mixed-root-contact-composition/RESULT.json",
+      "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/dee2663ba0918be86993fd9d63c8d64b020f4c83/research/mixed-root-contact-composition/RESULT.json",
+      "sha256": "621c943f72f94b4fe168a1e1ad10edc637cfe7221690d131b33ecbda4601b53c",
+      "git_blob": "be12d2101b76b3b81f1fa1be2c73b4aaa6796899"
+    },
+    {
+      "path": "inputs/merge-result.json",
+      "source_commit": "a928a7aa5ab5b21b7cf841d6d960ab2e7efd1041",
+      "source_path": "research/p104-clean-piggyback/RESULT.json",
+      "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/a928a7aa5ab5b21b7cf841d6d960ab2e7efd1041/research/p104-clean-piggyback/RESULT.json",
+      "sha256": "b208fe6b40397ddcc1c88a40fdd050628ad51f5907107867bd32014ddc0208d2",
+      "git_blob": "5c684a38ed74133917834ddcce3495ef21faa8e8"
+    },
+    {
+      "path": "inputs/root-proof.md",
+      "source_commit": "dee2663ba0918be86993fd9d63c8d64b020f4c83",
+      "source_path": "research/mixed-root-contact-composition/PROOF.md",
+      "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/dee2663ba0918be86993fd9d63c8d64b020f4c83/research/mixed-root-contact-composition/PROOF.md",
+      "sha256": "de410dc656d11e82ee299793c2d9af40e2c83553197ed27eb60c7a60198b8ca7",
+      "git_blob": "49a3bb14e2a4e533e647d03955d476fcfbc9d10b"
+    },
+    {
+      "path": "inputs/merge-proof.md",
+      "source_commit": "a928a7aa5ab5b21b7cf841d6d960ab2e7efd1041",
+      "source_path": "research/p104-clean-piggyback/PROOF.md",
+      "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/a928a7aa5ab5b21b7cf841d6d960ab2e7efd1041/research/p104-clean-piggyback/PROOF.md",
+      "sha256": "c1b32f7b50db99871da529ed8673b31754dde327ccddb1d7d54b6310cc27b193",
+      "git_blob": "55e5277159ea693deb8f4f48611df2d23e2a58f9"
+    },
+    {
+      "path": "inputs/root-NOTICE",
+      "source_commit": "dee2663ba0918be86993fd9d63c8d64b020f4c83",
+      "source_path": "research/mixed-root-contact-composition/NOTICE",
+      "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/dee2663ba0918be86993fd9d63c8d64b020f4c83/research/mixed-root-contact-composition/NOTICE",
+      "sha256": "60b778c0bfadff92601e1f158b7e0ca72af9f7c31e58a369d802376ee0adc9e6",
+      "git_blob": "4e3b429712e9c4a44e80d0b57a8a1030d96740ae"
+    },
+    {
+      "path": "inputs/merge-NOTICE",
+      "source_commit": "a928a7aa5ab5b21b7cf841d6d960ab2e7efd1041",
+      "source_path": "research/p104-clean-piggyback/NOTICE",
+      "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/a928a7aa5ab5b21b7cf841d6d960ab2e7efd1041/research/p104-clean-piggyback/NOTICE",
+      "sha256": "80b7d5fa85b817e9b544be00d3197aeabecfc7aa20e0666b9e4c69fbb4a029b3",
+      "git_blob": "20ea736c50a04bbc095012e8426644ffb9121978"
+    }
+  ]
+}