Improve conditional κ to 0.0016965151242727336 with a pure 44th dirty alias

research/t74-borrow-repacked/BORROW-DELETION-AUDIT.json

@@ -0,0 +1,24 @@
+{
+  "status": "PASS_FRESH_KERNEL_AND_SEPARATE_TRANSITIVE_AXIOM_AUDIT",
+  "source": "BorrowDeletion.lean",
+  "source_sha256": "4e08031897d54eb8e5d058145e763c30173f4b5314976aa4b9819013c3fd3860",
+  "lean_version": "4.33.0",
+  "theorems": {
+    "IntegerMultBounds.BorrowDeletion.strict_subadditive_rpow_pos": [
+      "propext",
+      "Classical.choice",
+      "Quot.sound"
+    ],
+    "IntegerMultBounds.BorrowDeletion.rank_four_deletion_strictly_cheaper": [
+      "propext",
+      "Classical.choice",
+      "Quot.sound"
+    ],
+    "IntegerMultBounds.BorrowDeletion.repeated_deletion_strict": [
+      "propext",
+      "Classical.choice",
+      "Quot.sound"
+    ]
+  },
+  "scope": "Universal sufficient cost certificates. For the actual owner deletion, separately checked complete-call endpoint and disjoint hosting equality identifies the profile exchange C1+C4 to C5."
+}

research/t74-borrow-repacked/BorrowDeletion.lean

@@ -0,0 +1,49 @@
+import Mathlib.Analysis.Convex.SpecificFunctions.Pow
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Ring
+import Mathlib.Tactic.NormNum
+
+/-! Sufficient cost certificates for removing a rank-four helper and returning
+its owned four axes to a rank-one remainder, replacing ranks 1 and 4 by 5. -/
+namespace IntegerMultBounds.BorrowDeletion
+
+/-- Joining two positive ranks strictly lowers every sublinear real-power cost. -/
+theorem strict_subadditive_rpow_pos (x y p : ℝ) (hx : 0 < x) (hy : 0 < y)
+    (hp : 0 ≤ p) (hp1 : p < 1) : (x+y)^p < x^p + y^p := by
+  rcases hp.eq_or_lt with hzero | hpos
+  · subst p
+    norm_num
+  have hsum : 0 < x+y := add_pos hx hy
+  have hweights : y/(x+y) + x/(x+y) = 1 := by
+    field_simp
+    ring
+  have hweights' : x/(x+y) + y/(x+y) = 1 := by linarith [hweights]
+  have h0 : (0 : ℝ) ∈ Set.Ici 0 := by norm_num
+  have hs : x+y ∈ Set.Ici (0 : ℝ) := le_of_lt hsum
+  have hne : (0 : ℝ) ≠ x+y := ne_of_lt hsum
+  have ha := (Real.strictConcaveOn_rpow hpos hp1).2 h0 hs hne
+    (div_pos hy hsum) (div_pos hx hsum) hweights
+  have hb := (Real.strictConcaveOn_rpow hpos hp1).2 h0 hs hne
+    (div_pos hx hsum) (div_pos hy hsum) hweights'
+  simp only [smul_eq_mul, Real.zero_rpow (ne_of_gt hpos), mul_zero, zero_add,
+    div_mul_cancel₀ _ (ne_of_gt hsum)] at ha hb
+  have heq : y/(x+y) * (x+y)^p + x/(x+y) * (x+y)^p = (x+y)^p := by
+    rw [← add_mul, hweights, one_mul]
+  linarith
+
+/-- The actual helper deletion changes C1+C4 into C5 and strictly saves cost. -/
+theorem rank_four_deletion_strictly_cheaper (p : ℝ) (hp : 0 ≤ p) (hp1 : p < 1) :
+    (5 : ℝ)^p - 1 - (4 : ℝ)^p < 0 := by
+  have h := strict_subadditive_rpow_pos 1 4 p (by norm_num) (by norm_num) hp hp1
+  norm_num at h
+  linarith
+
+/-- Any positive number of actual disjoint helper deletions gives a strict gain. -/
+theorem repeated_deletion_strict (p count old : ℝ) (hp : 0 ≤ p) (hp1 : p < 1)
+    (hcount : 0 < count) :
+    old + count * ((5 : ℝ)^p - 1 - (4 : ℝ)^p) < old := by
+  have h := mul_neg_of_pos_of_neg hcount (rank_four_deletion_strictly_cheaper p hp hp1)
+  linarith
+
+end IntegerMultBounds.BorrowDeletion

