DONE: compiler exact raw moments

[JoyboyBrian]

DONE (scoped result) / 2026-10-23T07:16:26.022232+00:00 / priority revision 7

All actual raw log moments through degree 24 strictly tighten the chord bounds, with independent Bell/EGF iid formulas. The unchanged degree-23 sufficient coefficient certificate nevertheless fails rigorously at coefficients 1..23; even zero paid excess cannot fix its highest coefficient. This is a fixed-majorant obstruction, not impossibility of the true capped law or a different compiler. No new rank N is emitted.

Public artifact: #5042, exact head 7d09263f63f8a05537a659045dbd7e98ae7237c6, package research/exact-raw-log-compiler. Scientific base f259dabc7d70e0db8d6d36bfda888f008bbfecc1.

Evidence status: author-checked with a separate AI-assisted read-only source/logic review; normal and optimized registered checks, source pins, committed bytes/history and package export checks pass. Exact commands, environments and unrun obligations are in the package. Hosted CI status is separate and is not implied by DONE.

Scope: Replace the bounded-support Bernoulli chord in net-tax-rank-compiler by directed enclosures of the complete actual raw log-rank moment list, combine iid moments by exact Bell coefficients, retain capped-reference paid-excess normalization, and test whether the unchanged native-concentrated-balanced benchmark admits log degree p=23 instead of 24. Keep all native jobs, tensor power, C/kappa, completion/splitting taxes and exit-law premises fixed. If p23 fails, certify the exact coefficient obstruction within this fixed certificate instead of expanding a parameter search.

Next work: see the package's Open next questions and explicit remaining contracts. No new selected frontier, complete multiplication theorem, independent human review or proof-kernel acceptance is asserted. This claim is released.

Credit: zxv structural rank compiler and native PR4453 benchmark; Jacob Alan Sussman Theorem1G; PR4411/4414/4416/4433 compiler/product lineage; Cinna Davis source native contributions and retained authors. Prepared by JoyboyBrian with substantial OpenAI Codex assistance.

{
  "schema": "integer-mult-coordination/v1",
  "kind": "DONE",
  "task": "formal-interface-lemma",
  "scope": "Replace the bounded-support Bernoulli chord in net-tax-rank-compiler by directed enclosures of the complete actual raw log-rank moment list, combine iid moments by exact Bell coefficients, retain capped-reference paid-excess normalization, and test whether the unchanged native-concentrated-balanced benchmark admits log degree p=23 instead of 24. Keep all native jobs, tensor power, C/kappa, completion/splitting taxes and exit-law premises fixed. If p23 fails, certify the exact coefficient obstruction within this fixed certificate instead of expanding a parameter search.",
  "base": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
  "expiry": null,
  "artifact": "https://github.com/CrocSwap/integer-mult-bounds/pull/5042"
}

[JoyboyBrian]

DONE / scoped result / 2026-10-23T08:05:19.897445+00:00

Scoped analytic true-cap obstruction: tail correction <=0.002146686936076 < required correction >0.003093849703915; fixed p23 j23 fails even for exact capped-reference mean and zero excess.

Public artifact: #5070, exact head fd2d388093e3a471c81dbb7ca90c36fd9d1b6dd2, package research/capped-paid-law-obstruction. Scientific base 4c0a359d88f22f05189d51f48387750b801a45d4, priority revision7. Normal/optimized targeted replay, source pins, committed bytes/history and Git-free export checks pass. A separate Astra exact-head proof/source review found no actionable issue. This is AI-assisted evidence, not human or proof-kernel acceptance; hosted CI is separate.

Scope and limitations: Fixed beta=127/125 and witness only; does not reject stronger beta or other certificates. True capped raw reference is bounded below; actual completed paid law is not bounded below. No higher capped moments, histogram convolution, scan, new uniform N, native/outer replay or full multiplication theorem. PR5042 README retained as historical context only; all numerical results independently recomputed from canonical-base inputs.

Credit: zxv net-tax compiler; Jacob Alan Sussman finite compiler; PR4411/4414/4416/4433 and Cinna Davis native lineage; JoyboyBrian #5042. JoyboyBrian with substantial OpenAI Codex assistance. The scoped claim is released; package Open next questions retain remaining obligations. No selected frontier change or full multiplication theorem is claimed.

{
  "schema": "integer-mult-coordination/v1",
  "kind": "DONE",
  "task": "independent-moment",
  "scope": "Decide whether the TRUE capped iid260 raw log-rank law can rescue the fixed p23 coefficient certificate of native-concentrated-balanced. First derive rigorous lower/upper bounds on m1=E[min(Xraw,1)] and compare the exact necessary highest-coefficient capacity. Only if that test permits success, certify capped moments through24 with full paid-excess normalization and all unchanged compiler guards.",
  "base": "4c0a359d88f22f05189d51f48387750b801a45d4",
  "expiry": null,
  "artifact": "https://github.com/CrocSwap/integer-mult-bounds/pull/5070"
}