Rule out profitable first-read captures of any G20 helper subset (no new kappa)

research/g20-joint-capture-flag-bound/PROOF.md

@@ -0,0 +1,183 @@
+# A flag bound for simultaneous first-read captures
+
+Jerry Chen (@CubeJerry), with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Statement and scope
+
+Fix the PR5708 word pinned in `SOURCES.json`. The 415 retained helpers are
+non-owned wires with index at least 222: 413 have target rank 8, and
+`P = {465, 684}` have target rank 4. Let `t = 1-C` be the **local BIT** moment
+exponent and assume `99/100 <= t <= 1`.
+
+Choose **any subset H** of helpers. Remove each chosen helper's independent
+public input and target credit, hold it zero before its first ADD-source use
+(dropping incoming writes and making its own queries free), and inject one
+arbitrary native-linear payload immediately before that first read. Afterwards
+keep the word's operations, making a query free only when its payload is zero.
+
+Native-linear means a finite F2 sum of terms `M x_i`, with M a native invertible
+address transformation, as in PR6113's payload model. It does **not** mean an
+unrestricted linear operator that need not preserve constant functions.
+Payloads use retained independent inputs. Grant injection, source access,
+scalar operations, frame preparation, storage, final erasure and restoration
+zero cost, and relax retained endpoint equations. These choices favor capture
+under the inherited nonnegative-charge contract. There are no new contacts,
+changed words, noncoordinate input contracts, later reinjections or jointly
+extended dead intervals. The census checks that no helper has a paid query
+after its last source read, so final erasure gives no additional query saving.
+
+Let Δ be saved paid t-moment minus lost target t-moment and let d8 count the
+chosen rank-8 helpers. Then
+
+\[
+\Delta\leq-\frac5{128}4^t d_8\leq0.
+\]
+
+The first inequality is strict if d8>0. For subsets of P alone it is only a
+non-improvement bound, consistent with the predecessor's neutral helper 684.
+No new κ. This is a written proof with an exact finite certificate, not a
+formalization of the multiplication theorem or enumeration of payload guesses.
+
+## 1. Necessary parity equations
+
+A native address permutation fixes the constant-one function. Evaluation on
+constant input functions therefore sends a finite F2 sum of native terms to
+the parity of its input labels: ADD becomes XOR, Q/ZERO_Q preserve the row,
+and ERASE zeros it. This is the augmentation homomorphism of the native
+operator algebra. Native zero implies projected zero; the converse is unused.
+
+Original owned inputs are zero. The census temporarily gives them independent
+labels and checks that none appears in any of the 2,846 paid query rows, so
+discarding those labels changes none of the certificate rows. Every paid row
+is nonzero. Frame chronology, query ranks and the published paid profile are
+checked, but native operator identities and endpoints are not reproved.
+
+## 2. First reads give a graph kernel
+
+Let V have the 637 original non-owned input labels as basis. Before helper h's
+first source read, its label x_h has never left that wire. Its projected base
+value is `x_h + a_h`, with no still-unread helper label in a_h.
+
+Process captures chronologically. Define L to fix retained inputs. At h's
+capture set `L(x_h)=f_h=w_h+L(a_h)`, where w_h is its projected injected payload.
+All labels in a_h are retained or belong to earlier captures, so f_h uses
+retained inputs only. Outside a chosen helper's held-zero prefix, its modified
+projected value is L of its base value. Indeed, a held-zero helper has no
+outgoing ADD, so dropping its writes affects no other wire; the capture
+equation establishes agreement at first read, and subsequent operations
+preserve it. This induction holds for every subset and payload.
+
+Thus `R=ker L` has basis `{x_h+f_h : h in H}` and projection R→coordinates H
+is an isomorphism. Every removed query outside an owned held-zero prefix has
+its base row in R.
+
+Partition helpers into P, F, O. P is the two partial helpers. F is the 180
+rank-8 helpers with an early own rank-2 query. O is the other 233 rank-8
+helpers. The census checks at most one early own query per helper, of rank 1
+or 2, and none for P. Write dP=|H∩P|, and similarly dF,dO. The graph property
+implies
+
+\[
+\dim R=d_P+d_F+d_O,\quad
+\dim(R\cap\{v_P=0\})\leq d_F+d_O,\quad
+\dim(R\cap\{v_P=v_F=0\})\leq d_O.
+\]
+
+Indeed, projection onto H is injective and the indicated coordinates vanish;
+zeros on retained helper coordinates can only lower these dimensions further.
+These stronger bounds distinguish cheap partial targets and costly early
+frees; an unweighted |H|-only bound does not use them.
+
+## 3. Cover early cross-helper effects
+
+Grant held-zero-prefix savings separately, at most `2^t dF + dO`. This even
+grants an H1 to each of O's 111 helpers without an early query. Other removed
+queries must contain a helper label, since L fixes non-helper inputs.
+
+An early query on an unchosen helper can disappear through a *different*
+chosen helper. Keep an early query in the token census whenever its row
+contains another helper label. These three events (zero-based) qualify:
+
+| Event | Destination | Rank | Helper-label support |
+| --- | ---: | ---: | --- |
+| 6231 | 467 | 1 | 274, 467 |
+| 6291 | 297 | 1 | 297, 465 |
+| 6510 | 464 | 1 | 323, 464 |
+
+Other early own queries can be omitted: if their destination is chosen they
+are already granted free; otherwise L fixes their nonzero row. Double counting
+a cross-helper query in the free allowance and token bound is harmless for an
+upper bound. This leaves **2,216 eligible queries and 1,945 distinct rows**.
+PR6113's printed census had 2,213: the three-query difference is intentional
+coverage, not a claim that its numerical pair results are false. A negative
+control omits event 6291's tokens and must fail exact coverage.
+
+## 4. The finite flag certificate
+
+For query ranks r=1,2,3,4,5,6 use respectively m(r)=17,33,49,64,80,96 copies
+of the row. Throughout the stated interval, `r^t <= m(r)4^t/64`. For r<4,
+`(r/4)^t` is largest at t=99/100; integer inequalities
+`r^99 64^100 <= 4^99 m(r)^100` certify the claim. For r>=4 use
+`(r/4)^t <= r/4 = m(r)/64`. No floating-point acceptance is used.
+
+`PARTITION.json.gz` partitions all **64,274 tokens into 108 colors**:
+
+| Colors (zero based) | Count | Allowed rows |
+| --- | ---: | --- |
+| 0–63 | 64 | unrestricted |
+| 64–91 | 28 | zero on P |
+| 92–107 | 16 | zero on P and F |
+
+Each color is F2-linearly independent. Rows are reconstructed from the word;
+every token multiplicity and flag is checked, and independence is checked by
+both highest-pivot and lowest-pivot elimination. IDs are the increasing integer
+order of distinct eligible rows. The witness suffices; no optimality or search
+completeness claim is made about the discovery algorithm.
+
+An independent set meets a subspace in at most its dimension. Summing the
+three graph-kernel dimension bounds across colors yields
+
+\[
+\text{non-prefix savings}\leq4^t
+\left(d_P+\frac{92}{64}d_F+\frac{108}{64}d_O\right).
+\]
+
+This single certificate covers all `2^415` ownership sets. They are not
+enumerated, and 108 is not asserted to be the minimum number of colors.
+
+## 5. Optimistic complete budget
+
+Lost target credit is `4^t dP + 8^t(dF+dO)`. Add prefix savings and subtract
+that debit:
+
+\[
+\Delta\leq4^t\left[
+\left(\frac{92}{64}+2^{-t}-2^t\right)d_F+
+\left(\frac{108}{64}+4^{-t}-2^t\right)d_O\right].
+\]
+
+Exact integer powers establish, on the full interval,
+`2^t > 127/64`, `2^(-t) < 65/128`, and `4^(-t) < 33/128`.
+For example the first is checked at the lower endpoint by
+`2^99 64^100 > 127^100`; the reciprocal inequalities are checked similarly.
+Both coefficients are strictly below -5/128:
+`184+65-254=-5` and `216+33-254=-5`. This proves the statement. Charging actual
+setup, source reads, frame changes, copies, erasure, restoration or recursive
+children cannot reverse this failed optimistic budget if they add nonnegative
+charges without changing the stipulated word or contract.
+
+## Limits and evidence status
+
+This closes the larger-set question for **individual first-read schedules on
+this exact word**, including both partial helpers. Joint deadness can permit
+later capture after a helper has influenced other wires; then a single entry
+substitution need not apply. Changed words, other input subspaces, unrestricted
+non-native-linear payload operators and other exponents remain outside scope.
+
+The projection implication and triangular argument are written mathematics,
+not Lean proofs. Seven deterministic payload/subset fixtures exercise the
+lemma but do not prove it. Two row representations and opposite elimination
+pivots reduce implementation dependence; they are not external peer review.
+The native/adjoint endpoint and complete caller were not replayed. No recursive
+supplier was built, and the selected theorem's native, owned-erasure, compiler,
+precision/tape and analytic-recovery assumptions remain unchanged.

