Skip to content
Open
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,8 +1,25 @@
# CI verification

## Current selected-family replay: #6030
## Current selected-family replay: #7000 with #7001

The [selected record](../certificates/selected-result.json) binds conditional
κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md),
[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json),
and [explicit source closure](../certificates/frontier7000-source.json).
`make frontier7000-verify` follows that exact-source selected replay. The review
reuses eleven authenticated preceding executions and records seven fresh serial
application, scalar and complete native-catalogue executions. The earlier
monolithic timeout is retained separately and is not completed coverage.
Consult the receipts for exact commands, source heads and limits.

The five inherited framework assumptions remain. No complete uniform word,
literal multiplier execution, independent human proof or formal-kernel proof
is asserted. Routine research submissions do not need to rerun this
selected-family replay. The sections below preserve historical checkpoints.

## Historical selected-family replay: #6030

The [historical checkpoint](../certificates/checkpoints/frontier6030.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).
Expand Down
8 changes: 8 additions & 0 deletions research/bit-terminal-main-bank-stock/AUDIT.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{
"canonical_word": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78",
"classes": 110,
"outside_canceled_but_unpaired": 40,
"outside_duals": 70,
"status": "PASS_PROJECTIVE_NORMAL_SET_SWEEP_AND_MARKED_SUFFIX",
"stock": 0
}
46 changes: 46 additions & 0 deletions research/bit-terminal-main-bank-stock/PROOF.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
# No same-midpoint main terminal funding in the fixed BIT word

**NO VERIFIED GAIN.** On the exact #6726 native word retained by #7001, the 22 rank-six-to-eight public main terminal banks cannot supply even one additional majority helper split in the declared fixed-word transfer model. The negative holds for every rational rank-seven midpoint, including midpoints absent from the source, and grants all literal and virtual coframe observations at arbitrary clocks. The complete optimistic raw margin stays negative at the exact campaign target.

## Declared transfer

The old word has 659 public roles, 237 owned roles and 34,137 events. A terminal bank is the last paid chart entry along a surviving public field lineage, following literal SWAPs. A normalized ADD changes the row on its destination without copying the paid bank. The main stock consists of the 22 public main outputs whose terminal bank enters the full rank-eight frame from rank six. The helper group G consists of the 410 original arbitrary rank-eight helper coordinates with boundary frames (0,1). Their old normalized endpoint is identity.

Keep the old normalized scalar actions, contacts, ownership, old paid jobs and productive nonhelper targets fixed. A candidate subdivides a selected main terminal bank into two positive rank-one children at one rational rank-seven midpoint, using its late child to supply a new independent helper continuation. Each such transfer must restore its own outside components and replace its own removed helper degree of freedom. Several disjoint transfers may be counted, each satisfying this local contract. It may gather and compensate using coframed linear combinations at that same midpoint. It must preserve the original main output and every external coordinate outside G. The coefficient maps are exact normalized F₂ maps. The inherited rational chart and all-column physical assumptions remain the basis for this necessary gate.

The envelope allows every literal coframed row across all old clocks, even when the clock is unusable. It additionally virtualizes all 185 subdividable rank-eight final public terminal banks, including main, majority and minority lineages. For each compatible midpoint it supplies the old normalized prefix row and suffix response of every such pivot. It ignores simultaneous placement and clock order and grants free holding, mixing, restoration and ownership. This only increases capacity. The original main pivot can retime inside its unchanged owner contact interval. Its normalized row and response are constant there, since no intervening operation touches it. The proof leaves cross-chart corrections, rewritten normalized contacts, extra virtual nonterminal or erased-bank subdivisions, joint corrections that close only across several selected main banks, and different paid primitives open.

## Complete rational geometry

Let A be the rank-six entrance of one selected main bank and B any eligible virtual bank's entrance. A rational rank-seven midpoint M is compatible precisely when it contains A, and it can host another virtual bank precisely when it contains B. The full rank-eight exit contains every such M.

A midpoint equal to a literal rank-seven chart is checked directly. Otherwise it has no old literal occupants in the unchanged word. If it contains some B outside A, then (A+B=M), since the join is strictly larger than rank six and lies in a rank-seven space. Thus every such midpoint is one of the finitely many rank-seven joins of A with another virtual entrance. Every other midpoint has exactly the virtual entrances already contained in A, so one generic class covers them. This yields 44 literal, 44 new-join and 22 generic bank/midpoint incidences. Each source chart has a distinct exact rational span. The independent audit obtains the same classes by solving projective normal equations in the two-dimensional annihilator of A.

## Coefficient gate

For one bank i and one midpoint, let P be the span of every granted coframed prefix row. Let S contain the corresponding literal suffix responses and all compatible virtual suffix responses other than i. Let (s_i) be the selected main pivot's suffix response. Any new helper continuation using the funded late child has coefficient one on this compulsory pivot in characteristic two. Copies to other coframed positions may add any vector of S. Preserving the arbitrary main outputs and the other outside coordinates forces the resulting response to lie in

```text
D_i = (s_i + S) intersect span(G).
```

The retired old helper value is a group-pure linear form in
(C=P\cap\operatorname{span}(G)). For an independently restored transfer, the
remaining old helper map annihilates its selected continuation direction (d)
in (D_i). The rank-one return (d c^T) must restore that direction in the
unchanged helper identity. Applying the identity to (d\ne 0) gives
(c^T d=1). Testing (C) against the linear span of (D_i) further grants
freedom. A joint transfer with several shared compensation directions would
need a separate matrix test and is outside this bound.

