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
78 changes: 78 additions & 0 deletions research/gate-existence-check/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
# Independent certified check of #4532: adaptive gates at a moment crossing

**Claim type:** an independent certified recomputation of the finite figures. **No new κ.** It covers
dillona's [#4532](https://github.com/CrocSwap/integer-mult-bounds/pull/4532) (head `644607ba`). That PR gives
a sufficient criterion for #4483's gates at the exact moment crossing, together with the critical-root
majorant `L(n) ≤ A n^θ (c + log n)^p`. #4535's κ = 0.003020165 (checked in my #4536) rests on it.

The code is separately written, using the certified interval helpers of my #4529. All figures match
#4532's tables.

## A. The abstract witness

The profile is `W_16 = 1, W_256 = 4; P_1 = 59, P_81 = 1`, with exact crossing `T(1/2) = P(1/2) = 68`.
Parameters: `a = b = 1`, `M = 4096`, `s = λ = 1/4`, `p = 12`, `c = 24`, `ℓ₀ = 128`, `n₀ = 2^{1544}`.

| guard on [1/2, 33/64] | certified | #4532 |
| --- | ---: | ---: |
| mean gap `μ_T(1/2) − μ_P(33/64)` | 4.7649 | ≥ 4 |
| mixed tail `U` | 0.6223559 | < .622356 |
| root tail `V` | 0.6603487 | < .660349 |
| mirror, worst `E_J(33/64)/S_J(1/2)` | 0.010664 | ≤ 1/80 |
| capacity `t·m^{t−1}` | 1/32 (exact) | 1/32 |
| tangent cover `τ(n₀)` | 0.510967 | ≤ 33/64 |
| recurrence lower bound | 272.8579195 | > 272.857919 |
| required `(1−η)/(η−β)` | 155/3 | 155/3 |

The ratio ordering also holds.

## B. The counterexample

The profile is `W_4 = 4, W_64 = 17; P_1 = 4, P_16 = 1`, at `t = 1/2`:

- `T = 144 > P = 8`;
- the mirror ratio is exactly `1/17 < 1/16` (the capacity);
- `μ_P(1/2) = 2 ln 2`, and exactly `T(1/2 − λ)·e^{λμ_P} = 8 + 136·16^{−λ} > 8 = P(1/2)` for every `λ > 0`.

So #4532's tail criterion fails for every `λ`, as it states.

## C. Root applications, with #4483's geometry

| | crossing bracket | mean gap | mirror (bracket) | capacity | mirror (cover) | D | required |
| --- | --- | ---: | ---: | ---: | ---: | ---: | ---: |
| p7 | (.997313, .997314) | 1.723542 | 0.320851 | 0.984544 | 0.321177 ≤ .322 | 0.028590 | 0.023329 |
| p16 | (.996979, .996980) | 1.042285 | 0.562814 | 0.982102 | 0.563147 ≤ .564 | 0.048546 | 0.042808 |

The crossing in each bracket is certified by opposite moment signs, and uniqueness by a positive mean gap.
The U, V, Q, d and ordering guards hold on the critical covers `[root, .997483]` and `[root, .997067]`.
The concavity and tangent-cover conditions hold, and so does the funding `D ≥ (1−η)/(η−β)`.

## Not covered

- #4532's theorem: the integral identities, the existence argument and the critical-endpoint majorant
proof.
- The criterion's "only if" direction, beyond the counterexample.
- The native premises.

## Reproduce

```sh
python3.12 -B scripts/research_package.py --package research/gate-existence-check --check-only
python3.12 -B scripts/research_package.py --package research/gate-existence-check
```

The verifier prints `PASS_GATE_EXISTENCE_CHECK` in about 25 seconds, using only the standard library.

## Open next questions

1. **Combine #4532's critical endpoint with my #4533 retuned geometry.**
- *Why it matters:* at the crossing exponent, a smaller `n₀` also shrinks the finite cutoff in #4535's
absorption.
- *First step:* rerun section C with #4533's p16 witness (`M = 768`, `ℓ₀ = 140`, `p = 3/5`, `c = 400`).

## Credit