research/g20-joint-capture-flag-bound/README.md

@@ -0,0 +1,118 @@
+# All-subset bound for G20 first-read helper captures
+
+**No new κ.** On the exact PR5708 word, simultaneous first-read capture of
+**any subset of all 415 retained helpers** cannot improve the local BIT signed
+moment for `0 <= C <= 0.01` (`t=1-C`). This includes the 180 helpers with an
+early rank-2 query and both partial rank-4 helpers. Every captured rank-8
+helper loses strictly more than `(5/128)*4^t` in the optimistic bill. Subsets
+containing only partial helpers have gain at most zero.
+
+The result grants arbitrary native-linear injected payloads and free setup,
+source access and restoration. It closes a fixed-schedule larger-set question
+left by [PR6113](https://github.com/CrocSwap/integer-mult-bounds/pull/6113), so
+further work on this mechanism must change that schedule or another stated
+premise. It is a scoped negative result, not an improved supplier or a general
+impossibility theorem.
+
+## Evidence and what is new
+
+[PROOF.md](PROOF.md) reduces capture to an entry substitution on constant-input
+parities. Its kernel projects injectively onto captured coordinates. A new
+**flag-constrained weighted partition** respects three different helper tariffs:
+64 unrestricted independent colors, 28 avoiding partial-helper coordinates,
+and 16 also avoiding early-rank-2 coordinates. This prices all subsets without
+enumerating their payloads. Exact integer powers extend the comparison over
+the full exponent interval; there is no floating-point acceptance decision.
+
+[PARTITION.json.gz](PARTITION.json.gz) covers 64,274 tokens from 2,216 queries
+and 1,945 rows. In particular it includes three cross-helper early queries
+(6231, 6291, 6510) that cannot simply be excluded from a uniform token census.
+[RESULT.json](RESULT.json) records the exact counts and row digest.
+
+PR6113 supplied the native-payload/individual-capture model, single/pair census
+and an unweighted token bound, but explicitly left larger sets with multiple
+rank-2 frees open. Its numerical pair findings are not contradicted here.
+PR5604's entry-subspace capacity bound concerned a different, static model
+and older word. This package adds a dynamic first-read graph-kernel argument,
+a tariff-sensitive certificate covering all helper sets, and exact uniform
+moment inequalities. No predecessor implementation is imported.
+
+## Reproduce
+
+From the repository root, using Python 3.12 and only its standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/g20-joint-capture-flag-bound
+```
+
+Both normal and explicit isolated optimized runs must print
+`PASS_G20_ALL_SUBSET_FIRST_READ_FLAG_BOUND`. Each run authenticates the three
+live inputs, checks all 14,794 events, compares integer-mask and set replays,
+checks every token and both Gaussian-elimination directions, verifies seven
+entry-substitution fixtures, and rejects eight corruptions: omitted tokens,
+duplicate/dependent color rows, both wrong flags, omitted cross-helper event
+6291, a forged query rank and changed source bytes. The fixtures support the
+written lemma; they are not a proof by exhaustive testing.
+
+The optional deterministic discovery command is separate from verification:
+
+```sh
+python3.12 -B research/g20-joint-capture-flag-bound/discover.py /tmp/g20-partition.json.gz
+```
+
+It stops at the first verified 108-color partition, a 1,200-second deadline,
+or exhaustion of its augmenting-path search. A timeout/failure is not an
+impossibility claim. Reproduction compares decompressed JSON, not gzip bytes.
+The successful discovery used 2,062 augmentations after the greedy stage.
+The verifier requires neither discovery nor any third-party solver.
+
+## Pins, boundaries and coordination
+
+Scientific and branch base: `721c03822c421b7f7fcbb2598993b947c4d88419`.
+[SOURCES.json](SOURCES.json) pins the exact word, frames and local invoice by
+Git blob and SHA256. Historical predecessor heads are PR5708
+`829d01fc031f7323ffcfa423fdfd1f24dcbe3190`, PR6113
+`f6712095d07d555969b6e67b792a0e98e8eea8d3`, and PR5604
+`b7c27a263b9e57d4e04b5e2dcb7b3199cc8c4170`. PR6113 is a credited research
+lead, not a live executable dependency. The selected certificate at the base
+is PR6030, conditional κ=781451/250000000; no selected record is changed.
+
+Only first-read individual capture schedules, coordinate ownership, native
+permutation-linear payloads and this exponent interval are covered. Later
+joint-dead captures, changed words and other input contracts remain open.
+Native/adjoint endpoints, the complete caller and recursive construction were
+not replayed. The selected theorem's native, owned-erasure, compiler,
+precision/tape and analytic-recovery assumptions are unchanged. This is an
+exact certificate plus a written proof, not a formal theorem audit.
+
+[TASK.json](TASK.json) records seed 08 (bit supplier), three candidate tasks,
+scope selection, checkpoint freshness and overlap limits. The local overlap
+inventory covered 8,348 research records; connected GitHub reads covered the
+latest 100 open PR bodies, focused searches and predecessor heads. Visible
+handoff posts were checked, not all discussion pagination or PR code diffs.
+No pinned sprint issue was found. The available connector cannot post to
+Discussions and the browser was signed out; an advance claim was recorded
+locally at 10:39 UTC rather than represented as a public reservation.
+
+## Open next questions
+
+- Can a jointly dead interval support a **later** reinjection whose complete
+  target and paid bill improves? Start with a triple extending PR6113's five
+  joint-dead pairs; emit an exact changed word and native endpoint before a
+  large search. The present graph-kernel proof does not apply after propagation.
+- Can this flag-certificate technique bound a different changed word? First
+  recompute early tariffs, query rows and projection flags on its exact source.
+  The current witness cannot be transferred by matching aggregate profiles.
+
+Structured first steps and blockers are in [TASK.json](TASK.json).
+
+## Credit
+
+Jerry Chen (@CubeJerry), with substantial OpenAI Codex assistance in research,
+proof drafting, implementation and verification. No subagents. Apache-2.0.
+Credit Matarener for PR6113 and its explicit larger-set handoff; Ali Romman for
+PR5604, PR5679 and the PR5708 word; ai-nanachi for PR5512's G20 construction;
+and Dugongue for the underlying refinements and late-binding work. The source
+packages and their original notices are unchanged. Binary matroid partition
+and augmentation are standard methods; the source-specific flag allocation,
+all-subset proof and finite witness are this contribution.