Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
109 changes: 109 additions & 0 deletions research/unconditional-moment-crosscheck/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,109 @@
# Independent numerical cross-check of PR4100's exact-root and paid-power ledger

This package independently recomputes the finite arithmetic layer behind the
headline exponent of PR #4100 (`research/unconditional-batched-crt`, retained
head `337d04939571a637aeab54a0f58f54fde811663a`). It re-implements the
moment certificate from scratch — its own rational logarithm and exponential
interval enclosures, its own bill evaluator and root bisection — and imports
no code from the audited package or from `staged544-mixed-fourth-entry/vendor`.
Constants are transcribed from the prose of PR4100's `PROOF.md` ("Paid powers"
and "Time" sections); the child histogram and the conditional-exponent
benchmark are read from the pinned PR4088 `RESULT.json`
(`research/staged544-mixed-fourth-entry/RESULT.json`).

## What was checked (and what it established)

For the profile `{1:8060060, 2:2310120, 3:751813, 4:327210, 5:66425,
8:25920, 48:138492}`, width `m = 73` and comparison count
`W = 896 × 360 = 322,560`, with the stated candidate

```text
b = .001730979115670792472760579929302792893760378764
kappa = .00173097911567079247276057 (the 26-decimal-place truncation of b)
```

the independent enclosure proves the finite statements:

1. `bill(a) = Σ_r n_r (r/73)^(1−a) / W` satisfies `bill(b) < 1` with
certified margin at most `-1.800e-48` and `bill(b + 1e-48) > 1` with
margin at least `+1.030e-48`. The model root therefore lies strictly
inside `(b, b + 1e-48)`; the 90-digit bisection localizes it to
`b + 6.363e-49`, agreeing with the margin ratio `1.800/(1.800+1.030)`.
2. `bill(kappa) < 1` with margin at least `2.815e-26`; also
`bill(a_eff) < 1` and `bill(q) < 1` for the package's `a_eff` and `q`.
3. All twelve paid-power slacks (`1 − kappa − power`) are strictly positive
and all fifteen side-condition slacks are strictly positive, recomputed
as exact rationals from the primitives stated in `PROOF.md`.
4. All five obsolete-route rejects (`old_Vd_crt`, `old_g_union_scans`,
`old_per_record_d_chirp`, `old_theta_chirp_guard`,
`no_group_gap_membership`) remain strictly negative at the claimed point.
5. The bootstrap constants reproduce exactly:
`a1 = c(1−c) = .00173039532444` and
`a2 = c(1−c²) = .001733394791695384296` for `c = 8667/5,000,000`, and
`7^16 < 2^45`.
6. The exact gap over PR4088's published conditional exponent reproduces:
`kappa − conditional_kappa = 5.700000000000000000001e-25 > 5.7e-25`,
and the profile agrees with the pinned PR4088 `RESULT.json`.

Controls (all rejected): an inflated rank-1 count, a bracket shifted up by
`1e-12` (which excludes the localized root), a root claimed at or above
`b + 1e-48`, and an unrounded `kappa` equal to `b`.

## Scope — exactly what this is

