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
1 change: 1 addition & 0 deletions research/pr4626-helper621-check/.gitattributes
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
PR4610-CHECKPOINT-ACTUAL-WORD.json.gz -text
Binary file not shown.
166 changes: 166 additions & 0 deletions research/pr4626-helper621-check/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,166 @@
# Independent check of #4626: helper621 chart change, census delta and arithmetic

This is a scoped check of hexapode's (Pierre-Loic Doulcet's) [#4626](https://github.com/CrocSwap/integer-mult-bounds/pull/4626), head
`e4413c43eeaacdd20be123fdd7d7add53427f028`. #4626 claims conditional κ 0.00302152 → 0.003021569.
It does so by moving helper621's entrance and first scalar contact into the chart A = span{30,429}
on top of the frozen #4610 checkpoint `4b4c75bc`. **No new κ is claimed here.**

## Questions

1. **Ledger.** Is the chart move legal in the native word's own frame bookkeeping? Does it produce exactly the claimed
paid census, helper census and whole cost change 18(H1 + 2H2 − H3 − H4 − H7 + H9)?
2. **Arithmetic.** Do the raw crossing, κ selection, strictification quotients and finite compiler exponent
follow from the full paid profile?

## Method

`verify.py` uses only the standard library and runs in about 2 s. It imports nothing from #4626.

**Inputs.**

- **Word.** The checkpoint word is vendored as `PR4610-CHECKPOINT-ACTUAL-WORD.json.gz`. Its git blob is
`79dad65b`, which is the same blob as #4610's `research/warp-interface-20261022/ACTUAL-WORD.json.gz` at
`4b4c75bc`, #4626's `predecessor/ACTUAL-WORD.json.gz` and #4614's vendored copy. Its SHA256 is pinned in
the verifier.
- **Main evaluators.** Two files from main are used: `joint-helper-lattice/CONTROLLER.json`, read as JSON,
and `clifford_exact.py`, used only to evaluate exact Clifford ranks. Both are pinned in `SOURCES.json`.

**Native side (own frame walker).**

- **Walker test.** Every paid climb is re-derived from the scalar and warp events. On the checkpoint word in
both orientations, the result reproduces all 3,290 shipped climbs as a multiset, plus the census
{1:2201, 2:412, 3:506, 4:135, 5:36, 8:8}.
- **Patch.** The patch is then applied (start[621] := A, frame(event 12704) := A) and the word is re-walked.

**Arithmetic.**

- **Precision.** All values are computed in 80-digit Decimal.
- **Root method.** The crossing is found by Newton iteration. #4615 used bisection.
- **Endpoint signs.** The margin sign is checked at both endpoints of #4626's bracket. Each margin exceeds
1e-60 in absolute value, far above the accumulated rounding error.

## Result: every checked claim reproduces, with two small findings

**Legality.**

- **First contact.** In both orientations nothing touches L621 before event 12704: no scalar, warp, climb,
adapter or centre event. Helper621 starts at ZERO and ends at FULL9.
- **Partner.** L514's previous contact is at ZERO.
- **Next contacts.** L514's next contact is at frame 797 = span{429,70,30}, and L621's is at frame 4329 =
span{25,30,96,426}.
- **Nesting.** A is nested in both. In fact **A equals their intersection**, so it is the largest chart that
both next contacts allow.
- **Scalars.** The scalar opcode and coefficient sequence is unchanged.

**Census delta (both orientations).**

- **Climbs.** Removed: 514: 0→797 (r3) and 621: 0→4329 (r4). Added: 514: 0→A (r2), 514: A→797 (r1) and
621: A→4329 (r2).
- **Paid change.** This gives ΔP = H1 + 2H2 − H3 − H4.
- **New census.** {1:2202, 2:414, 3:505, 4:134, 5:36, 8:8}. All five changed edges have exact Clifford rank
equal to their climb rank.

**Helper census.**

- **Two methods.** All 408 relative helper ranks are computed both by the nested-dimension count and by the
exact Clifford rank of C_final C_start⁻¹, using main's evaluator.
- **Checkpoint.** {4:28, 7:7, 8:47, 9:326}.
- **Patched.** {4:28, 7:8, 8:47, 9:325}. Only helper621 changes, from 9 to 7.

**Whole profile.**

- **Histograms.** The whole paid and target histograms equal #4626's `ARITHMETIC.json`: 64,422 paid calls,
10,928 fields and rank-mass surplus 752.
- **Cost change.** The difference of the whole moment margins equals 18(H1 + 2H2 − H3 − H4 − H7 + H9) to 1e-60.
- **PROOF.md value.** At a = .00302156 the change is −0.004016704251714083738. This lies inside PROOF.md's
interval.

**Finding 1 (cosmetic).** The PR body says the change is "≈ −0.00401665923 at the tested exponent". That
value is attained at a = 0.00302152, the predecessor κ. At the tested exponent .00302157 the value is
−0.0040167155066. PROOF.md's number is correct, and sign and magnitude are unaffected.

**Raw crossing.**

- **New root.** 0.00302157135763930442, inside (0.0030215713, 0.0030215714).
- **Control.** The checkpoint root 0.00302155511144603 reproduces #4610 and #4615.

**κ and compiler.**

- **Tested saving.** It is .00302157, the root floored to 1e-8, and lies only **1.36e-9** below the root.
- **κ.** κ = tested − 1e-9 = 0.003021569.
- **Strictification.** α, γ and δ reproduce all 30 digits #4626 displays. α clears its 1 − 1e-9 threshold
by only 4.15e-10.
- **Compiler exponent.** With step 7·10⁹, j = 48,264 is the least j with (step·j + 1)^1000 < 2^j, checked
in exact integers. Hence H = 337,848,000,000,000.

**Finding 2 (attribution of the gain).** #4626 changes two things: the native profile and the κ-selection
rule.

| Rule | Checkpoint (#4610 `4b4c75bc`) | With helper621 (#4626) |
|---|---|---|
| #4610's rule: ⌊root·10⁸⌋ − 3, gap 1e-8 | 0.00302152 | 0.00302154 |
| #4626's rule: ⌊root·10⁸⌋ − 1e-9, gap 1e-9 | 0.003021549 | 0.003021569 |

Of the +4.9e-8, about +2e-8 comes from helper621. The other +2.9e-8 comes from the compiler-gap retune, which
would apply equally to the checkpoint. The retune spends compiler headroom: tested sits 1.36e-9 below the
root, where #4610 left ≥ 2e-8. That trade is legitimate only if the outer ledger accepts it. Its 54 + 4
outer checks are **not** re-verified here.

**Context.** #4610's own later head claims 0.00302176 from a different joint change on the same checkpoint.
Whether #4626's helper621 move composes with it is not checked here.

## Controls (each must fail)

- **Non-nested chart.** span{30,1} is not nested in the next-contact frames.
- **Entrance only.** Moving the entrance without its contact leaves an A → ZERO edge.
- **Smaller chart.** The 1-dimensional chart span{30} gives a different census.
- **Old helper credit.** The census {…, 7:7, 9:326} is rejected.
- **Wrong κ selection.** #4610's κ rule does not give #4626's κ selection.
- **No idle charges.** Dropping the idle charges moves the root far above the bracket.
- **Wrong exponent.** j = 48,263 does not win.

Local mutation tests of the claims also fail as expected: a wrong chart, the old helper credit, a shifted
bracket, exponent 48,265, and the tested-exponent ΔC value in place of the body's.

## Not covered

- native literal replay of the 632 arbitrary input columns;
- absolute phases and the monomial normalizers of the rank-7 helper target. This check covers the rank only;
the phases are #4626's `verify_native.py` claims;
- the backward-orientation semantics beyond the frame census;
- the 54 strict and 4 functional outer checks, η, and the BIT supplier;
- Lean;
- whether a relative rank-7 helper target with an arbitrary input in chart A is admissible under the supplier
contract. That is the maintainers' call, as for #4610's generator substitution.

## Reproduction

```sh
python3.12 -B research/pr4626-helper621-check/verify.py
python3.12 scripts/research_package.py --package research/pr4626-helper621-check
```

## Open next questions

1. **Supplier contract.** Is the κ-selection retune (gap 1e-8 → 1e-9, tested 1.36e-9 below the raw root)
accepted by the 54 + 4 outer ledger independently of #4626's vendored engine? First step: rerun
`pr4359-p7-padding/.../endpoint.py`'s ledger with an independent parameter derivation. If it is accepted,
the same retune applied to #4610's checkpoint gives 0.003021549 with no native change.
2. **Composition with #4610's later head.** Does helper621's chart move compose with #4610's later joint change
(κ 0.00302176)? First step: check whether that head changes helper621's start, event 12704 or frames
797 and 4329.
3. **Other helpers.** Are there other ZERO-start helpers whose first contact partners' next-contact frames
intersect non-trivially? This chart move would apply to them in the same way. First step: scan all 408
helpers with the frame walker in this package.

## Credit

hexapode / Pierre-Loic Doulcet ([#4626](https://github.com/CrocSwap/integer-mult-bounds/pull/4626)), intqwq /
Cao Yifan ([#4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610)), Cinna Davis
([#4470](https://github.com/CrocSwap/integer-mult-bounds/pull/4470)) and the credited predecessor chain.
pinterbanget's [#4614](https://github.com/CrocSwap/integer-mult-bounds/pull/4614),
[#4615](https://github.com/CrocSwap/integer-mult-bounds/pull/4615) and
[#4616](https://github.com/CrocSwap/integer-mult-bounds/pull/4616) checked #4610's checkpoint. This package
reuses #4615's controller-histogram recipe, reimplemented here.

Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
30 changes: 30 additions & 0 deletions research/pr4626-helper621-check/SOURCES.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
{
"schema_version": 1,
"base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
"files": [
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
"sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
"sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
},
{
"path": "research/joint-helper-lattice/CONTROLLER.json",
"usage": "input",
"git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5",
"sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f"
},
{
"path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py",
"usage": "input",
"git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
"sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962"
}
]
}
112 changes: 112 additions & 0 deletions research/pr4626-helper621-check/TASK.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,112 @@
{
"schema_version": 1,
"task_id": "independent-moment",
"priority_revision": 7,
"base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
"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": "Independently reconstruct #4626's changed paid ledger (helper621 chart move on the #4610 checkpoint word: legality, climb delta, paid and helper census) and recompute its whole-profile crossing, kappa selection, strictification quotients and finite compiler exponent with a different method.",
"scope_change_reason": "Applies the card's generic question to the specific new claim #4626 (head e4413c43), which had no independent check.",
"bottleneck_link": "Independent pricing of #4626's changed ledger prevents an unsupported frontier claim and separates the native gain (+2e-8) from the compiler-gap retune (+2.9e-8).",
"budget_minutes": 60,
"stop_rule": "Stop after the census delta and the arithmetic chain reproduce or a concrete discrepancy is found; native phases, literal replay and the 54+4 outer ledger are out of scope.",
"outcome": "completed",
"evidence": "verify.py: own frame walker reproduces all 3,290 checkpoint climbs; patched census {1:2202,2:414,3:505,4:134,5:36,8:8}, dP=H1+2H2-H3-H4, A = frame797 ∩ frame4329; helper census {4:28,7:8,8:47,9:325} by dimension count and exact Clifford rank; raw root 0.0030215713576 by Newton in 80-digit Decimal; alpha/gamma/delta to 30 digits; least compiler exponent 48,264. Findings: PR body's dC value is at a=.00302152 not the tested exponent; +2.9e-8 of the gain is the compiler-gap retune.",
"author": "lm1909",
"ai_assistance": "Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance.",
"open_questions": [
{
"question": "Does the 54+4 outer ledger independently accept the compiler-gap retune (gap 1e-9, tested 1.36e-9 below the raw root)?",
"why_it_matters": "About +2.9e-8 of #4626's +4.9e-8 comes from this retune, which would apply equally to #4610's checkpoint (0.003021549).",
"first_step": "Re-derive the ledger parameters independently and evaluate research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py's ledger.",
"blocked_by": "nothing"
},
{
"question": "Does the helper621 chart move compose with #4610's later joint change (claimed 0.00302176)?",
"why_it_matters": "#4626 builds on the frozen checkpoint; the two improvements may or may not stack.",
"first_step": "Check whether #4610's later head changes helper621's start, event 12704 or frames 797/4329.",
"blocked_by": "nothing"
},
{
"question": "Which other ZERO-start helpers admit the same entrance/first-contact chart move?",
"why_it_matters": "The move is mechanical given nonzero intersection of both partners' next-contact frames.",
"first_step": "Scan all 408 helpers with this package's frame walker and price each candidate move.",
"blocked_by": "nothing"
}
]
}
22 changes: 22 additions & 0 deletions research/pr4626-helper621-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/joint-helper-lattice/CONTROLLER.json",
"research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py"
],
"commands": [
{
"argv": [
"{python}",
"-I",
"-B",
"{package}/verify.py"
],
"timeout_seconds": 120,
"checks": "Vendored #4610 checkpoint word pin; own frame walker reproduces checkpoint climbs; helper621 chart legality and patched paid/helper census; whole histograms, cost change, Newton raw root, kappa rule, strictification digits, least compiler exponent; rejection controls."
}
]
}
Loading