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
19 changes: 18 additions & 1 deletion docs/ci-verification.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,23 @@
# CI verification

## Current selected-family replay: #5599
## Current selected-family replay: #6030

The [selected record](../certificates/selected-result.json) binds conditional
κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md),
[validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json),
and [explicit source closure](../certificates/frontier6030-source.json).
`make frontier6030-verify` follows that source-bound selected replay. The review
separates retained normal primary macOS/Linux evidence from fresh independent
word/invoice/native, original caller, adapted caller and optimized primary checks.
Consult its receipts for exact commands, source heads and limits; the #5599
checkpoint below retains its own historical replay details.

The five inherited framework assumptions remain. Neither the full uniform word
nor a complete rounded multiplier is materialized. A source/metadata check is
not an operator replay or a formal theorem proof. Routine research submissions
do not need to rerun this selected-family replay.

## Historical selected-family replay: #5599

The [selected record](../certificates/selected-result.json) binds conditional
κ = 0.00310045 to the [proof review](research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md)
Expand Down
2 changes: 1 addition & 1 deletion docs/research/current-status.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Current reviewed status

Selected conditional κ: **0.003125804 = 781451/250000000**, DreamingOfClouds'
Selected conditional κ: **0.003125804** = 781451/250000000, DreamingOfClouds'
PR6030 on the cumulative P104 construction. The complete caller counts 13,444
productive fields and 66,834 paid calls. The saving is about 0.81775% above the
preceding selected PR5599 claim 0.00310045.
Expand Down
167 changes: 167 additions & 0 deletions research/spectator-row-reservoir/PROOF.md

Large diffs are not rendered by default.

64 changes: 64 additions & 0 deletions research/spectator-row-reservoir/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
# Complete spectator rows remove the active-axis stock restriction

**Constructive conditional interface theorem, with an exact reference. No new κ.**

A global Hadamard supplier can take its row prefix and compact controls from complete spectator coordinates. It can complete every selected axis in one outer invocation, with one padding by less than two, and restore the original coarse layout before the next diagonal. The prefix may be much larger than the active width.

Using the retained SUPPORT-ROUTER sparse extension, the construction maps the h complete K-bit active neighborhoods to their destination slots, then completes that map on their union. Only **2hK coordinate positions** can move, regardless of the row-prefix length or gather distance. The retained paid support router therefore preserves the supplier's exponent. This is a concrete replacement for active-axis reservation and deferred completion, with the full layout and cost proof in [PROOF.md](PROOF.md).

For total simultaneous stock

$$\log_2Q=O(h^\nu p^\zeta\operatorname{polylog}p),$$

at width h=Θ(p^x), the new fit test is **νx+ζ<1**, using the ambient Θ(p)-bit address. It requires no stock cutoff h≥p^(ζ/(1−ν)) and no individual-axis fallback caused by row reservation. Existing coordinates supply the rows; there is no 2^R volume multiplier.

## Significance for researchers

This opens a larger supplier/representation contract than allocating rows inside the active axes. For hypothetical completed U=B=.02 suppliers with guard exponent ρ=3/2 and stock h^(1/2)p^(3/5) polylog(p), active-axis allocation would require β>6/5. The spectator construction instead gives a passing **κ=.011 interface**, with global stock power 217/240<1 and grouped stock power 157/240<1. The stronger finite suppliers remain missing; the example is a sufficient target for their implementation, not a new .011 multiplier.

More generally, put M=min(U,B,1/32), and

$$E=\min(1,1/\rho,(1-\zeta)/\nu)$$