research/t74-borrow-repacked/CLAIM.json

@@ -0,0 +1,16 @@
+{
+  "status": "FROZEN_NEW_SUPPLIER_PENDING_STRICT_RELEASE_REPLAY",
+  "kappa": "33872836705681463/20000000000000000000",
+  "kappa_decimal": "0.00169364183528407315",
+  "baseline_pr": 2288,
+  "baseline_kappa": "0.001696310950415050",
+  "construction_improvement": true,
+  "outer_refinement": {
+    "grid_digits": 20,
+    "margin_digits": 30,
+    "bootstrap_steps": 14,
+    "endpoint_digits": 24
+  },
+  "scope": "Conditional finite construction only. All-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape, exact recovery, analytic transfer, PR559 recurrence correction and PR589 bit H1-H5 assumptions remain. No unconditional theorem, full Lean certification, or global packing claim.",
+  "verification": "Additional pure alias619->530, all666 completed calls use extra, literal6-row packing, fully charged private storage and monomial routing; exact native and conservative engines and strict replay required by verify_release.py. Full compiler/tape/recovery/analytic interfaces remain conditional."
+}

research/t74-borrow-repacked/CONSTRUCTION.json

@@ -0,0 +1 @@
+{"dispatch":{"extra":666},"helpers_per_call":436,"idle":{"1":23310,"14":1,"3":8673,"48":24479,"5":1479,"7":148},"roles":290376,"scope":"Literal strict windows, bin capacities, per-call helper widths and distinct physical families verified for the shipped fill; local programs are the borrow words; full parent binding, finite invoice and global admission run separately.","status":"PASS_EXACT_BORROW_WORD_T74_OWNER_FILL"}

research/t74-borrow-repacked/COST-GAIN-IDENTITY.json

@@ -0,0 +1,70 @@
+{
+  "status": "PASS_EXACT_NEW_VERSUS_UPSTREAM_PROFILE_DECOMPOSITION",
+  "upstream": {
+    "pr": 2269,
+    "repository": "jeremykothe2/integer-mult-bounds",
+    "commit": "b479fc5567bc09ab9185bffe89b62594f36d74e5",
+    "path": "research/gmx-t74-borrow43/new/SPEC.json",
+    "sha256": "bd091ed9e7f4939d06abb467d0d2c56ce0f34ba800d74132669f7b667e125d2d"
+  },
+  "new_spec_sha256": "1bf99767d806e7df1ad03a927c8e9923548128cf463cfa61c1321686332060ae",
+  "old_profile": {
+    "1": 1584738,
+    "2": 337002,
+    "3": 286065,
+    "4": 84246,
+    "5": 28785,
+    "7": 150,
+    "8": 5328,
+    "48": 24479
+  },
+  "new_profile": {
+    "1": 1581084,
+    "2": 338994,
+    "3": 287061,
+    "4": 82584,
+    "5": 29451,
+    "7": 148,
+    "8": 5328,
+    "14": 1,
+    "48": 24479
+  },
+  "exchanges": [
+    {
+      "multiplicity": 249,
+      "delta": {
+        "1": -12,
+        "2": 8,
+        "3": 4,
+        "4": -4
+      }
+    },
+    {
+      "multiplicity": 666,
+      "delta": {
+        "1": -1,
+        "4": -1,
+        "5": 1
+      }
+    },
+    {
+      "multiplicity": 1,
+      "delta": {
+        "7": -2,
+        "14": 1
+      }
+    }
+  ],
+  "total_delta": {
+    "1": -3654,
+    "2": 1992,
+    "3": 996,
+    "4": -1662,
+    "5": 666,
+    "7": -2,
+    "14": 1
+  },
+  "rank_mass_delta": 0,
+  "paid_child_count_delta": -1663,
+  "scope": "Exact coefficient identity; strict analytic improvement follows from the separate universal Mathlib theorems. Physical interpretation is certified by fresh native/owner/finite-invoice admission."
+}