- The theorem, the witness and the counterexample are dillona's (#4532), building on #4483.

Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
Apache-2.0.
36 changes: 36 additions & 0 deletions research/gate-existence-check/SOURCES.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
{
"schema_version": 1,
"base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
"files": [
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
"sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
"sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
},
{
"path": "research/compact-joint-compiler/arithmetic/RESULT.json",
"usage": "input",
"git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff",
"sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091"
},
{
"path": "research/higher-moment-strictification/RESULT.json",
"usage": "input",
"git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a",
"sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156"
},
{
"path": "research/rank-convergence/BENCHMARKS.json",
"usage": "input",
"git_blob": "bc58c96abda014c28de91eca3ff10a7d4ec30b32",
"sha256": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850"
}
]
}
100 changes: 100 additions & 0 deletions research/gate-existence-check/TASK.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
{
"schema_version": 1,
"task_id": "independent-moment",
"priority_revision": 7,
"base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
"original_card": {
"id": "independent-moment",
"question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
"starting_points": [
"docs/research/research-family-status.md",
"certificates/selected-result.json",
"research/staged544-mixed-fourth-entry/README.md",
"research/staged-fourth-mixture-ceiling/README.md",
"research/r437-two-window-carrier/README.md"
],
"methods": [
"Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
"Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
],
"acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
"first_step": {
"command": [
"python3",
"-B",
"scripts/research_baseline.py"
],
"expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
"inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
"scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
},
"first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
"bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
"allowed_variations": [
"Reconstruct either a source ledger or a numeric enclosure with a different method."
],
"scope_change_triggers": [
"Importing the primary function and calling its output independent verification.",
"Calling an aggregate histogram or source archive an independently accepted physical supplier."
],
"overlap_terms": [
"independent moment",
"rank histogram",
"exact enclosure",
"2979",
"rank7 joint endframes",
"paired extraction",
"joint lowering",
"4088",
"4091",
"4067",
"staged544-mixed-fourth-entry",
"staged-fourth-mixture-ceiling",
"r437-two-window-carrier"
],
"existing_checks": [
{
"scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
"evidence": "research/staged544-mixed-fourth-entry/README.md",
"remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
"status": "author-checked",
"source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
"selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
},
{
"scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
"evidence": "research/staged-fourth-mixture-ceiling/README.md",
"remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
"status": "author-checked",
"source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
"selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
},
{
"scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
"evidence": "research/r437-two-window-carrier/README.md",
"remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
"status": "author-checked",
"source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
"selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
}
]
},
"scope_status": "refined",
"actual_scope": "Independent certified check of #4532's finite witness, counterexample and root applications.",
"scope_change_reason": "#4535's new kappa rests on #4532.",
"bottleneck_link": "Independent coverage of the compiler behind the newest kappa claim.",
"budget_minutes": 45,
"stop_rule": "Stop at finite figures; #4532's theorem out of scope.",
"outcome": "completed",
"evidence": "All #4532 table figures reproduce: witness D 272.8579195 vs 155/3, U .6223559, V .6603487, mirror .010664<=1/80; counterexample identity; p7/p16 gap, mirror, capacity, D and required.",
"author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
"ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
"open_questions": [
{
"question": "Combine #4532's critical endpoint with #4533's retuned geometry.",
"why_it_matters": "Smaller finite cutoff in #4535's absorption.",
"first_step": "Rerun section C with #4533's p16 witness.",
"blocked_by": "None."
}
]
}
22 changes: 22 additions & 0 deletions research/gate-existence-check/VERIFY.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
{
"schema_version": 1,
"status": "ready",
"python": "3.12",
"requirements": [],
"inputs": [
"research/compact-joint-compiler/arithmetic/RESULT.json",
"research/higher-moment-strictification/RESULT.json",
"research/rank-convergence/BENCHMARKS.json"
],
"commands": [
{
"argv": [
"{python}",
"-B",
"{package}/verify.py"
],
"timeout_seconds": 300,
"checks": "#4532 recomputation: abstract witness guards (gap, U, V, mirror 1/80, capacity 1/32, cover, D > 272.857919 vs 155/3), counterexample identity and mirror 1/17, p7/p16 crossing brackets, mean gap, mirror, capacity and critical-cover guards with funding."
}
]
}
Loading
Loading