This is a **finite numerical audit of stated arithmetic claims** at the
retained source heads. It confirms that PR4100's exact-root certificate,
paid-power ledger and headline comparison gap reproduce under a second,
independent implementation. It does **not** validate the all-size arguments:
the CRT total repair (audited separately in #4169), the free-algebra lift in
`COMPLEX.md`, the precision/conditioning and fixed-tape obligations, and the
physical caller/realization premises all remain open. Nothing here is a new
selected result, a supplier admission, or a change to the selected frontier.
The selected conditional κ remains `0.001672660197076918`.

## Related open work (numerically checked)

- **#4100** (audited predecessor): the claims reproduced here are its own
stated numbers at head `337d049`.
- **#4088** (`staged544-mixed-fourth-entry`): source of the pinned profile
and `conditional_kappa`; both agree with the values used by #4100
(asserted in the verifier).
- **#4091 / #4170**: #4170 reports remaining headroom `1.140318244487202e-9`
of the #4091 pooled ceiling over the retained #4088 fill. Agreement check:
`0.00173097911567079247276057 + 1.140318244487202e-9 =
0.00173098025598903696000259… ≈ 0.001730980256`, matching the #4091
ceiling root quoted in the family record. The two audits study different
objects (pooled fixed-inventory ceiling vs this article's moment ledger)
and no number here contradicts #4170.
- **#4169**: audits the compact CRT repair inverse of the same #4100 head.
Complementary proposition; no overlapping number.

## Reproduce

From the repository root, with Python 3.12:

```sh
python3.12 -B research/unconditional-moment-crosscheck/verify.py
```

Expected: `PASS_UNCONDITIONAL_MOMENT_CROSSCHECK` and the JSON receipt above.
Runtime is well under one second. The registered check is
`python3 -B scripts/research_package.py --package research/unconditional-moment-crosscheck`.

## Open next questions

1. Can the free-algebra lift in `COMPLEX.md` be stated as one quantified
proposition at its actual caller and proved or falsified? (The numerical
layer checked here says nothing about it.)
2. Does the localized root margin (`b + 6.36e-49`) leave any room for the
chronological (non-pooled) fill to attain the #4091 pooled ceiling that
#4170 measured as remaining headroom? This package does not answer it.
3. Is the localized model root (about `b + 6.4e-49`) attainable by a
chronological (non-pooled) fill, or does it remain a pooled-inventory
optimum, as #4170's remaining-headroom analysis suggests for the related
#4091 ceiling? This package does not answer it.

Prepared by Nick Petalas with AI assistance. Apache-2.0. Predecessor
attribution is retained: the audited construction is PR #4100 by Cinna Davis
and its pinned lineage; the profile and benchmark come from PR #4088's
retained sources.
48 changes: 48 additions & 0 deletions research/unconditional-moment-crosscheck/SOURCES.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
{
"schema_version": 1,
"base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
"files": [
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
"sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
"sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
},
{
"path": "research/unconditional-batched-crt/README.md",
"usage": "provenance",
"git_blob": "06c9372b0a19ac69066c24c6929fe451705b5a1a",
"sha256": "32727fa6f2e9a32f65d10baae41bf6985a2ea4f72dae5c63d597262c1fc13789"
},
{
"path": "research/unconditional-batched-crt/PROOF.md",
"usage": "provenance",
"git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c",
"sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060"
},
{
"path": "research/unconditional-batched-crt/check_composition.py",
"usage": "provenance",
"git_blob": "eadf3a61abc1a21f469e049b4f9adb137ac96af0",
"sha256": "6a4be3072016bb08b3660b8c3bd2e89722dc19b0ebe844d6a0aa4084d0206145"
},
{
"path": "research/staged544-mixed-fourth-entry/RESULT.json",
"usage": "input",
"git_blob": "1174e25e2ef8f8bc9a0815c43ba5d64c8af08349",
"sha256": "6346ee768637aa9a1891d1d61d800d640235420b320fb7e659d1bf664ec42b3d"
},
{
"path": "research/staged544-mixed-fourth-entry/vendor/exact_root.py",
"usage": "provenance",
"git_blob": "96dab46ab3404adc92c4b004481759db0c71dfdf",
"sha256": "565e0d7de2fcd7587045f11731dfaba202e18f93e3a7a8178374f4933e502fbe"
}
]
}
80 changes: 80 additions & 0 deletions research/unconditional-moment-crosscheck/TASK.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
{
"schema_version": 1,
"task_id": "uniform-transfer-audit",
"priority_revision": 7,
"base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
"original_card": {
"id": "uniform-transfer-audit",
"question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
"starting_points": [
"docs/research/research-family-status.md",
"certificates/selected-result.json",
"research/unconditional-batched-crt/README.md"
],
"methods": [
"Prove one missing implication with explicit quantified hypotheses.",
"Find an exact counterexample at the claimed interface boundary."
],
"acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
"first_step": {
"command": [
"python3",
"-B",
"scripts/research_baseline.py"
],
"expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
"inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
"scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
},
"first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
"bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
"allowed_variations": [
"One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
],
"scope_change_triggers": [
"Replacing a quantified obligation with another finite smoke test.",
"Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
],
"overlap_terms": [
"uniform transfer",
"all-size",
"precision",
"4100",
"unconditional-batched-crt"
],
"existing_checks": [
{
"scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
"evidence": "research/unconditional-batched-crt/README.md",
"remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
"status": "author-checked",
"source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
"selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
}
]
},
"scope_status": "refined",
"actual_scope": "Not one all-size implication but the finite arithmetic substrate underneath them: an independent re-implementation of the exact-root certificate, paid-power ledger and headline comparison gap of PR4100 at its retained head 337d04939571a637aeab54a0f58f54fde811663a. Established as finite numerical facts under a second implementation: the moment root of the pinned profile lies strictly inside (b, b+1e-48) with b = .001730979115670792472760579929302792893760378764 (localized at b + 6.363e-49); bill(kappa) <= 1 - 2.815e-26; all twelve paid-power slacks, fifteen side slacks positive and five obsolete-route rejects negative as exact rationals; a1, a2 and the 7^16 < 2^45 bound reproduce; kappa - PR4088 conditional_kappa = 5.700000000000000000001e-25 > 5.7e-25.",
"scope_change_reason": "The card's quantified implications (CRT total repair, free-algebra lift, precision/conditioning, fixed-tape cost) are universal statements; the CRT repair was independently claimed in #4169 before this session. This session instead discharges the precondition every such audit leans on: that the package's own exact-root and cost-margin arithmetic reproduces under an independent implementation, so a later implication audit is not built on unrechecked numbers. The deliverable is explicitly finite, not an implication proof.",
"bottleneck_link": "PR4100 is the only retained proposal claiming to discharge the transfer premises for an exponent above the selected result. Its headline rests on an exact-root certificate and a twelve-row paid ledger; this audit shows those stated numbers are internally reproducible (finite layer), while the universal premises remain open and unaddressed here.",
"budget_minutes": 60,
"stop_rule": "Stop at the endpoint sign certificates, the localized root interval, the exact rational ledger reproduction, the gap and truncation checks, and four rejected controls. Do not attempt the CRT repair, the free-algebra lift, any all-size proof, or any kappa claim.",
"outcome": "partial",
"evidence": "verify.py prints PASS_UNCONDITIONAL_MOMENT_CROSSCHECK with the JSON receipt: root_bracket_independent [b+6.363e-49 to 52 decimals], bill margins -1.800e-48 at b and +1.030e-48 at b+1e-48, kappa margin 2.815e-26, full slack dictionaries, gap 5700000000000000000001e-25, four controls rejected. Enclosures: own atanh/Taylor rational interval arithmetic rounded outward at 50 significant digits, far below the 1e-26..1e-48 margins resolved; 90-digit Decimal bisection used only for informational root placement.",
"author": "Nick Petalas",
"ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
"open_questions": [
{
"question": "Does the free-algebra lift of COMPLEX.md hold as a quantified proposition at its actual caller?",
"why_it_matters": "It is the remaining unclaimed all-size proposition of the audited package; the finite layer checked here is necessary but far from sufficient.",
"first_step": "State the lift as one explicit implication with its quantifier domain over widths and read the caller in COMPLEX.md around the arbitrary-width recursion.",
"blocked_by": "Independent acceptance of the lift statement itself."
},
{
"question": "Is the localized model root attainable chronologically, or only by pooled inventory?",
"why_it_matters": "Determines whether the reproduced arithmetic corresponds to any executable schedule; connects to #4170's remaining-headroom measurement.",
"first_step": "Reuse #4170's transfer-audit framing against the profile localized here.",
"blocked_by": "Chronological fill model for the 1090-call fourth entry."
}
]
}
20 changes: 20 additions & 0 deletions research/unconditional-moment-crosscheck/VERIFY.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
{
"schema_version": 1,
"status": "ready",
"python": "3.12",
"requirements": [],
"inputs": [
"research/staged544-mixed-fourth-entry/RESULT.json"
],
"commands": [
{
"argv": [
"{python}",
"-B",
"{package}/verify.py"
],
"timeout_seconds": 120,
"checks": "Independent interval re-verification of PR4100's exact-root bracket (bill(b) < 1 < bill(b+1e-48) with certified margins), localized model root inside (b, b+1e-48), bill(kappa) < 1, twelve paid-power slacks, fifteen side slacks, five obsolete-route rejects, a1/a2/Strassen constants, the exact >5.7e-25 gap over PR4088's conditional exponent, profile agreement with the pinned PR4088 RESULT.json, and four rejecting controls."
}
]
}
Loading