research/t74-borrow-repacked/DISPATCH.json

@@ -0,0 +1 @@
+[[0,0,"extra"],[0,37,"extra"],[0,1,"extra"],[0,38,"extra"],[0,2,"extra"],[0,39,"extra"],[0,3,"extra"],[0,40,"extra"],[0,4,"extra"],[0,41,"extra"],[1,0,"extra"],[1,37,"extra"],[0,5,"extra"],[0,42,"extra"],[1,1,"extra"],[1,38,"extra"],[0,6,"extra"],[0,43,"extra"],[1,2,"extra"],[1,39,"extra"],[0,7,"extra"],[0,44,"extra"],[1,3,"extra"],[1,40,"extra"],[0,8,"extra"],[0,45,"extra"],[1,4,"extra"],[1,41,"extra"],[0,9,"extra"],[0,46,"extra"],[2,0,"extra"],[2,37,"extra"],[1,5,"extra"],[1,42,"extra"],[0,10,"extra"],[0,47,"extra"],[2,1,"extra"],[2,38,"extra"],[1,6,"extra"],[1,43,"extra"],[0,11,"extra"],[0,48,"extra"],[2,2,"extra"],[2,39,"extra"],[1,7,"extra"],[1,44,"extra"],[0,12,"extra"],[0,49,"extra"],[2,3,"extra"],[2,40,"extra"],[1,8,"extra"],[1,45,"extra"],[0,13,"extra"],[0,50,"extra"],[2,4,"extra"],[2,41,"extra"],[1,9,"extra"],[1,46,"extra"],[3,0,"extra"],[3,37,"extra"],[0,14,"extra"],[0,51,"extra"],[2,5,"extra"],[2,42,"extra"],[1,10,"extra"],[1,47,"extra"],[3,1,"extra"],[3,38,"extra"],[0,15,"extra"],[0,52,"extra"],[2,6,"extra"],[2,43,"extra"],[1,11,"extra"],[1,48,"extra"],[3,2,"extra"],[3,39,"extra"],[0,16,"extra"],[0,53,"extra"],[2,7,"extra"],[2,44,"extra"],[1,12,"extra"],[1,49,"extra"],[3,3,"extra"],[3,40,"extra"],[0,17,"extra"],[0,54,"extra"],[2,8,"extra"],[2,45,"extra"],[1,13,"extra"],[1,50,"extra"],[3,4,"extra"],[3,41,"extra"],[0,18,"extra"],[0,55,"extra"],[2,9,"extra"],[2,46,"extra"],[4,0,"extra"],[4,37,"extra"],[1,14,"extra"],[1,51,"extra"],[3,5,"extra"],[3,42,"extra"],[0,19,"extra"],[0,56,"extra"],[2,10,"extra"],[2,47,"extra"],[4,1,"extra"],[4,38,"extra"],[1,15,"extra"],[1,52,"extra"],[3,6,"extra"],[3,43,"extra"],[0,20,"extra"],[0,57,"extra"],[2,11,"extra"],[2,48,"extra"],[4,2,"extra"],[4,39,"extra"],[1,16,"extra"],[1,53,"extra"],[3,7,"extra"],[3,44,"extra"],[0,21,"extra"],[0,58,"extra"],[2,12,"extra"],[2,49,"extra"],[4,3,"extra"],[4,40,"extra"],[1,17,"extra"],[1,54,"extra"],[3,8,"extra"],[3,45,"extra"],[0,22,"extra"],[0,59,"extra"],[2,13,"extra"],[2,50,"extra"],[4,4,"extra"],[4,41,"extra"],[1,18,"extra"],[1,55,"extra"],[3,9,"extra"],[3,46,"extra"],[0,23,"extra"],[0,60,"extra"],[5,0,"extra"],[5,37,"extra"],[2,14,"extra"],[2,51,"extra"],[4,5,"extra"],[4,42,"extra"],[1,19,"extra"],[1,56,"extra"],[3,10,"extra"],[3,47,"extra"],[0,24,"extra"],[0,61,"extra"],[5,1,"extra"],[5,38,"extra"],[2,15,"extra"],[2,52,"extra"],[4,6,"extra"],[4,43,"extra"],[1,20,"extra"],[1,57,"extra"],[3,11,"extra"],[3,48,"extra"],[0,25,"extra"],[0,62,"extra"],[5,2,"extra"],[5,39,"extra"],[2,16,"extra"],[2,53,"extra"],[4,7,"extra"],[4,44,"extra"],[1,21,"extra"],[1,58,"extra"],[3,12,"extra"],[3,49,"extra"],[0,26,"extra"],[0,63,"extra"],[5,3,"extra"],[5,40,"extra"],[2,17,"extra"],[2,54,"extra"],[4,8,"extra"],[4,45,"extra"],[1,22,"extra"],[1,59,"extra"],[3,13,"extra"],[3,50,"extra"],[0,27,"extra"],[0,64,"extra"],[5,4,"extra"],[5,41,"extra"],[2,18,"extra"],[2,55,"extra"],[4,9,"extra"],[4,46,"extra"],[1,23,"extra"],[1,60,"extra"],[6,0,"extra"],[6,37,"extra"],[3,14,"extra"],[3,51,"extra"],[0,28,"extra"],[0,65,"extra"],[5,5,"extra"],[5,42,"extra"],[2,19,"extra"],[2,56,"extra"],[4,10,"extra"],[4,47,"extra"],[1,24,"extra"],[1,61,"extra"],[6,1,"extra"],[6,38,"extra"],[3,15,"extra"],[3,52,"extra"],[0,29,"extra"],[0,66,"extra"],[5,6,"extra"],[5,43,"extra"],[2,20,"extra"],[2,57,"extra"],[4,11,"extra"],[4,48,"extra"],[1,25,"extra"],[1,62,"extra"],[6,2,"extra"],[6,39,"extra"],[3,16,"extra"],[3,53,"extra"],[0,30,"extra"],[0,67,"extra"],[5,7,"extra"],[5,44,"extra"],[2,21,"extra"],[2,58,"extra"],[4,12,"extra"],[4,49,"extra"],[1,26,"extra"],[1,63,"extra"],[6,3,"extra"],[6,40,"extra"],[3,17,"extra"],[3,54,"extra"],[0,31,"extra"],[0,68,"extra"],[5,8,"extra"],[5,45,"extra"],[2,22,"extra"],[2,59,"extra"],[4,13,"extra"],[4,50,"extra"],[1,27,"extra"],[1,64,"extra"],[6,4,"extra"],[6,41,"extra"],[3,18,"extra"],[3,55,"extra"],[0,32,"extra"],[0,69,"extra"],[5,9,"extra"],[5,46,"extra"],[2,23,"extra"],[2,60,"extra"],[7,0,"extra"],[7,37,"extra"],[4,14,"extra"],[4,51,"extra"],[1,28,"extra"],[1,65,"extra"],[6,5,"extra"],[6,42,"extra"],[3,19,"extra"],[3,56,"extra"],[0,33,"extra"],[0,70,"extra"],[5,10,"extra"],[5,47,"extra"],[2,24,"extra"],[2,61,"extra"],[7,1,"extra"],[7,38,"extra"],[4,15,"extra"],[4,52,"extra"],[1,29,"extra"],[1,66,"extra"],[6,6,"extra"],[6,43,"extra"],[3,20,"extra"],[3,57,"extra"],[0,34,"extra"],[0,71,"extra"],[5,11,"extra"],[5,48,"extra"],[2,25,"extra"],[2,62,"extra"],[7,2,"extra"],[7,39,"extra"],[4,16,"extra"],[4,53,"extra"],[1,30,"extra"],[1,67,"extra"],[6,7,"extra"],[6,44,"extra"],[3,21,"extra"],[3,58,"extra"],[0,35,"extra"],[0,72,"extra"],[5,12,"extra"],[5,49,"extra"],[2,26,"extra"],[2,63,"extra"],[7,3,"extra"],[7,40,"extra"],[4,17,"extra"],[4,54,"extra"],[1,31,"extra"],[1,68,"extra"],[6,8,"extra"],[6,45,"extra"],[3,22,"extra"],[3,59,"extra"],[0,36,"extra"],[0,73,"extra"],[5,13,"extra"],[5,50,"extra"],[2,27,"extra"],[2,64,"extra"],[7,4,"extra"],[7,41,"extra"],[4,18,"extra"],[4,55,"extra"],[1,32,"extra"],[1,69,"extra"],[6,9,"extra"],[6,46,"extra"],[3,23,"extra"],[3,60,"extra"],[8,0,"extra"],[8,37,"extra"],[5,14,"extra"],[5,51,"extra"],[2,28,"extra"],[2,65,"extra"],[7,5,"extra"],[7,42,"extra"],[4,19,"extra"],[4,56,"extra"],[1,33,"extra"],[1,70,"extra"],[6,10,"extra"],[6,47,"extra"],[3,24,"extra"],[3,61,"extra"],[8,1,"extra"],[8,38,"extra"],[5,15,"extra"],[5,52,"extra"],[2,29,"extra"],[2,66,"extra"],[7,6,"extra"],[7,43,"extra"],[4,20,"extra"],[4,57,"extra"],[1,34,"extra"],[1,71,"extra"],[6,11,"extra"],[6,48,"extra"],[3,25,"extra"],[3,62,"extra"],[8,2,"extra"],[8,39,"extra"],[5,16,"extra"],[5,53,"extra"],[2,30,"extra"],[2,67,"extra"],[7,7,"extra"],[7,44,"extra"],[4,21,"extra"],[4,58,"extra"],[1,35,"extra"],[1,72,"extra"],[6,12,"extra"],[6,49,"extra"],[3,26,"extra"],[3,63,"extra"],[8,3,"extra"],[8,40,"extra"],[5,17,"extra"],[5,54,"extra"],[2,31,"extra"],[2,68,"extra"],[7,8,"extra"],[7,45,"extra"],[4,22,"extra"],[4,59,"extra"],[1,36,"extra"],[1,73,"extra"],[6,13,"extra"],[6,50,"extra"],[3,27,"extra"],[3,64,"extra"],[8,4,"extra"],[8,41,"extra"],[5,18,"extra"],[5,55,"extra"],[2,32,"extra"],[2,69,"extra"],[7,9,"extra"],[7,46,"extra"],[4,23,"extra"],[4,60,"extra"],[6,14,"extra"],[6,51,"extra"],[3,28,"extra"],[3,65,"extra"],[8,5,"extra"],[8,42,"extra"],[5,19,"extra"],[5,56,"extra"],[2,33,"extra"],[2,70,"extra"],[7,10,"extra"],[7,47,"extra"],[4,24,"extra"],[4,61,"extra"],[6,15,"extra"],[6,52,"extra"],[3,29,"extra"],[3,66,"extra"],[8,6,"extra"],[8,43,"extra"],[5,20,"extra"],[5,57,"extra"],[2,34,"extra"],[2,71,"extra"],[7,11,"extra"],[7,48,"extra"],[4,25,"extra"],[4,62,"extra"],[6,16,"extra"],[6,53,"extra"],[3,30,"extra"],[3,67,"extra"],[8,7,"extra"],[8,44,"extra"],[5,21,"extra"],[5,58,"extra"],[2,35,"extra"],[2,72,"extra"],[7,12,"extra"],[7,49,"extra"],[4,26,"extra"],[4,63,"extra"],[6,17,"extra"],[6,54,"extra"],[3,31,"extra"],[3,68,"extra"],[8,8,"extra"],[8,45,"extra"],[5,22,"extra"],[5,59,"extra"],[2,36,"extra"],[2,73,"extra"],[7,13,"extra"],[7,50,"extra"],[4,27,"extra"],[4,64,"extra"],[6,18,"extra"],[6,55,"extra"],[3,32,"extra"],[3,69,"extra"],[8,9,"extra"],[8,46,"extra"],[5,23,"extra"],[5,60,"extra"],[7,14,"extra"],[7,51,"extra"],[4,28,"extra"],[4,65,"extra"],[6,19,"extra"],[6,56,"extra"],[3,33,"extra"],[3,70,"extra"],[8,10,"extra"],[8,47,"extra"],[5,24,"extra"],[5,61,"extra"],[7,15,"extra"],[7,52,"extra"],[4,29,"extra"],[4,66,"extra"],[6,20,"extra"],[6,57,"extra"],[3,34,"extra"],[3,71,"extra"],[8,11,"extra"],[8,48,"extra"],[5,25,"extra"],[5,62,"extra"],[7,16,"extra"],[7,53,"extra"],[4,30,"extra"],[4,67,"extra"],[6,21,"extra"],[6,58,"extra"],[3,35,"extra"],[3,72,"extra"],[8,12,"extra"],[8,49,"extra"],[5,26,"extra"],[5,63,"extra"],[7,17,"extra"],[7,54,"extra"],[4,31,"extra"],[4,68,"extra"],[6,22,"extra"],[6,59,"extra"],[3,36,"extra"],[3,73,"extra"],[8,13,"extra"],[8,50,"extra"],[5,27,"extra"],[5,64,"extra"],[7,18,"extra"],[7,55,"extra"],[4,32,"extra"],[4,69,"extra"],[6,23,"extra"],[6,60,"extra"],[8,14,"extra"],[8,51,"extra"],[5,28,"extra"],[5,65,"extra"],[7,19,"extra"],[7,56,"extra"],[4,33,"extra"],[4,70,"extra"],[6,24,"extra"],[6,61,"extra"],[8,15,"extra"],[8,52,"extra"],[5,29,"extra"],[5,66,"extra"],[7,20,"extra"],[7,57,"extra"],[4,34,"extra"],[4,71,"extra"],[6,25,"extra"],[6,62,"extra"],[8,16,"extra"],[8,53,"extra"],[5,30,"extra"],[5,67,"extra"],[7,21,"extra"],[7,58,"extra"],[4,35,"extra"],[4,72,"extra"],[6,26,"extra"],[6,63,"extra"],[8,17,"extra"],[8,54,"extra"],[5,31,"extra"],[5,68,"extra"],[7,22,"extra"],[7,59,"extra"],[4,36,"extra"],[4,73,"extra"],[6,27,"extra"],[6,64,"extra"],[8,18,"extra"],[8,55,"extra"],[5,32,"extra"],[5,69,"extra"],[7,23,"extra"],[7,60,"extra"],[6,28,"extra"],[6,65,"extra"],[8,19,"extra"],[8,56,"extra"],[5,33,"extra"],[5,70,"extra"],[7,24,"extra"],[7,61,"extra"],[6,29,"extra"],[6,66,"extra"],[8,20,"extra"],[8,57,"extra"],[5,34,"extra"],[5,71,"extra"],[7,25,"extra"],[7,62,"extra"],[6,30,"extra"],[6,67,"extra"],[8,21,"extra"],[8,58,"extra"],[5,35,"extra"],[5,72,"extra"],[7,26,"extra"],[7,63,"extra"],[6,31,"extra"],[6,68,"extra"],[8,22,"extra"],[8,59,"extra"],[5,36,"extra"],[5,73,"extra"],[7,27,"extra"],[7,64,"extra"],[6,32,"extra"],[6,69,"extra"],[8,23,"extra"],[8,60,"extra"],[7,28,"extra"],[7,65,"extra"],[6,33,"extra"],[6,70,"extra"],[8,24,"extra"],[8,61,"extra"],[7,29,"extra"],[7,66,"extra"],[6,34,"extra"],[6,71,"extra"],[8,25,"extra"],[8,62,"extra"],[7,30,"extra"],[7,67,"extra"],[6,35,"extra"],[6,72,"extra"],[8,26,"extra"],[8,63,"extra"],[7,31,"extra"],[7,68,"extra"],[6,36,"extra"],[6,73,"extra"],[8,27,"extra"],[8,64,"extra"],[7,32,"extra"],[7,69,"extra"],[8,28,"extra"],[8,65,"extra"],[7,33,"extra"],[7,70,"extra"],[8,29,"extra"],[8,66,"extra"],[7,34,"extra"],[7,71,"extra"],[8,30,"extra"],[8,67,"extra"],[7,35,"extra"],[7,72,"extra"],[8,31,"extra"],[8,68,"extra"],[7,36,"extra"],[7,73,"extra"],[8,32,"extra"],[8,69,"extra"],[8,33,"extra"],[8,70,"extra"],[8,34,"extra"],[8,71,"extra"],[8,35,"extra"],[8,72,"extra"],[8,36,"extra"],[8,73,"extra"]]