Refine the certified staged544 conditional kappa endpoint to 80 digits

research/staged544-refined-endpoint/.gitattributes

@@ -0,0 +1,3 @@
+* text eol=lf
+*.gz binary
+vendor/** -text

research/staged544-refined-endpoint/CLAIM.json

@@ -0,0 +1,13 @@
+{
+  "complex_lower": "173057843726624681874071321804985755655644807397156243331276259008002643975681/100000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "complex_upper": "86528921863312340937035660902492877827822403698578121665638129504001321987841/50000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "endpoint_digits": 80,
+  "fresh_native_replay": false,
+  "gain": "762590080026439756810099999999999999999999000099999999999999999999/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "kappa": "1730578437266246818740713218049857556556448073971562433312762590080026439756809999999999999999999998999999999999999999999999/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "physical": 323069,
+  "previous": "17305784372662468187407132180498575565564480739715624333119999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "private_zero_buffers": 91,
+  "replicas": 360,
+  "selected_frontier_changed": false
+}

research/staged544-refined-endpoint/FORMAL-CHANGE-AUDIT.json

@@ -0,0 +1,30 @@
+{
+  "status": "PROOF_BODIES_UNCHANGED",
+  "changed_lines": {
+    "CapCertificate.lean": [
+      {
+        "line": 48,
+        "before_prefix": "def upper : Fin 7 \u2192 \u211a := ![(135077310945238073835664751237162262628210",
+        "after_prefix": "def upper : Fin 7 \u2192 \u211a := ![(135077310945238073835664751237162262628210"
+      }
+    ],
+    "AnalyticCertificate.lean": [
+      {
+        "line": 38,
+        "before_prefix": "def endpoint : \u211a := 54080576164570213085647288064058048642389002311611",
+        "after_prefix": "def endpoint : \u211a := 17305784372662468187407132180498575565564480739715"
+      },
+      {
+        "line": 41,
+        "before_prefix": "def upper : Fin 7 \u2192 \u211a := ![(100745261008386462509737099312640790310316",
+        "after_prefix": "def upper : Fin 7 \u2192 \u211a := ![(503726305041932312548685496563203951551581"
+      },
+      {
+        "line": 92,
+        "before_prefix": "/-- The actual real exponential moment at the published 60-digit endpo",
+        "after_prefix": "/-- The actual real exponential moment at the proposed 80-digit endpoi"
+      }
+    ]
+  },
+  "scope": "Textual change audit, not Lean elaboration/kernel check"
+}

research/staged544-refined-endpoint/FORMAL-DATA.json

@@ -0,0 +1,32 @@
+{
+  "endpoint": "173057843726624681874071321804985755655644807397156243331276259008002643975681/100000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "log_upper": {
+    "1": "42904594411483911290921088574385425709047528448715976645956988571617899759205973/10000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "2": "179865613029422290983743836799018300141462635525567120523750942383419817697545129/50000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "3": "319184715248028143769686362051601686625726228704884821286100452352429568270198833/100000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "4": "290416508002850051025764461452218943475375257615108715635433883817500273198120787/100000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "5": "268102152871429075449134952421235493137915149060307994268305096568761098821293953/100000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "8": "44220357989371104016808249861280257333565048835816638044673176573632182200230263/20000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "48": "41925843024050020002793513468331059395526174960782719637828448555072119482320947/100000000000000000000000000000000000000000000000000000000000000000000000000000000"
+  },
+  "weight_upper": {
+    "1": "5037263050419323125486854965632039515515813123979119739049327448446247437415523839971594780304879053/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "2": "1006244849300832117227334850803589471353259962367000112587337836237263822185857853193329141685299883/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "3": "10055390258478318702735196789299380974598979106244048870901713891769435640370131535754404057635525197/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "4": "2512596341033269936571327050488918900797498810133573533611463569761893864457578011954826530420192591/2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "5": "2511626245512671220465894009973910441561771954881139752642633015326322249610212835151571034808264101/2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "8": "2509584174213792103224997148477336282910856045665342057938515539919371590220915369255384660757605463/2500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "48": "10007258228810539199340477838604803218049186436146540908000107607859989792524228358661467016084073803/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+  },
+  "log_degree": 60,
+  "exp_degree": 26,
+  "root_upper": {
+    "1": "1709682071524341872977914446059068945687158662089760087588298513648466431140986964131832379/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "2": "78389268609117970295183841420183634117602514499308989820003491013074224898274587103932377/50000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "3": "59612205786190783200497858238480871280010105534840193468536084961687039700052165204929563/40000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "4": "718832762584181935863410006114861039343341562058796885073492442373725223855973513855130509/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "5": "349529725287554381854657482572542092721239471300292172144051890309678870642203459561245573/250000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "8": "1318345099355356699940061975994465396292039242917024224119936446107390011400428568787269981/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+    "48": "3293140230695581904239101463758503566499283368816211814999286028419201556213646303933641/3125000000000000000000000000000000000000000000000000000000000000000000000000000000000000"
+  }
+}

research/staged544-refined-endpoint/FRONTIER-COMPARISON.json

@@ -0,0 +1,9 @@
+{
+  "gain": "762590080026439756810099999999999999999999000099999999999999999999/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "head": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+  "new_kappa": "1730578437266246818740713218049857556556448073971562433312762590080026439756809999999999999999999998999999999999999999999999/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "physical_changed": false,
+  "previous_kappa": "17305784372662468187407132180498575565564480739715624333119999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "previous_pr": 3857,
+  "profile_changed": false
+}

research/staged544-refined-endpoint/LEAN-AXIOMS.txt

@@ -0,0 +1,6 @@
+info: CapCertificate.lean:69:0: 'Staged544Certificate.exact_certificate' depends on axioms: [propext, Classical.choice, Quot.sound]
+info: CapCertificate.lean:70:0: 'Staged544Certificate.admission' depends on axioms: [propext, Classical.choice, Quot.sound]
+info: AnalyticCertificate.lean:115:0: 'Staged544.actual_moment_lt_one' depends on axioms: [propext, Classical.choice, Quot.sound]
+info: AnalyticCertificate.lean:117:0: 'Staged544.actual_rpow_moment_lt_one' depends on axioms: [propext, Classical.choice, Quot.sound]
+Target module kernel replay: lake env leanchecker AnalyticCertificate, exit0.
+All-imports fresh kernel replay: NOT_RUN.

research/staged544-refined-endpoint/NOTICE

@@ -0,0 +1,43 @@
+Endpoint refinement and packaging by hexapode with Codex assistance.
+Direct predecessor: Dugongue PR3857, head ef4315b8caa605e47a2515004845eb2d2ed71a86.
+Retained proof bodies, engines and provenance follow below without removed credit.
+
+Dugongue, with substantial OpenAI Codex assistance. New work: Apache-2.0.
+
+Direct current predecessors:
+- ChaloupeMusic / PR3815, head 77ffbf287b6ca198b4a31e3835db3bae60718b93:
+  changed T360 clock/fill, exact fixed-inventory packing cap and complete release.
+- hexapode / PR3802, head de2cd5c58009205210e3bf328b0ef5cadf3903af:
+  first publication of the same prior endpoint via T385; PR3795 is the T488 prior.
+- dataisfire / PR3734, head fa041037a3374eaa08feeca0b26a5d6893194147:
+  staged helper 544 word, current native release and retained outer arithmetic.
+- zxv / PR3638 and PR3682: chronological T360 integration and retimed suppliers.
+- Ross Richardson / PR3605: staged-entry mechanism and source supplier.
+- roger-sato / PR3642 and PR3693: commuting-release retiming and whole-word adapter.
+- Sagar Thakrar / PR3687: arbitrary-dirty independent interpreter.
+- Arham Tahir: retained exact free-operator/frame audit lineage.
+- SovereignSteak / PR3531: positive-binomial precision precedent; dataisfire /
+  PR3361: source-bound precision integration precedent. No numerical-method priority.
+
+The original native, rank-seven, geometry, owner, hosting, COPY, prefix and outer
+contributors retain their credit: Jeremy Diviney, dcharb78, Nick Petalas,
+Marius-Paul Dumitrean, Jeremy Kothe, Mason Hale, Yiyang Lu, Tekalign, Philippe
+Van Velzen, Sagar Thakrar and all authors named in retained source notices.
+Vlado Vojdanovski supplies the outer construction; Chafik Boukhalfa's fine-prime
+padding uses Tim Trudgian's cited prime result; gauge-free/union contributors,
+eumemic's 47-row assembly and the PR589 BIT lineage remain credited.
+
+The extracted MathProof sufficient-transfer proof has Dugongue/Codex provenance.
+Mathlib supplies the sufficient real exponential/Taylor/rpow lemmas. These are
+standard methods; no claim that nobody has previously applied them is made.
+
+The vendored native receipt came from PR3734's optional source archive:
+https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/fa041037a3374eaa08feeca0b26a5d6893194147/research/staged544-producer-return/REPLAY-INPUTS.tar.gz
+Its archive and member SHA-256 hashes are documented by the retained upstream
+REPLAY-INPUTS manifest. Bounded replay authenticates the vendored receipt and
+actual words/native frames, not omitted full cache bytes. The archive is an
+explicit optional full-review source, not a hidden runtime dependency.
+
+All exact retained files keep their source-specific attribution and Apache-2.0
+notices. SOURCE-CREDITS.md under vendor/staged544-producer-return preserves
+that package's own predecessor list.

research/staged544-refined-endpoint/OVERLAP.md

@@ -0,0 +1,7 @@
+# Scope and prior work
+
+This is a precision refinement of PR3857, head ef4315b8caa605e47a2515004845eb2d2ed71a86. It uses the unchanged PR3815 T360 owner allocation and PR3734 staged544 native supplier, with the same normalized profile as PR3802. No new circuit, physical packing, independent proof method, or method priority is claimed.
+
+The team refreshes open contributions during work; publication must recheck the then-current supported frontier. This draft itself does not assert exhaustive Discussion coverage or absence of overlap. Historical predecessor intake is preserved at predecessor/OVERLAP.md and is not a current freshness claim.
+
+The proposed improvement is only the strictly larger certified conditional endpoint in CLAIM.json. All physical, compiler, hosting, precision, exact recovery, analytic transfer and BIT premises remain as in PR3857. The unrelated fiber-norm proposal is excluded. No PR or selected-record change has been made for this draft.