for ν>0; omit the last term for ν=0 and require ζ<1. The changed wrapper's 60 strict exponent predicates admit rational witnesses exactly when `E>1/2` and `OLD<κ<ME`. All nine source outer savings remain unchanged. [Nick Petalas](https://github.com/petalas)'s [PR5984](https://github.com/CrocSwap/integer-mult-bounds/pull/5984) supplies the unchanged-ledger result; the new contribution is the constructive ambient stock interface. [PR6062](https://github.com/CrocSwap/integer-mult-bounds/pull/6062) studies the earlier active-axis/fallback policy.

## Actual caller and retained obligations

The scientific base is canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`, selected PR6030 at κ=.003125804, priority 8. The retained tensor compiler has the same H schedule on every coarse label, with label dependence in diagonals between completed calls. The compact callee returns identity on row/control/spectator coordinates for arbitrary incoming coefficients. These exact source facts are pinned in [SOURCES.json](SOURCES.json).

The wrapper must run globally on the complete dyadic tensor. A fixed-label microbox is not enough. It must use the product of nested stock, a row-independent completed kernel, paid support routing, padding deletion and inverse exposure before the next diagonal. A stronger target still needs the corresponding paid BIT router; the selected .0034 primitive does not automatically fund .011 routing. Rounded callees need their explicit completed-error and padding-disposal guarantees. Native, compiler, restoration, fixed-tape, precision and analytic hypotheses remain; the five selected assumptions are not discharged.

The executable planner and indexed exact reference implement the new geometry and call boundary. They do not execute the selected finite supplier or a fixed-tape multiplier. The current ζ=0 construction gains a simpler no-deferral outer interface; its selected exponent is unchanged.

## Evidence and reproduction

[RESULT.json](RESULT.json) records:

- 600 sparse coordinate plans, including overlapping original/destination neighborhoods;
- all 384 Gaussian operator basis columns for every one-bit source location at six address bits, checked against an independently written column formula;
- 60 complete arbitrary Gaussian-dyadic payload fixtures, with actual full-row padding, internal dirty-row cycling, zero return, inverse exposure and surrounding address-dependent diagonals;
- seven rejection controls for missing inverse, row-dependent endpoint, early coarse diagonal, incomplete microbox, nonzero padded return, insufficient ambient space and maximum-only stock;
- 1,920 rational outer witnesses checking all 60 predicates, including points 10^-24 below the supremum;
- six encoded production layouts checking prefix/control/active capacity, source K guards, original long-axis neighborhoods, router reservoirs and protected suffixes at log2 p=480,960,1920.

The production checks manipulate compressed integer counts. The small semantic fixtures use K=G=1 to keep every address executable; they do not claim those small values meet the production compact-control guard. The all-size result uses the written proof. No independent human or proof-assistant review is claimed.

From the repository root, CPython 3.12 and the standard library:

```sh
python3.12 -B scripts/research_package.py --package research/spectator-row-reservoir
python3.12 -I -B research/spectator-row-reservoir/verify.py
python3.12 -I -O -W error -B research/spectator-row-reservoir/verify.py
```

The registered normal and optimized replays are read-only. `--emit` prints a fresh receipt. Coordination: [Discussion6056](https://github.com/CrocSwap/integer-mult-bounds/discussions/6056). Scope, source freshness and next questions are in [TASK.json](TASK.json).

## Open next questions

1. **Install the prefix planner at a literal global-H call.** Export its selected neighborhoods, complete product Q, physical record/suffix layout and returned endpoint. This would bind the constructive interface to a production caller. Retained physical routing and callee admission remain prerequisites.
2. **Use the larger ambient stock allowance in a new supplier.** First find a fully charged finite construction whose favorable moment has been unusable because of active-axis stock. The new target is νε+ζ<1, with the actual precision guard and complete BIT/complex budgets. No such stronger construction is supplied here.
3. **Bind a rounded callee to the same return boundary.** First check one call's complete error, common-grid or disposal contract and padding return. Ideal row independence alone is not an error proof.

## Credit

Prepared by [zxv](https://github.com/zxv), with substantial OpenAI Codex assistance in proof, implementation, source review, verification and writing. Apache-2.0. Retain the compact-layout/common-frame, global-H tensorization, support-router/adversarial audit and finite-template complete-stock lineage. In particular, credit [Vlado Vojdanovski](https://github.com/Vlado-V)'s PR1673, [Jeremy Kothe](https://github.com/jeremykothe2)'s PR1758, [Chafik Boukhalfa](https://github.com/chafreaky)'s PR1786, PR4359's mixed/stock/semantic-precision framework, [DreamingOfClouds](https://github.com/DreamingOfClouds)'s selected PR6030, [Nick Petalas](https://github.com/petalas)'s PR5984 and the retained Harvey–van der Hoeven/OpenAI manuscript sources. No predecessor bytes are changed.
112 changes: 112 additions & 0 deletions research/spectator-row-reservoir/RESULT.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,112 @@
{
"arbitrary_payload_fixtures": 60,
"complete_gaussian_basis_columns": 384,
"constructive_example": {
"margins": {
"boundary_algebraic_matrix": "5/64",
"fused_gaussian": "114969/292000",
"global_coordinate_router": "106/5475",
"group_bit_router": "258703/657000",
"group_scans": "1/2",
"main_transform": "139/12000",
"microbox_face_corrections": "4697/60",
"polynomial_products": "73/120",
"sparse_union_movement": "31/64"
},
"minimum_strict_slack": "7/43800",
"old_active_stock_boundary": "6/5",
"parameters": {
"a": "106/5475",
"b": "431/21900",
"beta": "13/120",
"bit_saving": "1/50",
"complex_uniform_saving": "1/50",
"epsilon": "73/120",
"kappa": "11/1000",
"layout": "1597/24000",
"nu": "1/2",
"q": "139/7300",
"r0": "7/320",
"rho": "3/2",
"stop": "7/862",
"zeta": "3/5"
}
},
"controls": {
"coarse_diagonal_before_restoration": "rejected by exact Gaussian output",
"incomplete_microbox": "rejected by explicit contract check",
"insufficient_ambient_space": "rejected by explicit contract check",
"maximum_instead_of_product": "rejected by product divisibility",
"missing_inverse": "rejected by exact Gaussian output",
"nonzero_padded_return": "rejected by explicit contract check",
"row_dependent_endpoint": "rejected by exact Gaussian output"
},
"encoded_production_layouts": [
{
"address_bits_log2": 476,
"log2p": 480,
"required_bits_log2_upper": 468,
"row_bits_log2_upper": 468,
"stock_power": "217/240",
"width_power": "73/120"
},
{
"address_bits_log2": 476,
"log2p": 480,
"required_bits_log2_upper": 348,
"row_bits_log2_upper": 348,
"stock_power": "157/240",
"width_power": "13/120"
},
{
"address_bits_log2": 956,
"log2p": 960,
"required_bits_log2_upper": 905,
"row_bits_log2_upper": 905,
"stock_power": "217/240",
"width_power": "73/120"
},
{
"address_bits_log2": 956,
"log2p": 960,
"required_bits_log2_upper": 665,
"row_bits_log2_upper": 665,
"stock_power": "157/240",
"width_power": "13/120"
},
{
"address_bits_log2": 1916,
"log2p": 1920,
"required_bits_log2_upper": 1776,
"row_bits_log2_upper": 1776,
"stock_power": "217/240",
"width_power": "73/120"
},
{
"address_bits_log2": 1916,
"log2p": 1920,
"required_bits_log2_upper": 1296,
"row_bits_log2_upper": 1296,
"stock_power": "157/240",
"width_power": "13/120"
}
],
"geometry_cases": 600,
"max_fixture_row_bits_per_active_bit": "3",
"outer_predicates": 60,
"outer_witnesses": 1920,
"scope": "Constructive conditional spectator-prefix theorem and exact indexed reference. Retained router/callee/tape/precision/analytic contracts remain. No new finite supplier, kappa or full multiplier.",
"source_sha256": {
"certificates/frontier6030/CLAIM.json": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e",
"notes/batched-complex-rows.tex": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c",
"notes/compact-control-layout.tex": "2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87",
"research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md": "bd5b06eca043c5c871227264f6a954473c55cd16ec85bb420ff538fb8ec1d8d6",
"research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/SUPPORT-ADVERSARIAL-AUDIT.md": "b1290f8720bf075ea2ad58d6070f3e1fc95c0155f8e33b165bc13439bbb9222d",
"research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/SUPPORT-ROUTER.md": "6ddb322e11883c1177ba6cd1a77d23a1dac827d7290b32eaf642457b1d762a54",
"research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/TENSOR-COMPILER.md": "4d3b8466598a864a234b978e25976648d4e761840aad9153dd18d73d3dfe4d15",
"research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779",
"research/p104-helper470-twin-rung-removal/pricing.py": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710",
"research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15"
},
"status": "PASS_SPECTATOR_ROW_RESERVOIR"
}
78 changes: 78 additions & 0 deletions research/spectator-row-reservoir/SOURCES.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
{
"schema_version": 1,
"base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
"files": [
{
"path": "certificates/frontier6030/CLAIM.json",
"usage": "input",
"git_blob": "f32ff3779274a349dc8af2e84a4c6234c6d62406",
"sha256": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e"
},
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
"sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
"sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
},
{
"path": "notes/batched-complex-rows.tex",
"usage": "input",
"git_blob": "e13bd96eb29bdc6526f10dc32e0a146bc17848a4",
"sha256": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c"
},
{
"path": "notes/compact-control-layout.tex",
"usage": "input",
"git_blob": "16f4d233471a7d189163ae7e7902becadecbba64",
"sha256": "2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87"
},
{
"path": "research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md",
"usage": "input",
"git_blob": "72404c42d77d4267105e8528cecff3327dfdd38c",
"sha256": "bd5b06eca043c5c871227264f6a954473c55cd16ec85bb420ff538fb8ec1d8d6"
},
{
"path": "research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/SUPPORT-ADVERSARIAL-AUDIT.md",
"usage": "input",
"git_blob": "80b2afa7433b3139ac926047012658ea500b4a5d",
"sha256": "b1290f8720bf075ea2ad58d6070f3e1fc95c0155f8e33b165bc13439bbb9222d"
},
{
"path": "research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/SUPPORT-ROUTER.md",
"usage": "input",
"git_blob": "4f39fa9eaf553d1df5111de8c19bcf5bf9829c2b",
"sha256": "6ddb322e11883c1177ba6cd1a77d23a1dac827d7290b32eaf642457b1d762a54"
},
{
"path": "research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/TENSOR-COMPILER.md",
"usage": "input",
"git_blob": "19efb9cb1c5a738e57caadf2dd6f5611af1bc78a",
"sha256": "4d3b8466598a864a234b978e25976648d4e761840aad9153dd18d73d3dfe4d15"
},
{
"path": "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md",
"usage": "input",
"git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535",
"sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779"
},
{
"path": "research/p104-helper470-twin-rung-removal/pricing.py",
"usage": "input",
"git_blob": "65bb723f8558dc60ff92764db1a43d8bf438aa09",
"sha256": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710"
},
{
"path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py",
"usage": "input",
"git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59",
"sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15"
}
]
}
Loading
Loading