For 70 classes, the exterior of (s_i) is outside the span of all other exteriors. The receipt includes an exact parity functional supported outside G that annihilates every other exterior and evaluates to one on (s_i). For the remaining 40 classes, outside cancellation is possible but the exact pairing against the full group-pure prefix span is zero. Thus none of the 22 banks can supply a direction, and the simultaneous stock of individually admissible transfers is zero. The independent audit rebuilds the word with set-valued rows, checks all parity functionals and marks the compulsory pivot in a transposed nuisance-coordinate nullspace calculation.

## Paid consequence

The full #7001 invoice remains charged. A terminal rank-preserving subdivision of a rank-eight helper after traversing rank a has ideal net credit (H_{a+1}-H_1-H_8+H_{8-a}) per native invocation at the most favorable first subpiece. Here (H_r=r^{1-kappa}). The later productive gains cancel the later paid children. The result grants this ideal credit to all eligible majority terminal banks and grants all 27 smaller helpers full free rank-one refinement. All 36 old native invocations are charged. The resulting upper is approximately −4.676835409452486 at target 0.0040075385047236, and −4.910335615712435 at stricter trial 0.004008162992724. It needs at least 21 of the 22 added main banks at target, or all 22 at the stricter trial. The exact compatible stock is zero even under the broader coefficient envelope. No physical route or new candidate was built.

## Scope and predecessors

The Round 18 pointwise bound counted the 22 terminal banks, priced their hypothetical credit and excluded direct same-entrance terminal exchanges. This result permits different entrances sharing a new common rank-seven span and all coframed compensation clocks, while retaining the literal normalized schedule. [#7202](https://github.com/CrocSwap/integer-mult-bounds/pull/7202) at `b32355e241c7e4dcb413cb20a0b8c8ed3d163f58` bounds three-child IDLE volume via a cover-orbit invariant grade. [#7199](https://github.com/CrocSwap/integer-mult-bounds/pull/7199) at `54b76434dd07ecfdeeaa5958268693f176f37e65` sharpens prime-power cyclotomic precision. The terminal coefficient and ownership conditions concern a distinct operation.

Credit CubeJerry's [#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001), [#6726](https://github.com/CrocSwap/integer-mult-bounds/pull/6726) for the literal native source, the causal helper-split contributors and Clear1nsight [#7161](https://github.com/CrocSwap/integer-mult-bounds/pull/7161) for the prefix/suffix formulation, Nick Petalas [#7175](https://github.com/CrocSwap/integer-mult-bounds/pull/7175) for the concave helper tariff, and Round 18's terminal-stock pricing. OpenAI Codex materially assisted.
51 changes: 51 additions & 0 deletions research/bit-terminal-main-bank-stock/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
# Bound BIT main-terminal transfer stock across rank-seven charts

**NO VERIFIED GAIN. The κ change is 0%.** For the retained #7001 BIT native
word, no one of the 22 main rank-six-to-eight terminal banks supplies a
qualifying pure helper transfer under the fixed normalized contacts and the
independently restored single-chart compensation contract. The map covers 44 literal chart classes,
44 new pairwise-join classes and 22 generic classes. It grants every
compatible one of 185 virtual public terminal pivots, regardless of clock.

The signed moment still falls short by about 4.676835409452486 at
κ = 0.0040075385047236 and 4.910335615712435 at the stricter raw trial. The
target would need at least 21 of 22 such transfers, before charging any
additional setup, routing, ownership, restoration, precision or tape work.
See the [proof](PROOF.md), [directed receipt](RESULT.json) and
[independent audit](AUDIT.json).

## Clean replay

From the repository root with CPython 3.12 and assertions enabled:

```sh
python3.12 -B scripts/research_package.py --package research/bit-terminal-main-bank-stock
```

The checker authenticates the exact native word, invoice and directed interval
arithmetic from canonical #7001 paths. It reconstructs terminal ownership and
all coefficient classes. A separate projective-normal enumeration and
marked-pivot elimination checks every class. No external data, prior run state
or extra Python packages are required.

## Open next questions

Could changing the bank graph supply a new helper response direction? First
enumerate the full compatible stock of already paid nonterminal and erased
bridges. Authenticate every prefix and suffix coefficient, then count distinct
owners and charge routing and restoration before selecting a prototype. This
package keeps those bridges, cross-chart corrections and scalar contact changes
outside its scope.

## Credit

CubeJerry [#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001)
supplied the retained word and tariff. The native and delayed-cover lineage
includes [#6726](https://github.com/CrocSwap/integer-mult-bounds/pull/6726),
[#6834](https://github.com/CrocSwap/integer-mult-bounds/pull/6834) and
[#6980](https://github.com/CrocSwap/integer-mult-bounds/pull/6980).
[Round 18](https://github.com/CrocSwap/integer-mult-bounds/discussions/7111#discussioncomment-19540580)
supplied the terminal funding question and initial price.
Clear1nsight [#7161](https://github.com/CrocSwap/integer-mult-bounds/pull/7161)
supplied the comparable complete witness. OpenAI Codex and subagents materially
assisted the proof, replay and independent audit. Apache-2.0.
Loading
Loading