diff --git a/research/retained-array-catch-up/PROOF.md b/research/retained-array-catch-up/PROOF.md new file mode 100644 index 0000000000..bd8921e1ca --- /dev/null +++ b/research/retained-array-catch-up/PROOF.md @@ -0,0 +1,929 @@ +# Retained-array catch-up in the scalar common-frame transport model + +This note answers [#1166 c18956869](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18956869) +within one stated model. It proves no new κ and no supplier. Section 7 gives the priced +decisions, and Section 8 lists every premise that is not proved here. Base commit: +`de880ca1fa4540472ee8461d400914a60fc9dd41`. + +**The question.** An array is retained across calls but no call reads it. Philippe Van Velzen +proposed two per-call prices for it: + +- **(S):** one paid unit per array per call. +- **(C):** one rank-8 copy plus 8 units per array per call. + +Which price, if either, does the selected model use? The answer decides his INIT64 + d_A +final-record route. His price gate reports a complex κ ceiling of 0.00228 under (S), or 0.00221 +with PR2468-style read invoices, and no saving under (C). `verify.py` reproduces the 0.00228 value +exactly (2285992139/1002285992139); the 0.00221 value is quoted, not reproduced. + +**The short answer.** Neither convention is a primitive of the transport moment. + +- **Holding is free.** Holding an array at a fixed frame costs nothing in the moment (Lemma 2). +- **Catch-up is charged.** The moment charges the frame transport that the consumer needs to + combine the record with its partners. + - Its exact value is a minimum over the meeting level, in both directions (Proposition 3). + - The record's rank ρ_r is measured modulo the rows the consumer may combine. +- **Eight coordinates per level.** In the selected nine-stage template, every pair passes + through nine levels of eight coordinates each. A level is advanced either by the pair's own + call or by an idle sweep (Fact T). + - So a record consumed at its pair's current frame pays **8 × ρ_r × (levels advanced between + capture and consumption)**, between level-boundary instants (Corollary 4). + +How the law compares with the two conventions: + +| Situation | Law | (C) | (S) | +|---|---|---|---| +| ρ_r = number of rows, pair advances one level per call of the lifetime, consumer at the current frame | equals (C)'s mass | 8 per call | under-prices 8× | +| Record of a pair that nothing touches during the lifetime (pair 3, six calls) | 0 whatever ρ_r is | 48 | 6 | +| Record that duplicates a row the consumer may combine | 0 (ρ_r = 0) | charges | charges | + +For the #1166 routes the first row applies under the observation premise P_obs and the rank +premise P_rank of §7.2: the law agrees with (C) up to one lifetime off-by-one. + +- So their (C) verdicts are derived here rather than assumed. +- With the stated end-of-replica decoder, INIT64 + d_A costs 3,648 units per replica and the + all-initial variant 3,456. +- Decoding each bank as soon as its observed field Y_(k,U) is final, under the final-value read + convention of P_obs (timing P_Y), still costs at least 2,496 and 2,304. +- Decoding each bank right after its last local call (P_early) costs 1,344 and 1,152. This is a + lower bound for every current-frame timing at or after each bank's last local call. The + decoder-timing premise P_dec (§7.2), which the derived decoders satisfy, gives exactly those + timings. +- All of these exceed the 896-unit no-saving threshold. +- P_dec is load-bearing. At decoders placed right after each bank's own last capture the moment + bound drops to 512, which leaves a κ cap above the selected κ. No decoder is known to run + there. +- Without P_rank, philippeVV's Theorem B rejects the route only at the end decoder P_final + (1,952 / 1,824). At earlier timings it needs an extra own-bank premise (§7.2). + +## 1. Model and premises + +**P1. The transport model.** This is the scalar common-frame transport model of +[PR1664](../dirty-host-cutrank-audit/PROOF.md) §4.1, and we use its rules 1–4 unchanged: + +1. Scalar copy, add, scale and clear at a common frame are free. +2. A transport moves one register's logical row from frame A to frame B and costs at least + |ν(A) − ν(B)|. +3. No uncharged cross-frame or multi-payload moves are allowed. +4. Any pre-existing side information belongs to the entry state. + +Rows are vectors over a field K. A transport keeps the logical row: it changes only the frame. + +**P2. Nested chain.** The frames of one data family form a nested chain. Height means the +number of applied coordinates. + +- PR1664's frame formula gives d(A, B) = dim A + dim B − 2 dim(A ∩ B), which is at least + |dim A − dim B|. For nested frames the two are equal. +- The selected frames are nested. [PR2540](../qq16-complete-native-decoder/PROOF.md) §1 gives + F_L = ∏_{j=0..8} C_(d e_j) (9 axes) and F_U1 with U1 = ⟨e0,…,e16⟩ (17 axes). +- A direct move from height a to height b costs at least |a − b|. That is the number of unit + cuts it crosses, so unit moves lose nothing. + +**P3. The region and its entry state are fixed.** Lower bounds hold for a stated region and +its complete entry configuration (PR1664 rule 4). + +**P4. The inherited words have no slack.** Sometimes the region contains the unchanged +inherited calls: F0, B1, the idle sweeps and so on. + +- Their transports are then taken to cross each cut exactly as often as the rank of the rows + they must deliver above it. Those rows are their own data endpoints and restored hosts. +- This is what the coverage identity says. Paid mass equals 72W + 64N exactly, so each family + crosses each of its 72 cuts once. +- For the centre path, PR1664 §5's conditional bound (H) gives 64 per call once the + author-reported rank r = 8 is substituted, and the selected path pays exactly that. PR1664 calls + this "arithmetic substitution into a proved conditional theorem, not an independent verification + of the selected S"; we use it only as support for P4. +- So the extra mass of a region equals M minus the inherited mass. It is at least + Σ_j(δ_j⁺ + δ_j⁻) minus the inherited deficits. + +This premise blocks one escape. A record cannot ride an inherited crossing "for free" by being +added into an inherited register: the demanded endpoint row must still reach the top, so one +extra independent row must cross. A construction that exhibits real slack in an inherited word +would escape P4, and it would have to show that slack explicitly. + +**Fact T. Template levels.** These are read from the pinned selected #1094 hosted +`GLOBAL-TEMPLATE` (replica 0). Its 30-event schedule equals the base split-centres template's +schedule. + +- **Pair binding.** The local calls at stages 0–8 use pairs 0,0,0,1,1,2,2,3,3. Even stages + are forward calls; odd stages are backward calls. +- **Levels.** Each pair starts at level −1 and ends at level 8. +- **Local calls.** A local call at stage s moves its pair from level s−1 to level s. It applies + the call's eight data coordinates. + - The QQ16 frames show this directly: F0 outputs F_L (9 axes) and B1 outputs F_U1 (17 axes); + see PR2540 §1. + - It also agrees with the coverage partition 8·k_f + 1 + hosted_f + idle_f = 73 + (ctoth, #1587). +- **Idle sweeps.** An idle sweep moves an idle pair from its current level to `to_level`. + - In the base template, its two children have rank 8 × (levels advanced). + - The hosted template replaces part of an idle child by hosted helper residuals. + [idle-axis-hosting](../idle-axis-hosting/PROOF.md) §2 shows that this leaves the product + unchanged, so the frame after the sweep is unchanged. +- **Bridges.** Every bridge joins two pairs at equal levels. We take pairs at equal levels to + share a frame (**P_glob**), as these free common-frame operations require. P_glob only + shows that some costs in §7.2 are 0; no lower bound uses it. +- **Hosting and level boundaries.** A hosted residual acts at its helper's invocation time, + inside the idle window. So part of an idle family's next block can be applied **before** its + sweep, and the family then sits between two declared levels. + - Example: just before event 7, some pair-0 families are already 4 or 9 coordinates above + level 2. + - The law's "8 × levels" form therefore holds between instants on level boundaries. In general + the charge is the number of coordinates applied between capture and consumption. + - `verify.py` checks the 21 route instants used below: the seven route captures, the four + P_early consumers, the three all-initial reads with their consumers, and the four P_Y + consumers. It checks replica 0 in both directions: + - **No overshoot.** Every residual hosted on the pair by then belongs to a sweep that has + already reached the stated level: 14,290 slot checks over 3,644 distinct residual slots, + 4,173 of them at the seven captures. + - **No undershoot.** Every residual of a sweep that has reached the stated level has already + landed: 9,280 checks of slots that have not landed yet. + - `independent_check.py` confirms the same 21 instants in **all 16 replicas** by replaying the + height of each of the 896 families of each replica. + - Twelve instants (the 7 captures, the 4 P_early consumers and bank 0's P_Y consumer) are + checked under both conventions for slots and events at equal times. + - The other 9 are read after their time has settled: the P_Y consumers of banks 1–3 and the + three all-initial reads with their consumers. Residual slots at that time belong to the + sweeps at that time, which come before the instant in event order. Under the slots-last + convention up to 5 of these 9 are not uniform (5 in replica 0), so they rest on this one + reading. + - An AI review pass replayed the hosted template convention-free, placing each slot at the + schedule position of its hosting invocation. It found all 21 instants uniform at the + stated heights in all 16 replicas. + - So the route masses below are the same in every replica. + +So one level is eight coordinates, and the nine levels are the 72 paid coordinates of each +family. + +**Level timeline** (pairs 0–3, after each event): + +| Event | Description | Pair levels | +|---|---|---| +| entry | — | −1 −1 −1 −1 | +| 0 | F0 | 0 −1 −1 −1 | +| 1 | B1 | 1 −1 −1 −1 | +| 2 | idle sweep, pair 1 | 1 1 −1 −1 | +| 4 | F2 | 2 1 −1 −1 | +| 5 | idle sweep, pair 1 | 2 2 −1 −1 | +| 7 | B3 | 2 3 −1 −1 | +| 8 | idle sweep, pair 2 | 2 3 3 −1 | +| 10 | F4 | 2 4 3 −1 | +| 11 | idle sweep, pair 2 | 2 4 4 −1 | +| 13 | B5 | 2 4 5 −1 | +| 14 | idle sweep, pair 3 | 2 4 5 5 | +| 16 | F6 | 2 4 6 5 | +| 17 | idle sweep, pair 3 | 2 4 6 6 | +| 19 | B7 | 2 4 6 7 | +| 20 | F8 | 2 4 6 8 | +| 21–23 | final idle sweeps, pairs 0–2 | 8 8 8 8 | + +Bridges (events 3, 6, 9, 12, 15, 18, 25–27) are omitted from the table because they do not +change levels. `verify.py` reads this table from the schedule. `independent_check.py` +recomputes it from explicit coordinate sets, using the idle child ranks and not the declared +levels. + +**Definitions.** + +- An **entry configuration** is a finite list of (row, height) pairs. +- A **demand** is a finite list of (row, height) pairs that must each be held, at some time + in the region, by a register at that height. +- For a cut j (between heights j−1 and j), let E_j⁺ and E_j⁻ be the spans of the entry rows + at heights ≥ j and < j. Let D_j⁺ and D_j⁻ be the spans of the demanded rows on each side. +- The **deficits** are δ_j⁺ = dim(E_j⁺ + D_j⁺) − dim E_j⁺ and δ_j⁻ = dim(E_j⁻ + D_j⁻) − dim E_j⁻. + +The entry configuration consists of every row the consumer may combine. In an application, a +row that the consumer's contract does not allow it to read is not part of the entry +configuration. This is how observation contracts such as P_obs (§7.2) enter. + +## 2. Lemma 1 (PR1664's cut-rank bound, for one nested chain) + +Every program in P1–P3 that meets the demand has paid mass + +M ≥ Σ_j (δ_j⁺ + δ_j⁻). + +**Proof.** This is PR1664 (C-down), its symmetric (C-up), and (A), applied with Q_j equal to +the demanded rows on each side. + +- Each high-to-low transport across cut j adds at most one direction to the retained span of + low rows. +- Common-frame operations, upward moves and clears add none. +- A move between heights a and b crosses |a − b| cuts. + +Summing over the cuts gives the bound. ∎ + +**The bound is not always attained.** The frame model in `verify.py` finds 45 non-tight cases +among 4,044 general instances. The smallest has the same row v at heights 0 and 2 and demands +v at height 1. Every cut deficit is 0, but one transport is needed. Proposition 3's +independence hypothesis excludes such duplicates. + +## 3. Lemma 2 (storage neutrality) + +In P1–P3, keeping a register at a fixed frame for any number of calls contributes nothing to +M. Adding duplicates of entry rows at their own heights changes neither the per-cut bound nor +the minimum M. + +**Proof.** + +- M counts transports only (rule 2). +- Spans do not change when duplicates are added. +- A same-frame copy is free (rule 1). So each configuration can reach the other at zero cost. + +∎ + +**Consequences.** + +- **No storage price.** No per-array-call storage price follows from the moment, so (S) is an + extra physical premise. + - The question of physical storage is real but lies outside the moment: tape, banks, hosting + windows, and the stream that holds an extra array. +- **Retention by existing streams.** The selected record keeps helper residuals across calls on + existing idle data streams, with no per-call charge (idle-axis hosting §2), and its hosted + template has no helper banks. + - This shows that the selected accounting puts no moment price on retention by an existing + stream. + - It does **not** show that new arrays are physically free. + +## 4. Proposition 3 (record, partner and consumer: exact both-direction minimum) + +**Setting.** + +- Records R sit at height h_r and partners P at height h_p, with span R ∩ span P = 0. +- The demand is a row set O ⊆ span(R ⊕ P) at height h_c. Optionally P must also stay at h_p. +- Let ρ_r = dim(P + O) − dim P. This is the part of O that only the records can supply. +- Let ρ_p = dim(R + O) − dim R. This is the part only the partners can supply. +- Let ρ_o = dim O. + +**Claim.** The minimum paid mass equals + +min_L f(L), where f(L) = ρ_r |L − h_r| + ρ_p |L − h_p| + ρ_o |L − h_c|. + +The minimum is attained at L = median(h_r, h_p, h_c), and it equals the sum of the cut deficits. + +**Lower bound.** Fix a cut j. A side is "high" if it lies at heights ≥ j. + +- **Consumer on the high side.** The upward deficit is: + - 0 if R and P are both high; + - ρ_r if only P is high; + - ρ_p if only R is high; + - ρ_o if neither is high. +- **Consumer on the low side.** The downward deficit is the mirror image. +- **Partner demand.** It never adds a deficit, because P is in the entry span on its own side. + +**Matching f.** At cut j, f(L) is charged with the weights of those points of +{h_r (weight ρ_r), h_p (weight ρ_p), h_c (weight ρ_o)} that lie on the other side from L. + +- If L lies on the **majority** side, the other side holds at most one point. Its weight is + exactly the deficit in the case list above. +- Putting L on the minority side instead costs at least as much, by three inequalities: + - ρ_r ≤ ρ_o, because ρ_r = dim(P+O) − dim P ≤ dim O; + - likewise ρ_p ≤ ρ_o; + - ρ_o ≤ ρ_r + ρ_p, because o ↦ (a(o), b(o)) below embeds O into A ⊕ B. + +The median of {h_r, h_p, h_c} lies on the majority side of every cut. Hence + +f(median) = min_L f(L) = Σ_j (δ_j⁺ + δ_j⁻) ≤ M, + +where the last inequality is Lemma 1. + +**Construction.** + +1. Write each o ∈ O uniquely as a(o) + b(o) with a(o) ∈ span R and b(o) ∈ span P. + - A = {a(o)} is the projection of O along P. Its kernel is O ∩ P, so + dim A = dim O − dim(O ∩ P) = ρ_r. + - Likewise B = {b(o)} has dim B = ρ_p. +2. Copy and move a basis of A from h_r to L, at cost ρ_r |L − h_r|. +3. Copy and move a basis of B from h_p to L, at cost ρ_p |L − h_p|. The partners stay at h_p. +4. At L, O lies in A + B, so form a basis of O there for free. +5. Move that basis to h_c, at cost ρ_o |L − h_c|. + +The total cost is f(L). ∎ + +**Special cases.** + +- (i) h_c = h_p ≥ h_r: the record **climbs**, at cost ρ_r (h_p − h_r). +- (ii) h_c = h_r ≤ h_p: the partners **descend**, at cost ρ_p (h_p − h_r). +- (iii) h_c = h_r = h_p: the cost is 0. + +The consumer level is a premise of the caller. Proposition 3 prices every choice of it; it +does not choose one. + +**A consumer that works low and returns its outputs.** Suppose a consumer forms O below h_p and +then moves its outputs back up to h_p. The whole program still delivers O at h_p, so it is +bounded by Proposition 3 with h_c = h_p. Only consumers whose outputs are used, and stay, below +the partners' frame are priced differently. + +**Finite checks.** + +- **Primary, by exhaustive search.** `verify.py` runs a breadth-first search over per-level + spans. It checks opt = Σ deficits = min_L f on 34,454 instances, each domain complete: + - GF(2)², 4 levels: 2,432 instances; + - GF(3)², 3 levels: 2,106 instances; + - GF(2)³, 3 levels: 29,916 instances over all 129 independent (R, P) pairs. +- **Independent.** `independent_check.py` runs Dijkstra over reduced echelon bases on 2,432 + GF(2)² instances, and checks opt = min_L f. +- **Negative controls.** An upward-only bound fails on 14,426 of the 34,454 instances. A formula + without the output term fails as well. + +## 5. Corollary 4 (eight coordinates per level) + +Under Fact T and P4, take a record of pair k captured at time t and consumed at its pair's +current frame at time t′, so h_c = h_p. Let ρ_r be its rank modulo the rows the consumer may +combine at t′ (Proposition 3). + +- **Exact charge.** The catch-up is exactly ρ_r × (coordinates applied to pair k between t and + t′). +- **Level boundaries.** When both instants lie on level boundaries, this is + **8 ρ_r (ℓ(t′) − ℓ(t))**. +- **Per incidence.** Call each local call of pair k between t and t′ a later **data incidence** + of the record. Each applies its own 8 coordinates, so the charge is at least 8 ρ_r per later + data incidence. +- **Idle sweeps** add further coordinates. +- **Duplicates are free.** A record whose rows the consumer may already combine (ρ_r = 0) costs + nothing, however many levels pass. + +**Child shape.** The law fixes the transported **mass**, not the shape of the children. + +- One child of rank 8Δℓ per independent row realizes it. So do rank-8 children, one per level. +- Per unit of mass, larger children cost less in the moment when a > 0. +- So convention (C)'s "rank-8 copy per call" shape is sufficient but not forced. + +## 6. Proposition 5: (S) and (C) compared with the law + +**(a) When (C) is a special case of the law.** + +- **The two masses.** (C)'s mass is 8 per array-call. The law's mass for a current-frame + consumer is 8 ρ_r per level advanced. +- **When they agree.** They are equal when ρ_r equals the number of rows and the source pair + advances one level per counted call of the lifetime. The condition is sufficient, not + necessary: half the rows and two levels per call also give equal masses. +- **The #1166 records satisfy this,** given P_obs and P_rank (§7.2): + - **INIT records** are captured just before their bank's first call, at levels −1, 2, 4 and 6. + Since the levels are the global stage index minus one, the lifetimes are 9, 6, 4 and 2. + - **d_A records** are captured right after the backward call, at levels 1, 3 and 5. The + lifetimes are 7, 5 and 3. +- **The off-by-one.** Philippe Van Velzen's price gate uses 8 for bank 0's d_A. Under the + convention he uses for INIT (calls after the capture point), the count is 7. + - The law therefore gives 8 × 456 = 3,648. + - (C) as published gives 8 × 464 = 3,712. + - No decision changes. + +**(b) A zero-advance window.** Take pair 3's Y streams in replica 0 (families 784–895). Nothing +acts on them from entry until event 14 (time 40). The window is replica-specific: it holds in 12 +of the 16 replicas, and in replicas 4, 5, 6 and 11 pooled slots land on some pair-3 Y families +before event 14 (`independent_check.py`). In replica 0: + +- no local call (stages 0–5 are on pairs 0–2); +- no idle sweep (the sweeps at events 2, 5, 8 and 11 are on pairs 1 and 2); +- no bridge (bridges at events 3, 6, 9 and 12 join pairs 0–1 and 1–2; event 15 is the first + bridge that touches pair 3); +- no hosted residual. Their sweep from level −1 to level 5 is an unhosted rank-48 child, and + no pooled slot lands on them before time 40. + +A record of such a stream, captured at entry and consumed at its current frame before event 14, +spans six calls. + +- The law charges 0 whatever ρ_r is, because no level is advanced. +- (S) charges 6 per array, and (C) charges 48. + +The record merely copies an untouched stream, so it is also free for the more basic reason of +Lemma 2. The example shows only which variable the law counts: levels advanced by the source +pair, not calls. It is not a useful retention. + +Pair 3's **X** streams host 160 helper residuals in the same window, so their frames do change. +That is the selected record's own use of this window shape ("nothing touches F between ι and +τ", idle-axis hosting §2). + +**(c) Lagging-pair records do not separate the law from (C).** + +- **The candidate.** Take a record of pair 0's X stream captured after B5 (event 13), when pair 0 + sits at level 2, and consumed at the end. + - In replica 0, pair 0 advances six levels, all in idle sweep 21, while three calls happen. + - An independent row would therefore pay 48 against (C)'s 24 there. (In 6 of the 16 replicas + some pair-0 X families already carry part of sweep 21 at that instant; the conclusion below + does not depend on heights.) +- **Why it does not separate them.** The record is not independent. In the pinned schedule: + - X_(0,U) is last written at event 6, by the bridge X_0 += c X_1. + - After event 13 pair 0 is touched only by: + - idle sweep 21, a transport that keeps the logical row; + - bridge 27 with src = 0, which only reads X_(0,U); + - the terminal Y translations; + - the terminal relabel (X_U, Y_U) → (Y_U, −X_U). +- **Consequence.** So the record equals, up to sign and frame, the final completed-X field + Y_(0,U), which the contract observes. Then ρ_r = 0 and the law charges 0. + - `verify.py` checks this schedule fact. + - A control with bridge 27 reversed, so that it writes X_(0,U), makes the check fail. +- **Conclusion.** This package exhibits no route in which (C) under-prices. + +**(d) (S).** Storage is not a moment price (Lemma 2). As a stand-in for catch-up, (S) +under-prices current-frame consumers by 8×. Example: PR2540's 16 early records over one call +cost 16 under (S), but the law gives 128, which is both forced and attained (§7.1). + +## 7. Applications and decisions + +### 7.1 Controls + +| Control | Law | Source value | +|---|---|---| +| PR2540: 16 early records, F_L → F_U1 (one level) | 16 × 8 = 128 | its 16 rank-8 upgrades (PR2540 §2) | +| PR2197: 8 Y_A arrays moved 18 frame terms to private frame I | 8 × 18 = 144 | 144-line floor | +| PR2678: 224 outputs, F_U1 → F_L | 224 × 8 = 1,792 | 224 H8 | +| PR2678: 224 outputs, F_U1 → (C_q, I), heights 17 → 1 and 17 → 0 | 112 × 16 + 112 × 17 = 3,696 | 112 H16 + 112 H17 | +| Selected centre path: 8 centres per call descend 8 → 0 (PR1664 §5.2 / ctoth's tree lemma) | 64 per call, 576 per replica | eight rank-8 copies, C = 64 | +| #1166 price gate against PR2474 | break-evens 573 (S) and 71 (C); (S) ceiling 2285992139/1002285992139 | reproduced with `ceiling.py` and with Decimal | + +Notes on the controls: + +- **PR2540.** It attains Proposition 3(i), assuming ρ_r = 16. That value is ywz65's PR2511 + rank-16 bound for its compressed observation interface, as quoted in PR2540's README. +- **PR2678 F0-gauge row (1,904).** It adds one signed-line gauge per Y. That is outside the + height model and is quoted from PR2678. +- **Centre path.** It is the law's descend direction. + +### 7.2 Route (a): the INIT64 + d_A final-record contract (philippeVV, fork 9fcd3d89) + +**Premises.** + +- **P_obs (observation contract).** + - **What the consumer may combine.** The consumer may combine only: + - the observations of the final-record contract, which are items 1–3 of + [qq16-final-record-obstruction](../qq16-final-record-obstruction/PROOF.md) §1: final + selected fields, final completed-X ordinary fields Y_(k,U), and the forward histories; + - the stated records or reads, at their stated capture times. + - **What is excluded.** The former-Y ordinary endpoints (final X_(k,U)), every additional + ordinary read, and transient stream contents. + - **Read convention (final-value reads).** The consumer may read a named observed field only + once that field holds its final value. + - A stream that still holds a non-final value counts as transient, even when that value is + a fixed combination of final fields. + - For example, on the literal replica-0 schedule bridges 25–27 are X_3 += X_2, + X_2 += X_1 and X_1 += X_0, followed by the terminal Y = −X. So X_(1,U) after event 12 + equals Y_(0,U) − Y_(1,U), fixed at level 4, and X_(2,U) after event 18 equals + −Y_(0,U) + Y_(1,U) − Y_(2,U), fixed at level 6. + - An AI review pass in this loop derived these two identities; `verify.py` checks the last + writes and bridge levels but not these combinations. + - This convention is what gives "transient stream contents are excluded" its meaning. Under + a span-based reading, banks 1 and 2 could decode at levels 4 and 6, which is the P_early + cost. So the P_Y bracket below is relative to this convention. + - **Where the premise comes from.** It is a premise of the QQ16 observation contract (the + obstruction's §1 excludes "former-Y ordinary endpoint, or additional ordinary read"). It is + not a consequence of the moment. + - **Why it matters.** Without it, rule 1 lets the consumer combine every level-8 row for free, + and a record row may lie in their span. + - The obstruction's kernel family is visible exactly in the former-Y endpoints (its §4). + - Local calls and bridges are invertible. +- **P_rank (contract level, unproved).** + - **Statement.** At every cut j, the stated arrays captured below j that a decoder above j + needs are linearly independent modulo the span of everything P_obs lets the consumers combine + at or above j. That span includes the retained history of the rows P_obs allows, in + PR1664's sense. + - It does not include the whole program's retained history. Local calls and bridges are + invertible and the inherited streams carry the initial data upward, so under that reading + the INIT and d_A rows would lie in the span and P_rank would be false. + - **Uncompressed delivery (our reading).** We read the published contract as delivering each + needed array itself, uncompressed, to the decoder that uses it. + - Its README states that "Every retained array stays live until the final decode" + (final-record README @9fcd3d89). That is the price gate's storage-lifetime convention. + - It does not by itself say that each array is transported to the decoder's frame. + - Uncompressed delivery is therefore our premise, not a statement of the published contract. + - **Effect.** The demanded rows are then the arrays themselves. By Lemma 1 the deficit at cut j + is the number of needed arrays captured below j whose decoder sits above j. Summed over the + cuts, each array pays its climb to its own decoder. + - **Why delivery matters.** Lemma 1 counts the rank of what is demanded, not the number of + arrays a decoder reads. A decoder output r1 + r2 forces one crossing, not two. Compressing + records before they climb is therefore a contract change; see Robustness. + - **Support.** Philippe Van Velzen's finite-model census and derived decoders (#2074 + c18950410, c18950926). + - The census tests whether blocks of records are sufficient and necessary for decoding from + the contract. It does not test this per-cut independence. + - It is not a proof on the actual cover. +- **Capture times.** As stated in the price gate (`price_gate.py` @9fcd3d89: "INIT records of + bank k are read just before that call", the bank's first call at stage 0, 3, 5 or 7): + - INIT records are query maps of the initial X_(k,U), for example B0 X_(0,U) and B2 X_(0,U) + in the obstruction's §1; + - d_A is captured right after the bank's backward call. + + Local calls overwrite X_U: x'_U = x_U − y_U backward, and x'_U = x_U − K_(s,U) f forward + ([CONSERVED-QQ16](../joint-query/evidence/CONSERVED-QQ16.md) (1) and (3)). No bridge writes + X_(k,U) before bank k's first call, and `verify.py` checks this. + - **Banks 1–3.** Their first call is backward, x'_U = x_U − y_U, so recovering x_U afterwards + needs the transient y_U. For them the stated INIT capture is the latest one that needs no + other read. + - **Bank 0 is an exception.** Its first call F0 is forward, and CONSERVED-QQ16 (3) inverts it + as z = w + K_(0,U) f0. f0 is a contract observation (the obstruction's §1 item 3). + - So B_t X_(0,U)(initial) = B_t X'_(0,U) + B_t K_(0,U) f0 for t = 0, 2. The 16 INIT0 rows + can therefore be formed at F0's output frame, level 0, one level above the stated + capture, from one X_(0,U) read after F0 plus the observed f0. + - This lowers every P_rank total by 16 × 8 = 128: 3,520 / 2,368 / 1,216 (original) and + 3,328 / 2,176 / 1,024 (all-initial) at P_final / P_Y / P_early. + - The own-bank floor at P_Y becomes 1,216 / 1,088. + - The one-level 1,952 / 1,824, the own-bank P_early 800 / 608 and every count-only value + are unchanged. + - All of these are still at least 896, so no verdict changes; `verify.py` computes them. + - This is the first concrete step of lever 1 below (open question 1). The tables below keep + the stated capture times. + - *Sensitivity (AI review pass, not computed by `verify.py`).* The backward word is invertible + from the pair's post-call X' and Y' (CONSERVED-QQ16 (1)). A capture one level later that + also reads the pair's transient Y (with bank 0 via f0) gives P_final 3,136 / 2,944, + P_Y 1,984 / 1,792 and P_early 832 / 640. The P_final and P_Y values stay ≥ 896, but the + P_early values fall below 896 (caps 0.00034 / 0.00135, both still below the selected κ). + So the P_early no-saving verdict depends on the stated capture times. +- **P_dec (decoder timing).** Each bank's decoder uses an observation of its own pair that + exists only after that pair's last local call. + - The derived decoders of #2074 c18950926 have this property. Through the tail identity + C_k = w_k + K_(2k+2) f_(2k+2) (C_k the final Y_(k,U), w_k the initial Y_(k,U)) each uses + f_(2k+2) and pair k's final selected fields, both available only after F_(2k+2), pair k's + last local call (F8 and f8 for bank 3). F0/B1/F2 conserve the cut sums X_p + Y_p on A ∪ T. + An AI review pass read the decoder code (fork 40d58b9e, as data only) and confirmed this. + - P_dec is a property of those decoders, not of the moment or of P_obs. + - **It is load-bearing.** Decoders placed right after each bank's own last stated capture + (levels 1, 3, 5, 6) are current-frame timings that P_obs alone does not exclude. There the + law gives only **512** in both variants, leaving κ caps of 0.0020286 idle-priced and 0.0020185 + rank-8-priced, above the selected κ and PR2474. + - Decoders right after each backward call (levels 1, 3, 5, 7) cost 640. That still leaves a + positive saving, with a cap of 0.0013547 idle-priced, below the selected κ. + - `verify.py` computes both values, and a negative control fails if P_early is claimed as a + floor for such decoders. +- **Consumer timing.** The decoder of bank k works at bank k's **current** frame (h_c = h_p in + Proposition 3). We use three timings. + - **P_final**, the stated contract: every bank decodes at the end, level 8, where the final + records and the replica's data endpoint live. + - **P_Y**, the earliest timing under the final-value read convention. + - The decoder of bank k uses the final completed-X field Y_(k,U) = −final X_(k,U) (terminal + relabel), through the tail identity C_k = w_k + K_(2k+2) f_(2k+2) (#2074 c18950926). + Under P_obs it may not use transient contents of X_(k,U). + - Local calls on pair k overwrite X_(k,U), and a bridge with dst = k adds into it. So the + field is final only after its last write: event 6 for bank 0 (pair 0 at level 2), and + bridges 27, 26 and 25 for banks 1, 2 and 3. Those three bridges run with every pair at + level 8. `verify.py` checks the last writes and the levels. + - So P_Y decodes bank 0 at level 2 and banks 1–3 at level 8. Other observations can only + delay a decoder. So, under P_obs with the final-value read convention and for decoders that + use their own Y_(k,U) (as the derived decoders do), every admissible timing has each + consumer at or above its P_Y level. + - **P_early**: decode each bank at its own frame right after its last local call (levels 2, 4, + 6, 8). + - For banks 1 and 2 this ignores the final-value read convention, so it is not attainable + under P_obs with that convention. + - It lower-bounds every current-frame timing at or after each bank's last local call, which + is every timing P_dec admits. The reason is that above the captures, catch-up only grows + with the consumer level. + - It does not bound earlier decoders (see P_dec). + - It also assumes, in the route's favour, that the corrected fields then ride the inherited + idle sweep to level 8 at no extra cost. If the decoded outputs were additional rows, P4 + would charge their climb. + + A consumer that works lower and returns its outputs is covered by Proposition 3 (§4). Only + consumers whose outputs stay below the partners' frame are not priced. + +**Catch-up per replica, original contract** (units; levels climbed in parentheses). + +| Records | Capture levels | P_final | P_Y | P_early | +|---|---|---|---|---| +| INIT, banks 0–3 (16 arrays each) | −1, 2, 4, 6 | 1,152 + 768 + 512 + 256 (9, 6, 4, 2) | 384 + 768 + 512 + 256 (3, 6, 4, 2) | 384 + 256 + 256 + 256 (3, 2, 2, 2) | +| d_A, banks 0–2 (8 arrays each) | 1, 3, 5 | 448 + 320 + 192 (7, 5, 3) | 64 + 320 + 192 (1, 5, 3) | 64 + 64 + 64 (1, 1, 1) | +| **Total** | | **3,648** | **2,496** | **1,344** | + +The P_early total is exactly 8 per later data incidence. Under P_Y and P_final the idle sweeps +add the rest. + +**The all-initial variant.** #2074 c18950926 item 2 publishes it as equivalent: it swaps the d_A +records for the reads B2 X_1U, B4 X_2U and B6 X_3U, which bank 0, 1 and 2 use respectively. + +- **When the reads can be taken.** X_(k+1,U) keeps its initial row until pair k+1's first call, + so the read may be taken at any level pair k+1 holds before then: {−1, 1, 2}, {−1, 3, 4} and + {−1, 5, 6}. +- **Cost at P_early.** Pair k+1 reaches bank k's P_early level (2, 4 or 6) in idle sweeps 5, 11 + and 17, before its first call. With pairs at equal levels sharing a frame (P_glob), the read is + taken at the consumer's own frame and costs 0. + - Both pairs sit at exact levels at that instant (times 10, 28 and 56, after every event and + slot at that time). Both checkers verify this. +- **Cost at P_Y.** Bank 0's read again costs 0 (level 2). The reads for banks 1 and 2 are best + taken at their latest levels, 4 and 6, and climb 4 and 2 levels to level 8: 256 + 128. +- **Cost at P_final.** The latest reads, at levels 2, 4 and 6, climb 6, 4 and 2 levels: + 8 × 8 × (6 + 4 + 2) = 768. +- **Totals.** INIT is unchanged, so the variant costs **3,456** (P_final), **2,304** (P_Y) and + **1,152** (P_early). +- **P_glob is not needed for the rejection.** It is used only to show that the zero read costs + are attained, and 0 is a trivial lower bound. The positive read climbs follow from + d(A, B) ≥ |dim A − dim B| for any two frames. + +**Price.** With C = 0 and the controller free, a paid mass of at least 896 units per replica +leaves no positive saving, whatever the packing. Write m = 73 and w = 896/9, the number of live +families per call (`ceiling.py`: w = families / stages). Then: + +- At a = 0, every child costs r/m. The moment is then total/(m·w) = (72w + u/9)/(73w), which is + at least 1 exactly when u ≥ 9w = 896: one unpaid coordinate for each of the 896 families. +- For a ≥ 0, every child cost (r/m)^(1−a) is at least r/m. + +Both `ceiling.py` (at 895 and 896) and the exact rational check agree. Our PR2470 found the same +threshold under the assumed centre-like convention: at C = 0 its last count with any positive +saving is 111 coordinate-calls, and 8 × 111 = 888 < 896 ≤ 8 × 112. `verify.py` checks that the +pinned row agrees. + +**Decision: rejected in the stated model, under P_obs, P_rank, P4, P_dec and the stated capture +times, for every current-frame consumer timing at or after each bank's last local call.** + +- The stated end decoder costs 3,648 (all-initial 3,456). +- Every timing admissible under P_obs with the final-value read convention, for decoders that use + their own Y_(k,U), costs at least the P_Y values, 2,496 (2,304). +- Every current-frame timing that satisfies P_dec costs at least the P_early values, 1,344 + (1,152). +- All of these are at least 896. Adding any non-negative storage price can only raise the cost. +- Bank 0's INIT via f0 lowers each value by 128, and every value stays at least 896. +- Without P_dec the lower-bound argument no longer rejects at some timing: 512, as above. No + decoder is known to run there (bank 3's needs f8; keeping only bank 3 at F8 gives 768, cap + 0.00068, below the selected κ, per an AI review pass), and 512 is not claimed to be minimal. + +**Robustness.** + +- **d_A alone** costs 960 under P_final, which is at least 896. +- **Theorem B in place of P_rank.** Theorem B in #2074 c18940190 (philippeVV) says any repair + needs at least 62 independent coordinates per owner per replica. + - **Status.** It is a posted claim, with fork `680d0997621a2cecfef2186ab143377658687825`, and + has not been reviewed. + - **Shape.** It is one global count: it does not say which bank's decoder needs which rows. + - **Common premises.** Below, the repair is restricted to the stated captures, each stated + array supplies at most one row per owner, and P_obs and P4 hold. +- **One consumer level (P_final): Theorem B alone rejects.** + - Fix a cut j below the consumer level, and let n⁺_j count the stated arrays captured at or + above it. Modulo the contract observations, those arrays span at most n⁺_j dimensions, + while the repair delivered at the consumer has rank at least 62 modulo the same + observations. + - Lemma 1 then forces at least max(0, 62 − n⁺_j) upward crossings of cut j. + - Summed over the cuts, this equals the total climb of the 62 cheapest captures: **1,952** + (original) and **1,824** (all-initial). Both are at least 896. + - This needs neither P_rank nor any assignment of rows to banks. It also covers compressed + deliveries, because Lemma 1 counts ranks and Theorem B counts the rank of the repair. +- **Several consumer levels (P_Y, P_early): the count alone does not decide.** When banks decode + at different levels, the cut argument must know which decoder needs which rows. + - **With an own-bank premise**, the single-level argument applies bank by bank. + - **The premise (strong reading).** Let W be the span of the rows P_obs lets the consumers + combine, C_k the captures that bank k's derived decoder uses (c18950926), and D_k the rows + bank k's decoder needs (m_k of them). The 62 rows split freely over the banks, and for every + bank k: + - (i) D_k ⊆ W + span C_k; + - (ii) D_k ∩ (W + Σ_{l≠k} span C_l) = 0, where C_l are **all** the other banks' captures, + not only those above the cut. + - **Per-cut additivity.** Fix a cut j. Let C⁺ be the captures at or above j, n⁺_{k,j} the + number of bank k's captures among them, and E⁺ = W + span C⁺. Lemma 1 bounds the joint + deficit dim(E⁺ + Σ_k D_k) − dim E⁺ = Σ_k m_k − dim ker φ, where + φ: ⊕_k D_k → V/E⁺ is the sum map over the banks whose consumers are above j. + - Project ker φ onto its first coordinate. A kernel element has + d_1 = e − Σ_{l≠1} d_l with e ∈ E⁺. By (i), Σ_{l≠1} D_l ⊆ W + Σ_{l≠1} span C_l, and + E⁺ ⊆ W + span C_1⁺ + Σ_{l≠1} span C_l. So the image lies in + I_1 = D_1 ∩ (W + span C_1⁺ + Σ_{l≠1} span C_l). + - By (ii), I_1 meets W + Σ_{l≠1} span C_l only in 0. So I_1 injects into the quotient + (W + span C_1⁺ + Σ_{l≠1} span C_l) / (W + Σ_{l≠1} span C_l), whose dimension is at most + n⁺_{1,j}. Also dim I_1 ≤ m_1. + - The kernel of the projection is the same sum map for the remaining banks with the same + E⁺, and the same two steps apply to bank 2, then bank 3. Induction gives + dim ker φ ≤ Σ_k min(m_k, n⁺_{k,j}), so the deficit is at least + Σ_k max(0, m_k − n⁺_{k,j}). Summed over the cuts, each bank pays the climbs of its m_k + cheapest captures, and minimizing over the free split gives the cheapest 62 own-bank + climbs. + - The argument needs only transport cost ≥ |Δheight|, not P_glob. + - It fails under weaker readings. An AI review pass in this loop found violations in + random GF(2)/GF(3) instances when (ii) is restricted to the other banks' demands or to + their above-cut captures. + - The floor is then the cheapest 62 own-bank climbs: **1,344 / 1,216** at P_Y, both at least + 896. + - At P_early it is **800 / 608**. Their κ caps are 0.0005091 / 0.0015234 idle-priced and + 0.0005051 / 0.0015144 rank-8-priced. All are below the selected 0.001672660197076918, and + therefore below every pending claim. + - **Without it,** a capture may serve any decoder. + - Under P_glob, 62 stated-capture rows can then be delivered, each to its nearest consumer + level in either direction, at total cost 608 / 544 at P_Y and 112 / 0 at P_early. + - If the stated captures are independent, these deliveries meet the count. So an argument + that uses only Theorem B's count and the capture heights cannot force more than these + costs. + - At P_Y the original variant's 608 has cap 0.0015234 idle-priced (0.0015144 rank-8), below + the selected κ. If the stated captures are independent modulo the observations, Lemma 1 + forces exactly this delivery (an AI review pass gave a two-consumer pivot proof and found + 0 mismatches in 685 GF(2) brute-force cases; with dependent captures it can fail), so + there the count still decides against the selected record. + - The caps at 544 (P_Y, all-initial), 112 and 0 (P_early) are 0.0018604, 0.0041203 and + 0.0047021 idle-priced, all above the selected κ. So at those timings Theorem B's count + alone does not reject the route. +- **Summary of the robustness.** P_rank rejects at every current-frame timing P_dec admits. + Theorem B alone + rejects at P_final. At earlier timings, where banks decode at different levels, it rejects + (against the selected κ) only with the own-bank premise. +- **Sufficiency.** Whether the contract is actually sufficient does not affect the rejection. + The evidence is finite models plus the derived decoders. A contract that is not sufficient + fails anyway, and one that is sufficient costs at least the amounts above. + +**What could revive the route.** + +- **The binding term.** In both variants it is INIT64's catch-up: 1,920 at P_Y and 1,152 at + P_early (1,792 and 1,024 with bank 0's INIT via f0). +- **Per term, if the INIT information were free** (`verify.py` prices each term): + - **At the stated end decoder (P_final) no INIT lever suffices.** The original variant's d_A + term alone costs 960, which is at least 896. The all-initial reads alone cost 768, whose cap + of 0.00067848 idle-priced is below the selected κ. + - **At P_Y the original variant's d_A term alone is 64 + 320 + 192 = 576.** Its cap of + 0.0016919 idle-priced beats the selected record only at the margin (576 is exactly the + rank-8 break-even). It loses to PR2474 and to every pending claim. + - **The live target is the all-initial variant at P_Y.** Its reads cost 0 + 256 + 128 = 384. + That leaves at most 573 − 384 = 189 units against PR2474, or 579 − 384 = 195 against the + selected record, for the INIT information, against 1,920 now: roughly ten times less. + - At P_early, a bound and not attainable under the read convention, the d_A term is 192 and + the reads are 0. Against PR2474 the INIT term of 1,152 would then have to fall below + 573 − 192 = 381 (original) or 573 (all-initial). +- **The target.** A gain needs catch-up-weighted retention below the break-evens, the largest + masses at which a route still gains: + - 573 idle-priced or 568 rank-8-priced against PR2474; + - 570 or 568 against #2843, #2848 and #2857; + - 568 or 560 against the bit endpoint (PR589). +- **For scale.** 62 arrays would need an average climb under about 9.2 coordinates, roughly one + level. + - The stated INIT captures sit 2 to 3 levels below the P_early consumers (exactly 2 with bank 0's + INIT via f0). + - At P_Y, banks 1 and 2 decode 6 and 4 levels above their INIT captures. +- **Three levers remain:** + 1. Capture the INIT information later, by rebuilding it from rows a contract may read (open + question 1). Bank 0's INIT via f0 is the first instance; it saves 128, and banks 1–3 remain. + 2. Read endpoint rows at the consumer frame. Such reads pay no catch-up in the moment. Their + price is a read or observation-contract question outside the moment. One example is the + optional PR2468-style read invoice in the price gate. + 3. Compress records before they climb. At P_final this is still bounded by Theorem B's + per-cut form (at least 1,952 / 1,824). At multi-level timings it is bounded only under the + own-bank premise; otherwise it is open. + + Each changes P_obs or the uncompressed-delivery part of P_rank, so each is a different contract + from the one rejected here. + +### 7.3 Route (b): shared-source centre sharing over a one-call gap + +**Which pairs.** PR2199 lists six classes of same-replica shared-data pairs: f0→b1, b1→f2, +b3→f4, b5→f6, b7→f8 and f0→f2. + +- f0→f2 is the only class with a one-call gap: B1 lies between the two calls. So 16 eligible + pairs exist, one per replica. +- The other five classes are adjacent. + +**Information status: open.** No predecessor establishes an information obstruction for f0→f2. + +- **PR2199** computes formal pair ranks (16 for every dependent pair) in a calls-only + projection. It states that this is "not a native obstruction". It also says the projection + does not by itself give a lower bound for groupings, and that f0→f2 pairs share all 88 + destination owners. + - Its open question 2 asks for the fixed-dirt source-only rank of exactly these 16 f0→f2 + pairs. +- **#2391 and #2461** (navinor; ywz65) concern only the adjacent f0→b1 class, selected calls 0 + and 4. They give a native non-lift and 104 owner-local coordinates per owner. + +**Catch-up.** Suppose the information is present, and the sharing is realized as #1166 prices +it. Assume three premises: + +- the 8 shared rows are retained across B1 and consumed at pair 0's current frame in f2; +- they are independent modulo the rows the f2 consumer may combine there, an observation premise + of the P_obs type; +- P4. + +B1 advances pair 0 by one level between capture and reuse, so Corollary 4 charges at least 8 per +row. That is at least 64 per shared 8-row set, which equals the per-call centre charge the +sharing would save. The net moment gain is therefore at most 0, which is (C)'s ×1.000. (S)'s +×1.787 leaves out this catch-up. + +**Decision: no moment gain, conditional on the three premises above, by the catch-up argument +alone.** + +- If the shared rows could be rebuilt at f2's frame from rows the consumer may already combine, + the sharing would need no retention. That is a different mechanism, which this package does + not price. +- The information question is open (PR2199 open question 2). + +### 7.4 Route (c): the retention row of the QQ16 retained caller (clarification) + +**One charge, not two.** + +- **Value.** In the moment, the retention row of the #2540/#2651 caller is exactly 128, which + is PR2540's 16 H8. +- **Why it is forced.** It is Proposition 3(i) with ρ_r = 16 (PR2511's interface bound) and an + F_U1 consumer, and PR2540 attains it. +- **Consequence.** A "16 H8" row and a separate "retention" row would double-count it. +- **Holding is free.** Holding the records at F_L across B1 costs nothing in the moment + (Lemma 2). +- **Physical storage** of the 16 arrays across B1 is UNKNOWN. #2651 coalesces these arrays into + output banks. + +**Child shape.** The 128 cannot be realized more cheaply in the moment. Each of the 16 +independent rows must cross 8 cuts, and rule 3 allows one row per transport. So at most one +child of rank 8 is available per row, and rank-8 children are the cheapest per unit of mass. + +**The comparison with the zero-retention decoder is not ours.** + +- **The decoder.** #2707 (ywz65; `research/qq16-line-normalized-decoder`) refines Arham Tahir's + PR2681 to 336 H1 children, no H8 children, and no value retained across B1. +- **The comparison.** Its child moment beats PR2540's for 0 ≤ a ≤ 1/16. The difference has + numerator 112 − 16·8^(1−a), which is negative there because 8^15 > 7^16. +- **Status.** #2707, #2651 and PR2681 were incorporated on main after this package's base, in + integration commits `5d8817103` and `481b8711e`. +- **The maintainers' review.** The review in + `research/community-efficient1600-audit/combined-2707-review.json` on main records this + comparison. It also records #2707's surplus of 192 wrappers, 256 maps and 8,368 scalar + allowance. +- **Our check.** `verify.py` re-checks only the integer inequality. + +**Consequence for the #2617 gate: a clarification, not a new decision.** + +- The retention row cannot fall below 16 H8 for this interface in the moment. So further + moment-level retention work on the retained caller cannot change the comparison. +- The open task remains #2617's physical one: owners, streams and tape positions for the + sixteen early values, priced against #2707's non-moment surplus. +- Precision (PR2603 and the #2692 chain), travel (#2794), allocation (#2709) and the output + consumer (UNKNOWN) are unaffected. + +## 8. Scope and unresolved obligations + +- **Physical storage, tape and hosting windows of retained arrays** lie outside the moment and + are UNKNOWN. Lemma 2 neither prices nor dismisses them. +- **P_obs** is a premise of the QQ16 observation contract, not of the moment. + - A contract that reads endpoint rows at the consumer frame pays no catch-up in the moment. + - Its cost is a read-contract question that is not priced here. +- **P_rank for INIT64 + d_A**, and for its all-initial variant, rests on finite-model evidence + only. Its uncompressed-delivery part is our reading of the published contract, whose README + states only the storage lifetime. A compressing contract is a different one (§7.2, lever 3). +- **Consumer timing** is a premise, not a theorem. + - The stated contract is P_final. + - P_Y is the earliest timing under the final-value read convention of P_obs, for decoders + that use their own Y_(k,U). Under a span-based reading it is not a bound. + - P_early lower-bounds every timing at or after each bank's last local call, which is what + P_dec gives. P_dec is a property of the derived decoders, and it is load-bearing: without + it, the moment bound drops to 512 at one timing. P_early is not attainable under the read convention for banks + 1 and 2, and its ride-along assumption favours the route. + - Consumers whose outputs stay below the partners' frame are not priced. +- **Capture times** are the price gate's. Bank 0's INIT can be formed one level later via f0 + (−128 on every P_rank total, no verdict change). Later captures for banks 1–3 need an extra + read of the pair's transient Y (lever 1); one level later they would give P_early 832 / 640, + below 896, so the P_early verdict depends on the stated capture times (§7.2). +- **P4 (no slack in inherited words)** is supported by the coverage identity and PR1664 §5. It + is not re-derived event by event here. Slack exhibited in an inherited word would reduce the + forced catch-up by at most that slack. +- **P_glob** (pairs at equal levels share a frame) is supported by the bridge schedule. It is + used only to show that some costs are 0 (the all-initial reads at P_early and bank 0's read at + P_Y) and that the count-only Theorem B deliveries are attained. The rejection does not need it. +- **Theorem B** is an unreviewed posted claim, and our per-cut application of it is written + out in §7.2. + - Alone it rejects only at the end decoder (P_final), where every bank decodes at level 8. + - At P_Y and P_early it needs the own-bank premise in the strong reading of §7.2, which is + ours, not the claim's. +- **Forward histories.** The derived decoders use f2, f4, f6 and f8 (the tail identity holds for + every bank; bank 3 uses f8), and bank 0 also uses f0 (+512–576 / 128–192 / 128–192, AI review + pass). None of them is counted in the 464 array-calls. + - Suppose each is retained as one 8-row array, captured at its forward call's output level + (2, 4, 6, 8) or input level (1, 3, 5, 7). + - Then the law adds 768 to 1,024 under P_final, 384 to 640 under P_Y and 0 to 256 under + P_early. For f2, f4 and f6 alone the ranges are 768–960, 384–576 and 0–192. + - The row count is our reading of the 8-dimensional query outputs f = R_s x. The rejection + does not need these additions. +- **Non-nested frames.** Only nested chains are treated. + - For non-nested frames, d ≥ |Δh| still gives a lower bound. + - Gauges such as signed lines can add more (PR2678's 1,904). +- **Prices.** Break-evens are given for ideal idle packing (rank 51) and for rank-8 children. + The prices are ceilings, not attained exponents. +- **Frame-model checks** cover the stated finite domains only. Proposition 3 is proved in + general above. +- **No new κ, no supplier, no change to the selected frontier.** + +## 9. Credit + +- **Model and lemma.** The transport model and the cut lemma are Andrey Mas's (an664, PR1664), + with the GPT-6 Pro review it records. +- **Coverage.** The tree lemma and the coverage partition are ctoth's (#1516, #1587). The + coverage identity is PR1012's. +- **Idle-axis hosting** comes from the #434 lineage. +- **Native frames, interfaces and tariffs.** + - ywz65: PR2511, the source of ρ = 16; PR2540; #2707. + - Arham Tahir: PR2681, the zero-retention logical decoder that #2707 refines. + - petalas: the tariff (PR2678). + - 1337isnot1337: the private d_A floor (PR2197). +- **Philippe Van Velzen** contributed the conventions, the final-record census, the price gate, + the derived decoders, the all-initial variant and Theorem B. The fork commits are listed + below. +- **The precursor.** Philippe Van Velzen's sibling-helpers note anticipates Lemma 2 and + Corollary 4. On helper time-sharing it says "the bill is coordinate advances, not storage". + - The note is at fork `b5ce9d223feeed73d07e2a07321f7a025bd5865e`, + `research/complex-budget-law/closures-2/sibling-helpers/README.md`. + - Its author marks it LOCAL-ONLY, and here it was read as data only. +- **Information results.** navinor (#2391), ywz65 (#2461) and our PR2199. +- **Our PR2470** (`research/qq16-cut-retention-census`) screened PR2443's retained copies under + the assumed centre-like convention, 8 per coordinate-call. + - Its C = 0 limit of 111 coordinate-calls with any positive saving is the 896 threshold here. + - It also noted that a decoder that may read the whole post-B1 state needs no copy, which is + the endpoint-read lever of §7.2. + - Corollary 4 now derives that convention for current-frame consumers under P4. +- **Also credited:** + - Ross Richardson (PR2480); + - alephnan (PR2346); + - commdata2338 (PR2174, PR2651); + - the QQ16 lineage of Ali Romman; + - the maintainers' combined review of #2707. + +**Fork data.** These were read as data and never executed: + +- `philippeVV/integer-mult-bounds@9fcd3d899cc5bad2e27ab1d3d64d241cbfe30793`, + `research/joint-query-first-pair-catalogue/final-record/{price_gate.py, PRICE-GATE.json}`; +- the decoder at fork `40d58b9e`, which was cited but not read. + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). +Review so far consists of AI review passes in the same automated loop. There has been no human or +formal-kernel review. Apache-2.0. diff --git a/research/retained-array-catch-up/README.md b/research/retained-array-catch-up/README.md new file mode 100644 index 0000000000..1e384ee4ef --- /dev/null +++ b/research/retained-array-catch-up/README.md @@ -0,0 +1,514 @@ +# Retained-array catch-up in the transport moment: the forced price and the #1166 INIT64 + d_A decision + +**Research note: a scoped lemma and a conditional negative result. No new κ, no supplier, and the +selected frontier is unchanged.** + +Base commit `de880ca1fa4540472ee8461d400914a60fc9dd41`. Every pinned input has the same git blob on +main `304c32e6f11a1b024012ae6a61b155bfe13142ce` (checked through the GitHub API on 2026-10-16). + +The two conventions Philippe Van Velzen offered for a retained array are: + +- **(S):** 1 paid unit per array-call. +- **(C):** one rank-8 copy plus 8 units per array-call. + +**Summary.** + +- **Stakes.** [#1166 c18956869](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18956869) + (Philippe Van Velzen) asks how to price an array that is retained across calls but read by none + of them. The answer decides his INIT64 + d_A final-record route: + - under storage pricing (S) his price gate reports a complex κ ceiling of 0.00228, or 0.00221 + with PR2468-style read invoices. We reproduce the 0.00228 value exactly; the 0.00221 value is + quoted. The bit endpoint (0.0017334) caps either in practice; + - under centre-like pricing (C) it has no saving. +- **Result.** The answer holds in PR1664's scalar common-frame transport moment. + - Holding an array costs nothing. + - The consumer must bring the record to a common frame with its partners. That costs **8 + coordinates per level the source pair advances, for each record row that is independent of + the rows the consumer's contract lets it combine** (Corollary 4). + - For the stated contract this is (C)'s mass, up to a one-call lifetime off-by-one. + - INIT64 + d_A costs **3,648 units per replica** with the stated end-of-replica decoder. + - Decoding each bank as soon as its observed field is final (under the final-value read + convention) still costs at least **2,496**. + - Decoding each bank right after its last local call costs **1,344**. This lower-bounds every + timing at or after each bank's last local call, which is what the derived decoders' timing + (P_dec) gives. + - The all-initial variant costs 3,456, 2,304 and 1,152 under the same three timings. + - All are at least the exact **896-unit no-saving threshold**, so the (S) escape closes in this + model. Capturing bank 0's INIT information via f0 lowers each value by 128 and changes no + verdict. +- **Premises.** The rejection is conditional on the following, each defined under + [Premises](#premises): + - the stated observation contract with final-value reads (P_obs); + - P_rank, which has finite-model evidence only, with uncompressed delivery (our reading of the + published contract); + - the stated capture times; + - P4: no slack in the inherited words; + - current-frame consumers with the decoder-timing premise P_dec. It is load-bearing: at + decoders right after their own last captures the moment bound drops to 512, which leaves a + κ cap above the selected κ. No decoder is known to run there. + + Physical storage stays **UNKNOWN**. It can only add cost. +- **Without P_rank.** philippeVV's Theorem B still rejects the route at the end decoder + (P_final). At earlier timings, where banks decode at different levels, it needs an extra + own-bank premise. + +**Terms used below.** + +- **The law** means Corollary 4. +- **Idle-priced:** extra mass packed as ideal rank-51 idle children. +- **Rank-8-priced:** extra mass as rank-8 children, which is (C)'s shape. +- **Units** are paid coordinates per replica. +- **Data incidence:** a later local call of the record's own pair. + +## Statement + +[PROOF.md](PROOF.md) gives the statements and proofs. + +- Items 1 and 2 are theorems of the scalar common-frame transport model of + [PR1664](../dirty-host-cutrank-audit/PROOF.md). +- Item 3 also uses Fact T (the pinned template) and P4. +- Item 4's statements about the #1166 records also use P_obs and P_rank. + +1. **Storage is free in the moment (Lemma 2).** + - Holding an array at a fixed frame for any number of calls adds no paid mass. + - So (S) is not a consequence of the moment. Physical storage is a separate premise, and it + remains **UNKNOWN**. +2. **Catch-up is charged exactly (Proposition 3).** + - Take records R at height h_r and partners P at height h_p, with R ∩ P = 0. + - Delivering O ⊆ R ⊕ P at the consumer height h_c costs exactly + `min_L ρ_r|L−h_r| + ρ_p|L−h_p| + ρ_o|L−h_c|`. + - ρ_r is what only the records supply, ρ_p is what only the partners supply, and ρ_o = dim O. + Each rank is taken modulo the rows the consumer may combine. + - The minimum is attained at the median level, and it equals the sum of the + [PR1664](../dirty-host-cutrank-audit/PROOF.md) cut deficits. So the record may climb or the + partners may descend; the bound covers both. + - The consumer level is an explicit premise. +3. **Eight coordinates per level in the selected template (Fact T and Corollary 4, under P4).** + - The pinned #1094 template moves every pair through nine levels of eight coordinates each. + - A level is advanced either by the pair's own call or by an idle sweep. + - Between two level-boundary instants, a record consumed at its pair's current frame pays + **8 × ρ_r × (levels advanced)**. That is at least 8 ρ_r per later data incidence. + - Hosted residuals put some idle families between declared levels at other instants. Every + instant used below is checked to lie on a level boundary, in all 16 replicas (nine of them + after their time settles; see `independent_check.py` below). +4. **How the law compares with (S) and (C) (Proposition 5).** + - (C) is a special case: ρ_r equals the number of rows and the pair advances one level per + call. Under P_obs and P_rank every route (a) record satisfies this, so the (C) verdicts for + route (a) are derived here rather than assumed. + - (S) is not a moment price. As a stand-in for catch-up it under-prices current-frame + consumers by 8×. PR2540 costs 16 under (S), but the law forces 128 under PR2511's ρ = 16, + and PR2540 attains it. + - The law counts levels advanced by the source pair, not calls. In replica 0 (and in 12 of + the 16 replicas), pair 3's Y streams are untouched across six calls. A record of them costs 0 + under the law whatever ρ_r is, against 48 under (C) and 6 under (S). That record merely copies + an untouched stream, so the example only shows which variable the law counts. + - Lagging-pair records do not separate the law from (C). A pair-0 X record taken after B5 + equals the observed Y_(0,U) up to sign and frame, because X_(0,U) is last written at event + 6. So ρ_r = 0 (PROOF.md §6(c)). `verify.py` checks the schedule fact, and a control with + bridge 27 reversed fails. + +## Priced decisions + +Each row uses the pinned [`ceiling.py`](../complex-local-word-ceiling/ceiling.py) with +C = 0 and a free controller. Route (a) has three consumer timings, defined under +[Premises](#premises): P_final (stated), P_Y (earliest under the final-value read convention) +and P_early (each bank right after its last local call, a floor under P_dec). + +| Route | Law (units/replica) | Verdict | +|---|---:|---| +| (a) INIT64 + d_A final-record contract, stated end-of-replica decoder (P_final) | **3,648** | **Rejected** in the stated model. Anything ≥ 896 leaves no positive saving, and any non-negative storage price only adds. | +| (a) the same, each bank decoded as soon as its observed field Y_(k,U) is final (P_Y) | ≥ **2,496** | Also ≥ 896. A lower bound for every timing P_obs admits under the final-value read convention, for decoders that use their own Y_(k,U). | +| (a) the same, each bank decoded right after its last local call (P_early) | ≥ **1,344** = 8 per later data incidence | Also ≥ 896. A lower bound for every current-frame timing at or after each bank's last local call (P_dec), given the stated capture times (see Premises: capture times). | +| (a) without P_dec: decoders right after their own last captures (levels 1, 3, 5, 6) / right after each backward call (1, 3, 5, 7) | 512 / 640 (both variants) | **Not rejected by the moment argument** at 512: cap 0.0020286 idle-priced, above the selected κ. 640 still leaves a positive saving (cap 0.0013547, below the selected κ). So P_dec is load-bearing. No decoder is known to run at these timings; bank 3's needs f8, and keeping only bank 3 at F8 gives 768 (cap 0.00068, below the selected κ; AI review pass, not computed by `verify.py`). | +| (a) bank 0's INIT via f0 (one level later; PROOF.md §7.2, capture times) | 3,520 / ≥ 2,368 / ≥ 1,216 (all-initial 3,328 / 2,176 / 1,024) | Also ≥ 896; no verdict changes. | +| (a) all-initial variant (#2074 c18950926: d_A swapped for reads of the initial X_(1..3,U)) | 3,456 (P_final) / ≥ 2,304 (P_Y) / ≥ 1,152 (P_early), with each read taken at its latest admissible level | Also ≥ 896. Its reads cost 0 at P_early, so INIT64's catch-up is the binding term. The re-timing favours the route: the published variant's reads are live from event 0, which gives 4,416 / 3,264 / 2,112 in replica 0 (AI review pass). | +| (a) d_A records alone (P_final) | 960 | Also ≥ 896. | +| (a) Theorem B in place of P_rank (robustness; PROOF.md §7.2) | one level (P_final): 1,952 / 1,824. Own-bank premise: 1,344 / 1,216 (P_Y), 800 / 608 (P_early). Count only: 608 / 544 (P_Y), 112 / 0 (P_early) | P_final: ≥ 896, **rejected without P_rank**. Own-bank: P_Y ≥ 896; at P_early the best case, 608, caps κ at 0.0015234 idle-priced (0.0015144 rank-8-priced), below the selected 0.001672660197076918. Count only: if the stated captures are independent, the original variant at P_Y (608, same cap) is still below the selected κ; 544, 112 and 0 are **not decided** (caps above the selected κ). | +| (b) gap-1 shared-source centre sharing (the f0→f2 class) | ≥ 64 per shared set, equal to the 64 saved | **No moment gain** under the stated premises, by catch-up alone. The f0→f2 information question remains **open** (PR2199 open question 2). #2391/#2461 cover only the adjacent f0→b1 class. | +| (c) QQ16 retained caller #2540/#2651, retention row | exactly 128 = its 16 H8 | **Clarification only:** one charge, not two. It is proved under ρ = 16 with an F_U1 consumer, and PR2540 attains it. The moment comparison with zero-retention #2707 is #2707's own result: it wins for 0 ≤ a ≤ 1/16, because 8^15 > 7^16. It is now incorporated and reviewed. Storage is UNKNOWN. | + +### Premises + +The route (a) rows depend on these premises; PROOF.md §7.2 states each one. + +- **P_obs (observation contract).** + - The consumer may combine only: + - the contract observations (final selected fields, final completed-X fields Y_(k,U), the + forward histories); + - the stated records and reads, at their stated capture times. + - **Final-value reads.** The consumer may read a named observed field only once it holds its + final value. A stream holding a non-final value is transient, even when that value is a + fixed combination of final fields. For example, X_(1,U) after event 12 equals + Y_(0,U) − Y_(1,U). P_Y is relative to this convention; under a span-based reading it is not a + bound. + - Other endpoint rows, such as the former-Y ordinary endpoints, and transient stream contents + are excluded by the contract. This exclusion is a premise of the QQ16 observation contract + (qq16-final-record-obstruction §1), not a consequence of the transport moment. + - Without P_obs a record row may lie in the span of level-8 endpoint rows, which the moment + lets the consumer combine for free. The obstruction's kernel family is visible exactly + there. +- **P_rank.** + - The stated arrays below each cut are independent modulo everything P_obs allows above it, + including the retained history of those allowed rows (not the whole program's history). + - We read the published contract as delivering each needed array itself, uncompressed, to the + decoder that uses it. Its README states that "every retained array stays live until the final + decode", which is a storage-lifetime convention. Uncompressed delivery is our premise. Lemma 1 + counts ranks, so compression before the climb would be a different contract. + - The evidence is philippeVV's finite-model census and derived decoders. It is not a proof on + the actual cover. +- **Capture times.** As stated in the price gate: INIT just before each bank's first call, and + d_A right after its backward call. + - Local calls overwrite X_U, and no bridge writes X_(k,U) before bank k's first call. + - For banks 1–3, whose first call is backward, the stated INIT capture is the latest one that + needs no other read. + - Bank 0's first call F0 is forward and invertible through the observed f0 + (z = w + K_(0,U) f0). So its 16 INIT rows can be formed one level later, at F0's output + frame. This lowers every P_rank total by 128 and changes no verdict. + - *Sensitivity (AI review pass, not computed by `verify.py`).* The backward word is invertible + from the pair's post-call X' and Y' (CONSERVED-QQ16 (1)). A capture one level later that + also reads the pair's transient Y (with bank 0 via f0) gives P_final 3,136 / 2,944, + P_Y 1,984 / 1,792 and P_early 832 / 640. The P_final and P_Y values stay ≥ 896, but the + P_early values fall below 896 (caps 0.00034 / 0.00135, both still below the selected κ). + So the P_early no-saving verdict depends on the stated capture times. +- **P_dec (decoder timing).** Each bank's decoder uses an observation of its own pair that exists + only after that pair's last local call. + - The derived decoders (#2074 c18950926) do this: each uses f_(2k+2) and pair k's final + selected fields, both available only after F_(2k+2) (bank 3: F8, f8). In the tail identity + C_k = w_k + K_(2k+2) f_(2k+2), C_k is the final Y_(k,U) and w_k the initial Y_(k,U). An AI + review pass read philippeVV's decoder code (fork 40d58b9e, as data only) and confirmed this. + - P_dec is a property of those decoders, not of P_obs or the moment. + - It is load-bearing. At decoders right after their own last captures the moment bound is only + 512, and a negative control checks that P_early does not bound them. +- **Consumer timing.** Current-frame consumers. + - **P_final** is the stated contract: every bank decodes at the end, level 8. + - **P_Y** decodes bank k as soon as its observed field Y_(k,U) = −final X_(k,U) is final. + - X_(k,U) is last written at event 6 for bank 0 (level 2), and by bridges 27, 26 and 25 for + banks 1–3, which run at level 8. + - Other observations can only delay a decoder. So under the final-value read convention, + and for decoders that use their own Y_(k,U), P_Y is a lower bound for every timing P_obs + admits. + - **P_early** decodes each bank right after its last local call (levels 2, 4, 6, 8). + - For banks 1 and 2 it ignores the final-value read convention, so it is not attainable + under P_obs. + - Above the captures, catch-up only grows with the consumer level. So P_early lower-bounds + every current-frame timing at or after each bank's last local call, which is every timing + P_dec admits. It does not bound earlier decoders. + - It also assumes, in the route's favour, that the decoded fields ride the inherited idle + sweep for free. + - A consumer whose outputs must return to the bank's frame is covered automatically. +- **P4.** The inherited words have no slack, as the coverage identity 72W + 64N indicates. +- **ρ = 16 for PR2540.** This is PR2511's interface bound. +- **Own-bank premise** (the Theorem B rows at P_Y and P_early only). It is ours, not part of + Theorem B. The 62 rows split freely over the banks. In the strong reading needed for per-cut + additivity (PROOF.md §7.2, with proof), for each bank k: + - (i) bank k's needed rows D_k lie in W + span C_k, where W is what P_obs allows and C_k are + the captures its derived decoder uses; + - (ii) D_k ∩ (W + Σ_{l≠k} span C_l) = 0, where C_l are all the other banks' captures. +- **Equal levels share a frame (P_glob).** Every bridge in the schedule joins two pairs at equal + levels. P_glob is used only to show that some costs are 0 and that the count-only deliveries + are attained. No lower bound, and so no rejection, depends on it. + +### Comparison with the published conventions + +- (C) as published charges 8 × 464 = 3,712. +- The law equals (C) with uniform lifetimes, 8 × 456 = 3,648. +- The price gate counts bank 0's d_A as live for 8 calls. Under the convention it uses for INIT, + the count is 7. No verdict changes. +- The (S)-priced 464 array-calls reproduce PRICE-GATE.json's storage ceiling + 2285992139/1002285992139 (0.0022808 idle-priced) exactly. + +### Break-even catch-up mass + +Break-even catch-up mass per replica, the largest mass at which a route still gains: + +| Comparison point | κ | Idle-priced | Rank-8-priced | +|---|---:|---:|---:| +| Selected record (#1094) | 0.001672660197076918 | 579 | 576 | +| PR2474 (pending) | 0.001703676387993676 | 573 | 568 | +| #2843 (pending) | 0.00171865827784172 | 570 | 568 | +| #2848 (pending) | 0.00171865850830493 | 570 | 568 | +| #2857 (pending; opened after the base) | 0.00172009662868483 | 570 | 568 | +| PR589 bit endpoint | 0.001733427039589844 | 568 | 560 | + +- The pending rows reflect open PRs at review time. +- Break-even mass does not increase with κ, and `verify.py` checks this across the table. So any + claim between the selected record and the bit endpoint, such as #2853 or #2856, has its + break-even in [568, 579] idle-priced or [560, 576] rank-8-priced. +- **No-saving threshold: 896** units per replica, one unpaid coordinate for each of the 896 + families. It is exact; PROOF.md §7.2 gives the proof. + - Our PR2470 found the same threshold under the assumed centre-like convention: its C = 0 limit + of 111 coordinate-calls with any positive saving is 888 units, and 896 = 8 × 112. + `verify.py` checks the pinned row against it. + +## What is new + +- **The price, derived.** Philippe Van Velzen's price gate and the #1166 request assume (S) or + (C). This package derives which price the transport moment actually forces, and states the + observation premise it needs. It reprices both published variants of the #1166 route at three + consumer timings. +- **Theorem B's reach, made explicit.** Its global count of 62 rejects the route without P_rank + at the end decoder (P_final). At multi-level timings the count alone does not decide, except + for the original variant at P_Y against the selected record. +- **Which premises carry the verdict.** The decoder-timing premise P_dec and the final-value read + convention are named, and P_dec is shown to be load-bearing (512 without it). Bank 0's INIT + information is shown to be capturable one level later via f0. +- **Controls of a single law.** PR2540, PR2197 and PR2678 each pay one concrete frame charge. + They are reproduced here as controls of the law. The F_L → F_U1 upgrades in PR2492/PR2512 are + the same one-level climb, but they are not recomputed separately. +- **Earlier treatments.** + - PR2480 counts information only. + - The [centre-sharing overhead budget](../centre-sharing-overhead-budget/README.md) treats ΔH + abstractly. + - Our PR2470 ([qq16-cut-retention-census](../qq16-cut-retention-census/README.md)) priced + PR2443's retained copies under an assumed centre-like convention. Corollary 4 now derives + that convention for current-frame consumers under P4. PR2470 also noted that reading the + whole post-B1 state needs no copy, which is the endpoint-read lever below. +- **Precursor.** Philippe Van Velzen's sibling-helpers note says, for helper time-sharing, "the + bill is coordinate advances, not storage". + - It lives at `philippeVV/integer-mult-bounds@b5ce9d223feeed73d07e2a07321f7a025bd5865e`, + `research/complex-budget-law/closures-2/sibling-helpers/README.md`. + - Its author marks it LOCAL-ONLY. It is concurrent with this package and is credited as a + precursor. + +## Reproduce + +Run from the repository root. Only the standard library is needed. Local runs used CPython 3.14.4; +the registered replay in [VERIFY.json](VERIFY.json) uses Python 3.12, which was not available +locally. + +```sh +python3 -I -B research/retained-array-catch-up/verify.py # ~50 s +python3 -I -B research/retained-array-catch-up/independent_check.py # ~2 s +python3 scripts/research_package.py --package research/retained-array-catch-up --check-only +``` + +Expected output: + +```text +PASS_RETAINED_ARRAY_CATCH_UP pr2540=128 init64_dA=3648/2496/1344 all_initial=3456/2304/1152 dA_only=960 thmB_one_level=1952/1824 thmB_own_bank=1344/1216/800/608 thmB_count_only=608/544/112/0 without_P_dec=512/640 init0_via_f0=3520/2368/1216 array_calls=464/456 no_saving=896 breakeven_S=573 breakeven_C=71 zero_advance_calls=6 hosted_instants=21 frame_instances=34454/4044 negative_controls=17 no_new_kappa +PASS_RETAINED_ARRAY_CATCH_UP_INDEPENDENT pr2540=128 init64_dA=3648/2496/1344 all_initial=3456/2304/1152 dA_only=960 thmB_one_level=1952/1824 thmB_own_bank=1344/1216/800/608 thmB_count_only=608/544/112/0 zero_advance_calls=6 zero_advance_replicas=12/16 hosted_route_instants=21x16 breakeven_S=573 breakeven_C=71 no_saving=896 echelon_dijkstra_instances=2432 controls_rejected=2 +``` + +How to read the tokens: + +- `init64_dA` and `all_initial` are P_final / P_Y / P_early. +- `thmB_one_level` is original / all-initial at P_final. +- `thmB_own_bank` and `thmB_count_only` are original / all-initial at P_Y, then at P_early. +- `without_P_dec` is the original variant with decoders right after their own last captures / + right after each backward call. `init0_via_f0` is the original variant at P_final / P_Y / + P_early with bank 0's INIT formed via f0. + +`verify.py --write` regenerates [RESULT.json](RESULT.json). It refuses to replace a differing +file unless `--force` is also given. + +### What `verify.py` checks + +1. **Source pins.** It checks: + - 16 file pins and two archive-member pins; + - 36 verbatim premise lines, including the bridge and terminal semantics, the observation + list, the X_U updates of the local words, PR2199's open f0→f2 question and PR2470's + centre-like limit. +2. **Level timeline.** It replays the selected template's level timeline. + - The hosted and base schedules are equal. + - The base idle children have rank 8 per level, and hosted residuals never exceed that. + - Every bridge joins two pairs at equal levels. + - X_(k,U) is last written at events 6, 27, 26 and 25, and bridges 25–27 run with every pair at + level 8. + - **Hosting, replica 0, both directions.** It uses 21 instants: the seven route captures, the + four P_early consumers, the three all-initial reads with their consumers, and the four P_Y + consumers. + - No overshoot: every residual hosted on the pair by then belongs to a sweep that has already + reached the stated level. That is 14,290 slot checks over 3,644 distinct residual slots, + 4,173 of them at the seven captures. + - No undershoot: every residual of such a sweep has landed. That is 9,280 checks of slots + that have not landed yet. + - The window streams host nothing; pair 3's X streams host 160 residuals in that window. +3. **The law and routes.** It computes: + - the controls: PR2540 128, PR2197 144, PR2678 1,792 and 3,696, centre path 576; + - both variants of route (a) at P_final, P_Y and P_early; + - the Theorem B floors: the one-level cut sum, the own-bank floor and the count-only delivery + at each timing; + - one law for any consumer vector, which must reproduce both variants at all three timings; + - the timings without P_dec (512 and 640), bank 0's INIT via f0 (3,520 / 2,368 / 1,216; all-initial + 3,328 / 2,176 / 1,024; own-bank P_Y 1,216 / 1,088) and the per-term revival masses (d_A 960 / + 576 / 192; all-initial reads 768 / 384 / 0); + - the forward-history add-on for f2, f4, f6 and f8; + - the lagging example's schedule fact. +4. **Pricing.** With the pinned `ceiling.py` it checks: + - the 896 threshold, which agrees with PR2470's centre-like limit of 111 coordinate-calls; + - the #1166 break-evens 573 and 71, and the PRICE-GATE.json storage ceiling; + - the comparison table, including that break-even mass does not increase with κ; + - which route rows have no saving, which stay below the selected κ, and that the count-only + deliveries at 544, 112 and 0 stay above it; + - that 512 without P_dec leaves a cap above PR2474, that the d_A term 576 at P_Y beats the + selected record but not PR2474, and the all-initial INIT budgets 195 / 189 at P_Y. +5. **Frame model.** A breadth-first minimum is compared with Lemma 1 and the meeting formula. + - There are 34,454 record/partner instances, and in all of them opt = Σ deficits = min_L f. + They cover GF(2)² with 4 levels (2,432), GF(3)² with 3 levels (2,106) and GF(2)³ with 3 + levels (29,916), each domain complete. + - On 4,044 general instances the bound is sound, and it is tight on 3,999. PROOF.md §2 gives + the smallest non-tight case. +6. **Tensor toy.** A two-call rational toy runs 25 trials. + - Adding a record without catch-up gives a wrong output every time. + - The paid catch-up, or a partner descent, repairs it. + +### Negative controls that must fail + +There are 17 in total. Each of the 14 explicit ones must fail with its stated message, and +`verify.py` asserts the message: + +- a mutated idle `to_level`; +- PR2540 priced with 15 rows (120), or with two incidences (256); +- INIT bank 1 captured at level −1 (4,032); +- the window extended past the first touch of pair 3 (48); +- the window stretched into pair-3 Y hosting; +- a pair-1 residual of sweep 2 delayed to time 25 (undershoot); +- 464 array-calls under uniform lifetimes (456); +- a positive saving claimed to vanish at 895; +- a break-even at 574; +- the all-initial read barred from bank 0's consumer level (1,216); +- bridge 27 reversed so that it writes X_(0,U) (last write 27); +- Theorem B at P_early without the own-bank premise (112, not 800); +- P_early claimed as a floor for decoders right after their own last captures (512 < 1,344). + +The other three are an upward-only cut bound, which fails on 14,426 instances, and, in the tensor +toy, omitted catch-up and catch-up on the wrong axis. + +### What `independent_check.py` does differently + +It shares no code with `verify.py` and does not import `ceiling.py`. The independence lies in the +representation and the algorithms. Its base template is a byte-identical copy (same sha256) of the +same member, read from the PR2346-pinned #1042 archive. + +- **Coordinate sets.** Frames are explicit coordinate sets built from idle child **ranks**. The + declared level fields are only cross-checked. It recomputes every stated-capture route value + at all three timings, and the last writes of X_(k,U). + - Some values are computed by `verify.py` only: the timings without P_dec, bank 0's INIT via + f0, the per-term revival masses and the f8 add-on. An AI review pass in this loop reproduced + them in a separate scratch script, which is not part of the package. +- **Theorem B by enumeration.** It enumerates every split of the 62 rows over the banks for the + own-bank floor, takes nearest-consumer deliveries for the count-only value, and runs a direct + cut loop for the one-level sum. +- **Per-family hosted heights, all 16 replicas.** It replays the hosted template family by family: + local call +8, idle child +remaining rank, pooled slot +width at its own time. + - It requires one uniform height on all 224 families of the pair at the 21 route instants, in + every replica. + - Twelve instants (the 7 captures, the 4 P_early consumers and bank 0's P_Y consumer) are + checked under both conventions for equal times. + - The other 9 are read after their time settles: the P_Y consumers of banks 1–3 at time 88, + and the three all-initial reads with their consumers. The slots at those times belong to + that time's sweeps, which precede the instant in event order (PROOF.md Fact T). Under the + slots-last convention up to 5 of these 9 are not uniform (5 in replica 0; all 9 are uniform + under slots-first), so they are checked under one reading. + An AI review pass found that even then the worst per-owner P_Y mass is at least 2,064, which + is still at least 896. + - It finds that the zero-advance window holds in exactly 12 replicas, all except 4, 5, 6 and 11. +- **Different arithmetic.** It evaluates moments with `decimal` at 80 digits, and checks the 896 + threshold with exact rationals. +- **Different solver.** It runs Dijkstra over reduced echelon bases on 2,432 instances, plus two + controls. Each control must be rejected for its stated reason, and the count is enforced. + +## Scope, inherited assumptions and UNKNOWN obligations + +- **Physical storage, tape movement and hosting windows** for retained arrays lie outside the + moment and stay UNKNOWN. +- **Endpoint reads.** Any read of an endpoint row at the consumer frame pays no catch-up in the + moment. Its price is a question for the read and observation contract, outside the moment. +- **Premises.** All of the following are premises, listed in PROOF.md §8: + - P_obs with its final-value read convention; + - P_rank, with uncompressed delivery as our reading; + - the capture times; + - the consumer timing and P_dec; + - P4; + - PR2540's ρ = 16. +- **P_dec is load-bearing.** It is a property of the derived decoders. A decoder that ran before + its pair's last local call would no longer be bounded by the argument (512); whether a correct + decoder can run that early is not examined, and 512 is not claimed to be the minimum. +- **Theorem B.** It is a posted claim of #2074 that has not been reviewed. Our per-cut + application of it is written out in PROOF.md §7.2. Alone it rejects only at P_final; the + own-bank premise it needs at P_Y and P_early is ours. +- **Forward histories.** The derived decoders use f2, f4, f6 and f8; bank 3 uses f8, and bank 0 + also uses f0. None is in the 464 array-calls. + - If each is retained as one 8-row array, captured at its forward call's output or input + level, the law adds 768–1,024 under P_final, 384–640 under P_Y or 0–256 under P_early. + f0 would add a further 512–576 / 128–192 / 128–192 (AI review pass, not in `verify.py`). + - These only add, so the rejection does not depend on them. +- **Frames.** Only nested frames are modelled. Gauge terms, such as PR2678's signed-line 1,904 + row, are quoted rather than derived. +- **Prices.** They are ideal-packing ceilings, not attained exponents. +- **Finite checks.** These cover the stated domains only. The general statements are the + written proofs, which no human or formal kernel has checked. + +## Open next questions + +The same questions appear, structured, in [TASK.json](TASK.json). + +1. **Can the INIT information be captured late or read at the consumer frame?** + - *Why it matters.* INIT64's catch-up is the binding term of both variants: 1,920 at P_Y and + 1,152 at P_early. + - *Where a gain could still come from.* Per term, with the INIT information free: + - **P_final: no INIT lever suffices.** d_A alone costs 960, which is at least 896. The + all-initial reads alone cost 768, with cap 0.00067848, below the selected κ. + - **P_Y, original variant.** Its d_A term alone, 576, beats the selected record only at the + margin (cap 0.0016919) and loses to PR2474 and every pending claim. + - **P_Y, all-initial variant: the live target.** Its reads cost 384, leaving at most + 189 units (against PR2474) or 195 (against the selected record) for the INIT + information, against 1,920 now. + - *First step.* Bank 0 is done: its INIT rows can be formed at level 0 via f0, which saves + 128. For banks 1–3, find the latest cut at which the initial query information can still + be rebuilt from rows a contract may read. Then price that read with the law, and separately + as a read contract. + - *Blocked by.* No priced observation contract for endpoint or ordinary reads, and no + actual-cover proof of P_rank. +2. **Does the forward-history retention make any QQ16 decoder worse?** + - *First step.* Determine whether f2, f4, f6 and f8 are kept in data ports or in separate + arrays, then apply the law. +3. **What does physical storage cost?** This is the UNKNOWN that the moment cannot settle. + - *First step.* Bind one caller's 16 early arrays (#2651) to concrete streams and tape + positions across B1. Price that against #2707's surplus of 192 wrappers, 256 maps and 8,368 + scalars. +4. **Where do the F_U1 outputs go?** Name the consumer, and its frame, for the 224 F_U1 outputs + of #2540/#2707. Proposition 3 needs this premise. Handoff thread: #2657. +5. **A per-record-class schedule search.** Can idle sweeps be re-timed so that records sit in + zero-advance windows? + - PR1012 shows that restoration deferral is mass-neutral, so this is a real question. + - It was not attempted in this session. + +## Credit + +The full list is in PROOF.md §9. + +- **The model, the lemma and the lineage.** Andrey Mas (an664, PR1664), ctoth (#1516, #1587), + PR1012, and the idle-axis-hosting / #434 lineage. +- **The native frames, interfaces and tariffs.** + - ywz65: PR2511, the source of ρ = 16; PR2540; #2707; #2461. + - Arham Tahir: PR2681, the zero-retention lineage that #2707 refines. + - petalas (PR2678) and 1337isnot1337 (PR2197). +- **The conventions, census, price gate, decoders and Theorem B.** Philippe Van Velzen. +- **The information results.** navinor (#2391), ywz65 (#2461) and our PR2199. +- **The earlier retention screen.** Our PR2470. +- **Others.** + - Ross Richardson (PR2480); + - alephnan (PR2346); + - commdata2338 (PR2174, PR2651); + - Ali Romman's QQ16 lineage; + - the maintainers' combined review of #2707. + +### External sources, read as data + +These were read as data and never executed. Their pinned numbers are reproduced independently +here. + +- `philippeVV/integer-mult-bounds@9fcd3d899cc5bad2e27ab1d3d64d241cbfe30793`, + `research/joint-query-first-pair-catalogue/final-record/`: + - `price_gate.py`, sha256 `d4c2c077…cb39`; + - `PRICE-GATE.json`, sha256 `78eed8a0…53d0`; + - `README.md`. +- Discussion posts: #2074 c18940190 (Theorem B, fork `680d0997621a2cecfef2186ab143377658687825`), + c18950410 and c18950926 (the decoders and the all-initial variant). + +[SOURCES.json](SOURCES.json) records the full hashes. + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). +Review so far consists of AI review passes in the same automated loop. There has been no human or +formal-kernel review. Apache-2.0. diff --git a/research/retained-array-catch-up/RESULT.json b/research/retained-array-catch-up/RESULT.json new file mode 100644 index 0000000000..03f1d8c69d --- /dev/null +++ b/research/retained-array-catch-up/RESULT.json @@ -0,0 +1,939 @@ +{ + "frame_model": { + "domains": [ + { + "coverage": "complete", + "dim": 2, + "field": "GF(2)", + "independent_RP_pairs": 15, + "levels": 4, + "record_partner_instances": 2432, + "subspaces": 5 + }, + { + "coverage": "complete", + "dim": 2, + "field": "GF(3)", + "independent_RP_pairs": 23, + "levels": 3, + "record_partner_instances": 2106, + "subspaces": 6 + }, + { + "coverage": "complete", + "dim": 3, + "field": "GF(2)", + "independent_RP_pairs": 129, + "levels": 3, + "record_partner_instances": 29916, + "subspaces": 16 + } + ], + "general_instances": 4044, + "general_tight": 3999, + "record_partner_instances": 34454, + "upward_only_failures": 14426 + }, + "levels": [ + { + "after": "entry", + "pairs_0_3": [ + -1, + -1, + -1, + -1 + ] + }, + { + "after": "event 0 local_cover_sweep", + "pairs_0_3": [ + 0, + -1, + -1, + -1 + ] + }, + { + "after": "event 1 local_cover_sweep", + "pairs_0_3": [ + 1, + -1, + -1, + -1 + ] + }, + { + "after": "event 2 idle_cover_sweep", + "pairs_0_3": [ + 1, + 1, + -1, + -1 + ] + }, + { + "after": "event 3 bridge", + "pairs_0_3": [ + 1, + 1, + -1, + -1 + ] + }, + { + "after": "event 4 local_cover_sweep", + "pairs_0_3": [ + 2, + 1, + -1, + -1 + ] + }, + { + "after": "event 5 idle_cover_sweep", + "pairs_0_3": [ + 2, + 2, + -1, + -1 + ] + }, + { + "after": "event 6 bridge", + "pairs_0_3": [ + 2, + 2, + -1, + -1 + ] + }, + { + "after": "event 7 local_cover_sweep", + "pairs_0_3": [ + 2, + 3, + -1, + -1 + ] + }, + { + "after": "event 8 idle_cover_sweep", + "pairs_0_3": [ + 2, + 3, + 3, + -1 + ] + }, + { + "after": "event 9 bridge", + "pairs_0_3": [ + 2, + 3, + 3, + -1 + ] + }, + { + "after": "event 10 local_cover_sweep", + "pairs_0_3": [ + 2, + 4, + 3, + -1 + ] + }, + { + "after": "event 11 idle_cover_sweep", + "pairs_0_3": [ + 2, + 4, + 4, + -1 + ] + }, + { + "after": "event 12 bridge", + "pairs_0_3": [ + 2, + 4, + 4, + -1 + ] + }, + { + "after": "event 13 local_cover_sweep", + "pairs_0_3": [ + 2, + 4, + 5, + -1 + ] + }, + { + "after": "event 14 idle_cover_sweep", + "pairs_0_3": [ + 2, + 4, + 5, + 5 + ] + }, + { + "after": "event 15 bridge", + "pairs_0_3": [ + 2, + 4, + 5, + 5 + ] + }, + { + "after": "event 16 local_cover_sweep", + "pairs_0_3": [ + 2, + 4, + 6, + 5 + ] + }, + { + "after": "event 17 idle_cover_sweep", + "pairs_0_3": [ + 2, + 4, + 6, + 6 + ] + }, + { + "after": "event 18 bridge", + "pairs_0_3": [ + 2, + 4, + 6, + 6 + ] + }, + { + "after": "event 19 local_cover_sweep", + "pairs_0_3": [ + 2, + 4, + 6, + 7 + ] + }, + { + "after": "event 20 local_cover_sweep", + "pairs_0_3": [ + 2, + 4, + 6, + 8 + ] + }, + { + "after": "event 21 idle_cover_sweep", + "pairs_0_3": [ + 8, + 4, + 6, + 8 + ] + }, + { + "after": "event 22 idle_cover_sweep", + "pairs_0_3": [ + 8, + 8, + 6, + 8 + ] + }, + { + "after": "event 23 idle_cover_sweep", + "pairs_0_3": [ + 8, + 8, + 8, + 8 + ] + }, + { + "after": "event 24 idle_cover_sweep", + "pairs_0_3": [ + 8, + 8, + 8, + 8 + ] + }, + { + "after": "event 25 bridge", + "pairs_0_3": [ + 8, + 8, + 8, + 8 + ] + }, + { + "after": "event 26 bridge", + "pairs_0_3": [ + 8, + 8, + 8, + 8 + ] + }, + { + "after": "event 27 bridge", + "pairs_0_3": [ + 8, + 8, + 8, + 8 + ] + }, + { + "after": "event 28 terminal_Y_translations", + "pairs_0_3": [ + 8, + 8, + 8, + 8 + ] + }, + { + "after": "event 29 terminal", + "pairs_0_3": [ + 8, + 8, + 8, + 8 + ] + } + ], + "negative_controls_rejected": [ + "idle sweep to_level +1", + "PR2540 rows 16 -> 15", + "PR2540 two incidences", + "INIT bank-1 capture level -1", + "zero witness extended past first pair-3 touch", + "uniform lifetimes give 464 array-calls", + "witness window stretched into pair-3 Y hosting (time + 17)", + "hosted residual of sweep 2 delayed to time 25 (undershoot)", + "895 units/replica has no saving", + "break-even 574 (S) against PR2474", + "all-initial read of X_(1,U) barred from bank 0's consumer level", + "bridge 27 reversed (dst = 0): X_(0,U) written after the capture", + "Theorem B at P_early without the own-bank premise", + "P_early as a floor for decoders without the decoder-timing premise" + ], + "pricing": { + "breakeven_vs_PR2474": { + "C_array_calls": 71, + "S_array_calls": 573 + }, + "centre_path_576_kappa_cap": "0.0016824552169656", + "free_controller_C0_kappa_cap": "0.0047020509675915", + "mass_breakeven_units_per_replica": { + "PR2474": { + "idle_units": 573, + "kappa": "425919096998419/250000000000000000", + "rank8_units": 568 + }, + "PR2843": { + "idle_units": 570, + "kappa": "42966456946043/25000000000000000", + "rank8_units": 568 + }, + "PR2848": { + "idle_units": 570, + "kappa": "171865850830493/100000000000000000", + "rank8_units": 568 + }, + "PR2857": { + "idle_units": 570, + "kappa": "172009662868483/100000000000000000", + "rank8_units": 568 + }, + "bit_endpoint_PR589": { + "idle_units": 568, + "kappa": "1733427039589844234749/1000000000000000000000000", + "rank8_units": 560 + }, + "selected_1094": { + "idle_units": 579, + "kappa": "836330098538459/500000000000000000", + "rank8_units": 576 + } + }, + "no_saving_threshold_units_per_replica": 896, + "routes": { + "INIT64_plus_dA_C_published": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 3712 + }, + "INIT64_plus_dA_S_published": { + "idle_priced_kappa_cap": "0.0022807782977406", + "rank8_priced_kappa_cap": "0.0022704880238689", + "units_per_replica": 464 + }, + "INIT64_plus_dA_earliest_Y_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 2496 + }, + "INIT64_plus_dA_early_relaxation_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1344 + }, + "INIT64_plus_dA_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 3648 + }, + "all_initial_earliest_Y_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 2304 + }, + "all_initial_early_relaxation_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1152 + }, + "all_initial_init0_via_f0_earliest_Y_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 2176 + }, + "all_initial_init0_via_f0_early_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1024 + }, + "all_initial_init0_via_f0_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 3328 + }, + "all_initial_init0_via_f0_thmB_own_bank_earliest_Y": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1088 + }, + "all_initial_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 3456 + }, + "all_initial_thmB_count_only_earliest_Y": { + "idle_priced_kappa_cap": "0.0018603537513912", + "rank8_priced_kappa_cap": "0.0018505083492553", + "units_per_replica": 544 + }, + "all_initial_thmB_count_only_early_relaxation": { + "idle_priced_kappa_cap": "0.0047020509675915", + "rank8_priced_kappa_cap": "0.0047020509675915", + "units_per_replica": 0 + }, + "all_initial_thmB_one_level_end": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1824 + }, + "all_initial_thmB_own_bank_earliest_Y": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1216 + }, + "all_initial_thmB_own_bank_early_relaxation": { + "idle_priced_kappa_cap": "0.0015233811701210", + "rank8_priced_kappa_cap": "0.0015143670861515", + "units_per_replica": 608 + }, + "d_A_only_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 960 + }, + "init0_via_f0_earliest_Y_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 2368 + }, + "init0_via_f0_early_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1216 + }, + "init0_via_f0_law": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 3520 + }, + "init0_via_f0_thmB_own_bank_earliest_Y": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1216 + }, + "revival_all_initial_reads_earliest_Y": { + "idle_priced_kappa_cap": "0.0027003264953633", + "rank8_priced_kappa_cap": "0.0026902488262201", + "units_per_replica": 384 + }, + "revival_all_initial_reads_end": { + "idle_priced_kappa_cap": "0.0006784777963427", + "rank8_priced_kappa_cap": "0.0006734016736129", + "units_per_replica": 768 + }, + "revival_dA_term_earliest_Y": { + "idle_priced_kappa_cap": "0.0016919378975098", + "rank8_priced_kappa_cap": "0.0016824552169656", + "units_per_replica": 576 + }, + "revival_dA_term_end": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 960 + }, + "thmB_count_only_earliest_Y": { + "idle_priced_kappa_cap": "0.0015233811701210", + "rank8_priced_kappa_cap": "0.0015143670861515", + "units_per_replica": 608 + }, + "thmB_count_only_early_relaxation": { + "idle_priced_kappa_cap": "0.0041202745576597", + "rank8_priced_kappa_cap": "0.0041157971063159", + "units_per_replica": 112 + }, + "thmB_one_level_end": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1952 + }, + "thmB_own_bank_earliest_Y": { + "idle_priced_kappa_cap": null, + "rank8_priced_kappa_cap": null, + "units_per_replica": 1344 + }, + "thmB_own_bank_early_relaxation": { + "idle_priced_kappa_cap": "0.0005090718448615", + "rank8_priced_kappa_cap": "0.0005051036823380", + "units_per_replica": 800 + }, + "without_P_dec_after_backward_call": { + "idle_priced_kappa_cap": "0.0013546833794986", + "rank8_priced_kappa_cap": "0.0013462439630070", + "units_per_replica": 640 + }, + "without_P_dec_after_own_last_capture": { + "idle_priced_kappa_cap": "0.0020286289192494", + "rank8_priced_kappa_cap": "0.0020185264778401", + "units_per_replica": 512 + } + } + }, + "routes": { + "INIT64": [ + { + "bank": 0, + "capture_before_event": 0, + "capture_level": -1, + "consumer_level": 8, + "mass": 1152, + "rows": 16 + }, + { + "bank": 1, + "capture_before_event": 7, + "capture_level": 2, + "consumer_level": 8, + "mass": 768, + "rows": 16 + }, + { + "bank": 2, + "capture_before_event": 13, + "capture_level": 4, + "consumer_level": 8, + "mass": 512, + "rows": 16 + }, + { + "bank": 3, + "capture_before_event": 19, + "capture_level": 6, + "consumer_level": 8, + "mass": 256, + "rows": 16 + } + ], + "INIT64_plus_dA_early_consumer_mass": 1344, + "INIT64_plus_dA_mass": 3648, + "INIT64_plus_dA_y_mass": 2496, + "PR2540_early_records": { + "capture": "after F0 (event 0)", + "capture_level": 0, + "consumer": "F_U1 after B1 (event 1)", + "consumer_level": 1, + "mass": 128, + "rows": 16 + }, + "all_initial_variant": { + "early_mass": 1152, + "final_mass": 3456, + "reads": [ + { + "bank": 0, + "early_consumer_level": 2, + "early_mass": 0, + "early_read_after_event": 5, + "early_read_level": 2, + "final_mass": 384, + "latest_read_level": 2, + "levels_held_while_initial": [ + -1, + 1, + 2 + ], + "read": "B2 X_(1,U)", + "rows": 8, + "y_mass": 0 + }, + { + "bank": 1, + "early_consumer_level": 4, + "early_mass": 0, + "early_read_after_event": 11, + "early_read_level": 4, + "final_mass": 256, + "latest_read_level": 4, + "levels_held_while_initial": [ + -1, + 3, + 4 + ], + "read": "B4 X_(2,U)", + "rows": 8, + "y_mass": 256 + }, + { + "bank": 2, + "early_consumer_level": 6, + "early_mass": 0, + "early_read_after_event": 17, + "early_read_level": 6, + "final_mass": 128, + "latest_read_level": 6, + "levels_held_while_initial": [ + -1, + 5, + 6 + ], + "read": "B6 X_(3,U)", + "rows": 8, + "y_mass": 128 + } + ], + "source": "#2074 c18950926 item 2: the d_A records swapped for the reads B2 X_1U, B4 X_2U and B6 X_3U", + "y_mass": 2304 + }, + "array_calls": { + "C_mass_published": 3712, + "C_mass_uniform": 3648, + "S_units_published": 464, + "published": 464, + "uniform_lifetime": 456 + }, + "controls": { + "PR2197": 144, + "PR2540": 128, + "PR2678_common_FL": 1792, + "PR2678_entry": 3696, + "centre_path_per_replica": 576 + }, + "d_A": [ + { + "bank": 0, + "capture_after_event": 1, + "capture_level": 1, + "consumer_level": 8, + "mass": 448, + "rows": 8 + }, + { + "bank": 1, + "capture_after_event": 7, + "capture_level": 3, + "consumer_level": 8, + "mass": 320, + "rows": 8 + }, + { + "bank": 2, + "capture_after_event": 13, + "capture_level": 5, + "consumer_level": 8, + "mass": 192, + "rows": 8 + } + ], + "d_A_only_mass": 960, + "early_consumer_after_events": [ + 4, + 10, + 16, + 20 + ], + "early_consumer_levels": [ + 2, + 4, + 6, + 8 + ], + "forward_histories_addon": { + "early_mass_range": [ + 0, + 256 + ], + "f2_f4_f6_only": { + "P_Y": [ + 384, + 576 + ], + "P_early": [ + 0, + 192 + ], + "P_final": [ + 768, + 960 + ] + }, + "final_mass_range": [ + 768, + 1024 + ], + "histories": "f2, f4, f6, f8: one 8-row array each, captured at the forward call's output (low end) or input level", + "y_mass_range": [ + 384, + 640 + ] + }, + "hosting": { + "distinct_slots_checked": 3644, + "instants_checked": 21, + "pair3_X_hosted_slots_in_window": 160, + "pair3_Y_hosted_slots_in_window": 0, + "route_capture_slot_checks": 4173, + "slot_instant_checks": 14290, + "undershoot_slot_checks": 9280 + }, + "init0_via_f0": { + "all_initial": { + "P_Y": 2176, + "P_early": 1024, + "P_final": 3328 + }, + "init_capture_levels": [ + 0, + 2, + 4, + 6 + ], + "original": { + "P_Y": 2368, + "P_early": 1216, + "P_final": 3520 + }, + "thmB_one_level_end": { + "all_initial": 1824, + "original": 1952 + }, + "thmB_own_bank": { + "P_Y": { + "all_initial": 1088, + "original": 1216 + }, + "P_early": { + "all_initial": 608, + "original": 800 + }, + "P_final": { + "all_initial": 1824, + "original": 1952 + } + } + }, + "lagging_record_example": { + "C_mass": 24, + "calls_after_capture": 3, + "capture_level": 2, + "last_write_event_of_X0": 6, + "law_mass": 0, + "law_mass_if_independent_row": 48, + "levels_advanced": 6, + "pair0_events_after_capture": [ + "idle_cover_sweep", + "bridge src=0 dst=1", + "terminal_Y_translations", + "terminal" + ], + "record": "X_(0,U) captured after event 13, consumed at the end" + }, + "qq16_gate": { + "retained_caller_H8": 16, + "retained_caller_retention_mass": 128, + "sign_certificate": "8^15 > 7^16", + "zero_retention_H1_minus_retained_H1": 112 + }, + "revival_terms": { + "all_initial_reads_term": { + "P_Y": 384, + "P_early": 0, + "P_final": 768 + }, + "dA_term": { + "P_Y": 576, + "P_early": 192, + "P_final": 960 + } + }, + "theorem_B": { + "P_Y": { + "all_initial": { + "count_only": 544, + "one_level_cut_sum": null, + "own_bank": 1216 + }, + "original": { + "count_only": 608, + "one_level_cut_sum": null, + "own_bank": 1344 + } + }, + "P_early": { + "all_initial": { + "count_only": 0, + "one_level_cut_sum": null, + "own_bank": 608 + }, + "original": { + "count_only": 112, + "one_level_cut_sum": null, + "own_bank": 800 + } + }, + "P_final": { + "all_initial": { + "count_only": 1824, + "one_level_cut_sum": 1824, + "own_bank": 1824 + }, + "original": { + "count_only": 1952, + "one_level_cut_sum": 1952, + "own_bank": 1952 + } + } + }, + "without_decoder_timing_premise": { + "after_backward_call": { + "all_initial": 640, + "consumer_levels": [ + 1, + 3, + 5, + 7 + ], + "original": 640 + }, + "after_own_last_capture": { + "all_initial": 512, + "consumer_levels": [ + 1, + 3, + 5, + 6 + ], + "original": 512 + } + }, + "x_last_write_event": [ + 6, + 27, + 26, + 25 + ], + "x_last_write_levels_all_pairs": [ + [ + 2, + 2, + -1, + -1 + ], + [ + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8 + ], + [ + 8, + 8, + 8, + 8 + ] + ], + "y_consumer_levels": [ + 2, + 8, + 8, + 8 + ], + "zero_witness": { + "C_mass_per_array": 48, + "S_per_array": 6, + "calls_in_window": [ + 0, + 1, + 2, + 3, + 4, + 5 + ], + "capture": "entry", + "consumer_before_event": 14, + "consumer_before_time": 40, + "law_mass_per_array": 0, + "levels_advanced": 0, + "pair": 3, + "record_copies_an_untouched_stream": true, + "side": "Y (replica-0 families 784..895)" + } + }, + "schema": "retained-array-catch-up/1", + "sources": { + "anchored_premise_lines": 36, + "pinned_files": 16 + }, + "status": "PASS_RETAINED_ARRAY_CATCH_UP pr2540=128 init64_dA=3648/2496/1344 all_initial=3456/2304/1152 dA_only=960 thmB_one_level=1952/1824 thmB_own_bank=1344/1216/800/608 thmB_count_only=608/544/112/0 without_P_dec=512/640 init0_via_f0=3520/2368/1216 array_calls=464/456 no_saving=896 breakeven_S=573 breakeven_C=71 zero_advance_calls=6 hosted_instants=21 frame_instances=34454/4044 negative_controls=17 no_new_kappa", + "tensor_toy": { + "naive_wrong": 25, + "repaired_correct": 25, + "trials": 25, + "wrong_axis_wrong": 25 + } +} diff --git a/research/retained-array-catch-up/SOURCES.json b/research/retained-array-catch-up/SOURCES.json new file mode 100644 index 0000000000..f273c84d2c --- /dev/null +++ b/research/retained-array-catch-up/SOURCES.json @@ -0,0 +1,165 @@ +{ + "schema_version": 1, + "base_commit": "de880ca1fa4540472ee8461d400914a60fc9dd41", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/centre-owner-observation-floor/README.md", + "usage": "input", + "git_blob": "22522cb5e6d057f219da6a592ecf24fd24a5da74", + "sha256": "5f9079af7f45bff8d0b0acc8366f9c0def90fad9c8a38bab772b0ef13e3d5be0" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-local-word-ceiling/README.md", + "usage": "input", + "git_blob": "f5f742f8196da29d2c3f4dffb3c27685ca9401f6", + "sha256": "b60be039cb0e03e064a27407d0bce9e58908d793da5ee405c876de5aebfa5f81" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/dirty-host-cutrank-audit/PROOF.md", + "usage": "input", + "git_blob": "042fc663f14f0aff985984f201a1cdf89997d594", + "sha256": "2921c2c741ab5086a87c53340f18180ecc55675ca7dadc49579da32aba71d2f5" + }, + { + "path": "research/idle-axis-hosting/PROOF.md", + "usage": "input", + "git_blob": "4468a00349b4f68dce103e785a8392099435e1d6", + "sha256": "cfe34bf0b64259661312dae22c3a23adc5bf6f6326951eee5c1488ccfc347542" + }, + { + "path": "research/joint-query/README.md", + "usage": "input", + "git_blob": "2bf4fc0aa252c01242278cb58befc350acf7c85f", + "sha256": "419f076e46f5a6ce43efe30a608baed0a535034c388e1ac76a29a2026685ba77" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/qq16-complete-native-decoder/PROOF.md", + "usage": "input", + "git_blob": "6ae136c8baef4793f4f7ae630720afff6c23a953", + "sha256": "09d587f1d6bc250e90e29fa8751a40f45be79f1a8a56af0b645c144cefaefa46" + }, + { + "path": "research/qq16-cut-retention-census/README.md", + "usage": "input", + "git_blob": "83d2b42eed128a7a9e2151e47990ac8966b6d4f9", + "sha256": "796636d4d9824bc4959b00d9d2cbbfafec07c14e6845a1e238fb668a2f3d8adf" + }, + { + "path": "research/qq16-entry-frame-tariff/README.md", + "usage": "input", + "git_blob": "c53ee2870d1f8f92be80502b342a941fdbfefa2f", + "sha256": "cb0e658cfbdd3fb74a43b195665d3b13d5eb8e74294831daa05165128ad9ef5d" + }, + { + "path": "research/qq16-final-record-obstruction/PROOF.md", + "usage": "input", + "git_blob": "894b0281522cbf1c8183a6375cb3b76173aecc46", + "sha256": "109490f1d9c4288445e11e65e77616d84555ce9f212df97c81e6efde0c2ebf43" + }, + { + "path": "research/qq16-private-da-frame-floor-seed81b017/README.md", + "usage": "input", + "git_blob": "9ac44dcd2bae0482b3dbe2abc5ca2719de989cda", + "sha256": "8e4c3f1d2e76b110ef47aecdce8098c84403b969f8d6e386b0ecabb8173f091b" + }, + { + "path": "research/selected-centre-chrono-source-census/README.md", + "usage": "input", + "git_blob": "4fc0643eb118157575e60449820939809825a030", + "sha256": "0db44f2ce702ee1e5b11c9f8cd05517593bd259f45ae897437c58a1bd81b2943" + }, + { + "path": "research/selected-centre-quarter-native/README.md", + "usage": "input", + "git_blob": "8c9c6e182ca775e9f361545213c69348ecf4696d", + "sha256": "bfae0aff6aefc90b2afb8da76bc6d07b698deeabdbd758d01910d9fdb937ec72" + } + ], + "external_read_as_data": [ + { + "repository": "philippeVV/integer-mult-bounds", + "commit": "9fcd3d899cc5bad2e27ab1d3d64d241cbfe30793", + "path": "research/joint-query-first-pair-catalogue/final-record/price_gate.py", + "sha256": "d4c2c07758b589a619fd1821b1c70f1fc48eec1e07b37a27a89234f8ecd4cb39", + "usage": "capture-time premise and INIT_AC/DA_AC lifetimes; never executed" + }, + { + "repository": "philippeVV/integer-mult-bounds", + "commit": "9fcd3d899cc5bad2e27ab1d3d64d241cbfe30793", + "path": "research/joint-query-first-pair-catalogue/final-record/PRICE-GATE.json", + "sha256": "78eed8a0ab9ac703ce6b43645d745c7837f1920fbb8e788c9e857b33b8a353d0", + "usage": "storage_readsFalse, breakeven_storage, breakeven_centre (reproduced by verify.py)" + }, + { + "repository": "philippeVV/integer-mult-bounds", + "commit": "9fcd3d899cc5bad2e27ab1d3d64d241cbfe30793", + "path": "research/joint-query-first-pair-catalogue/final-record/README.md", + "sha256": "fc29c926948a85ce241f7b768941f2d0ecf2d5bede0da9bb71e2542e2c934925", + "usage": "contract and census description" + }, + { + "repository": "philippeVV/integer-mult-bounds", + "commit": "b5ce9d223feeed73d07e2a07321f7a025bd5865e", + "path": "research/complex-budget-law/closures-2/sibling-helpers/README.md", + "usage": "precursor quotation (LOCAL-ONLY note, concurrent)" + }, + { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074", + "comments": [ + "c18940190 (Theorem B; fork 680d0997621a2cecfef2186ab143377658687825)", + "c18950410 (final-record census and price gate)", + "c18950926 (derived decoders; all-initial variant)" + ], + "usage": "premises and route definitions" + }, + { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166", + "comments": [ + "c18956869 (the request answered here)" + ], + "usage": "question" + }, + { + "repository": "CrocSwap/integer-mult-bounds", + "commit": "0b61b222fcf5c96ba50cc9cee2eeb976d5a74b7f", + "path": "research/qq16-line-normalized-decoder/README.md; research/community-efficient1600-audit/combined-2707-review.json", + "usage": "#2707 comparison and maintainer review, incorporated after this package's base (cited, not pinned)" + } + ] +} diff --git a/research/retained-array-catch-up/TASK.json b/research/retained-array-catch-up/TASK.json new file mode 100644 index 0000000000..93219f2ed7 --- /dev/null +++ b/research/retained-array-catch-up/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 5, + "base_commit": "de880ca1fa4540472ee8461d400914a60fc9dd41", + "original_card": { + "id": "joint-query-controller", + "question": "Can one unresolved retention, output-consumer, hosting or physical-cost obligation complete a pinned QQ16 controller proposal within budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Design and price one consumer or retained-state boundary for a pinned local decoder, including final restoration.", + "Audit one claimed physical invoice or prove a target-specific obstruction for its explicit retention/hosting contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the QQ16 row in research-family-status.md. The fixed-first-pair witness remains scoped; pending #2540 adds early records and claims a complete local native decoder, but not a favorable global controller. Read its output-frame and ownership contract before designing another inverse.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Check live claims and pin the newest relevant completed local word (starting lead #2540). Choose one unresolved consumer, retention, whole-cover movement, hosting or precision obligation. Price the complete proposal and test that obligation; do not repeat its claimed local inverse or native reconstruction unless providing distinct independent verification.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder" + ] + }, + "scope_status": "refined", + "actual_scope": "Price the retention obligation itself: in the PR1664 scalar common-frame transport model, what paid mass does an array retained across calls force (storage versus frame catch-up), with the consumer level and the consumer's observation contract explicit; then apply it to the two #1166 c18956869 routes (the QQ16 INIT64+d_A final-record contract in both published variants; gap-1 shared-source centre sharing) and clarify the retention row of the QQ16 retained caller #2540/#2651.", + "scope_change_reason": "The card asks whether one unresolved retention/consumer/hosting obligation can complete a pinned QQ16 controller proposal. The live blocker was a pricing question, not a construction: #1166 c18956869 asked maintainers which retention convention (S) or (C) applies, and three routes (two in #1166, the #2540 caller row in #2617) depend on it. We derive the transport-model price instead of assuming a convention. Physical storage remains outside the moment and is recorded as UNKNOWN; no supplier is attempted.", + "bottleneck_link": "Retained query information is the QQ16 family's missing link to a composed recursive interface. This result fixes the moment price of that retention (frame catch-up: 8 coordinates per level advanced per record row independent of what the consumer's contract may combine). Under the stated observation contract with final-value reads (P_obs), P_rank with uncompressed delivery (our reading of the contract), P4, the stated capture times and current-frame consumers satisfying the decoder-timing premise P_dec (each bank's decoder uses an observation that exists only after its pair's last local call, as the derived decoders do), it rejects the INIT64+d_A final-record route in both published variants: 3648 / 3456 units per replica with the stated end decoder, at least 2496 / 2304 when each bank decodes as soon as its observed field is final (P_Y), and at least 1344 / 1152 for every timing at or after each bank's last local call (P_early); all exceed the exact 896 no-saving threshold. Bank 0's INIT via f0 lowers each by 128 and changes no verdict. P_dec is load-bearing: at decoders right after their own last captures the moment bound drops to 512 (kappa cap 0.0020286, above the selected kappa; no decoder is known to run there). The P_early value also depends on the stated capture times: an AI review pass found that captures one level later with an extra read of the transient Y give 832 / 640 at P_early (below 896, caps still below the selected kappa), while P_final and P_Y stay >= 896. Without P_rank, Theorem B (#2074) still rejects at the end decoder (1952 / 1824); at multi-level timings it needs an own-bank premise (1344 / 1216 at P_Y, both >= 896; 800 / 608 at P_early, below the selected kappa) and its count alone does not decide there except, for independent captures, the original variant at P_Y (deliveries of 608 / 544 and 112 / 0 meet it; 608 is below the selected kappa). It finds no moment gain for gap-1 centre sharing under its premises (the f0->f2 information question stays open), and clarifies that the #2540-style caller's retention row is its existing 16 H8, one charge. The remaining levers (late capture of INIT information, endpoint reads at the consumer frame, compression before the climb, physical storage) all lie in the observation contract or outside the moment.", + "budget_minutes": 180, + "stop_rule": "Stop if the frame-model search falsifies the min-cut, or a legal synchronization without paid mass appears (publish a parametrized price as a handoff instead). Otherwise stop after the package, the posts and one audit PR. No per-record-class schedule search; no census extensions.", + "outcome": "completed", + "evidence": "Written proofs (PROOF.md: Lemma 1 restated from PR1664, Lemma 2 storage neutrality, Proposition 3 exact both-direction meeting-level minimum, Corollary 4 eight coordinates per level, Proposition 5 S/C versus the law, with lagging-pair records shown not to separate the law from (C); section 7.2 per-cut application of Theorem B, valid alone for one consumer level, and the own-bank per-cut additivity proof under its strong reading). Finite exact checks: verify.py (pinned template levels and bridge levels, last writes of X_(k,U), two-sided hosting at 21 route instants in replica 0, controls, both route variants at three consumer timings, Theorem B floors, pinned ceiling.py pricing including the PRICE-GATE.json storage ceiling and PR2470's centre-like limit, 34,454 + 4,044 frame-model instances by BFS on complete domains, rational tensor toy, the decoder-timing counterexample 512 / 640, bank 0's INIT via f0, per-term revival masses, 17 negative controls with asserted failure messages) and independent_check.py (coordinate-set replay of a byte-identical template copy from a second pinned archive, Theorem B by split enumeration, per-family hosted height replay of all 16 replicas (12 instants under both equal-time conventions, the 9 time-88 and all-initial instants after their time settles), Decimal-80 moments, echelon Dijkstra on 2,432 instances, 2 controls rejected for their stated reasons). Premises are explicit and unproved here: P_obs (the QQ16 observation contract), P_rank (finite-model evidence only; uncompressed delivery is our reading of the published contract), the stated capture times, consumer timing (P_final stated; P_Y a lower bound under the final-value read convention; P_early a lower bound under P_dec, a property of the derived decoders), P4, PR2540's rho = 16 (PR2511), Theorem B (unreviewed) and, for its multi-level rows, our own-bank premise. P_glob is used only for zero costs and count-only deliveries. Physical storage is UNKNOWN. No human or formal-kernel review; review so far consists of AI passes in the same automated loop.", + "author": "thakrarsagar", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5): source reading, derivation, proofs, both checkers and package text, run in an automated research loop under thakrarsagar's direction. No human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Can the INIT information be captured later, or read at the consumer frame, under a priced observation contract?", + "why_it_matters": "INIT64's catch-up is the binding term of both published variants (1,920 units per replica at P_Y, 1,152 at P_early). At the end decoder no INIT lever suffices (d_A alone 960; all-initial reads alone 768, cap below the selected kappa); at P_Y the original variant's d_A term alone (576) loses to PR2474; the live target is the all-initial variant at P_Y, whose reads cost 384 and leave at most 189 units (vs PR2474) or 195 (vs the selected record) for the INIT information. Bank 0's INIT via f0 (saving 128) is a first instance; endpoint reads at the consumer frame pay no catch-up in the moment.", + "first_step": "For each bank, find the latest cut at which the initial query information can still be rebuilt from rows a contract may read, and price that read both with Corollary 4 and as a read contract.", + "blocked_by": "No priced observation contract for endpoint or ordinary reads; P_rank is finite-model evidence only." + }, + { + "question": "Do the forward query histories f2, f4, f6, f8 used by the derived final-record decoders add retention catch-up?", + "why_it_matters": "They are absent from the 464 array-call count; retained as one 8-row array each, they would add 768 (output-level capture) to 1,024 (input-level capture) units under an end decoder, 384 to 640 at P_Y, or 0 to 256 at P_early (f2, f4, f6 alone: 768-960, 384-576, 0-192).", + "first_step": "Identify whether the QQ16 words keep the forward histories in data ports or in separate arrays, then apply Corollary 4.", + "blocked_by": "The storage location of the histories in a complete controller is not specified." + }, + { + "question": "What does physical storage of the sixteen early arrays across B1 cost for the #2540/#2651 caller?", + "why_it_matters": "It is the only cost that could make the retained caller preferable to zero-retention #2707, whose surplus (192 wrappers, 256 maps, 8,368 scalars) is also outside the moment.", + "first_step": "Bind the sixteen arrays of #2651 to concrete streams and tape positions across B1 and compare with #2707's surplus in one physical cost model.", + "blocked_by": "No maintainer-accepted physical storage/tape price for new arrays; the moment cannot supply it (Lemma 2)." + }, + { + "question": "Which consumer, in which frame, accepts the 224 F_U1 outputs of #2540/#2707?", + "why_it_matters": "Proposition 3 needs the consumer level as a premise; a different consumer frame changes the catch-up from record climb to partner descent.", + "first_step": "Determine from pinned sources whether any caller contract names the frame of the next consumer (handoff thread #2657).", + "blocked_by": "No complete caller contract for the QQ16 decoder outputs is published." + }, + { + "question": "Can idle sweeps be re-timed so that retained records sit in zero-advance windows?", + "why_it_matters": "The law is zero while the source pair advances no level (pair 3 across six calls); restoration deferral is mass-neutral (PR1012), so window placement is a genuine design lever.", + "first_step": "For one route, list the records' source pairs and the idle sweeps that separate capture from consumption, and test one re-timing on the level timeline.", + "blocked_by": "Re-timing must preserve hosting windows and the selected endpoint contract; not attempted in this session." + } + ] +} diff --git a/research/retained-array-catch-up/VERIFY.json b/research/retained-array-catch-up/VERIFY.json new file mode 100644 index 0000000000..68c8ba235c --- /dev/null +++ b/research/retained-array-catch-up/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/centre-owner-observation-floor/README.md", + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-local-word-ceiling/README.md", + "research/complex-local-word-ceiling/ceiling.py", + "research/dirty-host-cutrank-audit/PROOF.md", + "research/idle-axis-hosting/PROOF.md", + "research/joint-query/README.md", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/qq16-complete-native-decoder/PROOF.md", + "research/qq16-cut-retention-census/README.md", + "research/qq16-entry-frame-tariff/README.md", + "research/qq16-final-record-obstruction/PROOF.md", + "research/qq16-private-da-frame-floor-seed81b017/README.md", + "research/selected-centre-chrono-source-census/README.md", + "research/selected-centre-quarter-native/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Primary: 16 source pins, two archive-member pins and 36 premise lines; selected #1094 template level timeline (8 coordinates per level; bridges join equal levels; X_(k,U) last written at events 6/27/26/25 with bridges 25-27 at level 8); two-sided hosting at 21 route instants in replica 0 (14,290 overshoot and 9,280 undershoot slot checks); catch-up law controls PR2540 128 / PR2197 144 / PR2678 1792,3696 / centre path 576; INIT64+d_A 3648 (P_final) / 2496 (P_Y) / 1344 (P_early, a floor under P_dec), all-initial 3456 / 2304 / 1152, d_A 960; Theorem B floors: one level 1952 / 1824, own-bank 1344 / 1216 (P_Y) and 800 / 608 (P_early), count-only deliveries 608 / 544 and 112 / 0; array-calls 464/456, zero-advance window, lagging example (X_(0,U) last written at event 6), forward-history add-on f2..f8, decoder timings without P_dec 512 / 640, bank 0's INIT via f0 3520 / 2368 / 1216 (all-initial 3328 / 2176 / 1024), per-term revival masses; pinned ceiling.py pricing (896 threshold = PR2470's centre-like limit, #1166 break-evens 573/71, PRICE-GATE.json storage ceiling, comparison table monotone in kappa, route verdicts); exact frame model (34,454 record/partner instances on complete GF(2)^2, GF(3)^2, GF(2)^3 domains with opt = cut bound = meeting formula; 4,044 general instances sound); two-call rational tensor toy; 17 negative controls with asserted failure messages; RESULT.json equality." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent: coordinate-set replay of a byte-identical base-template copy from the PR2346-pinned #1042 archive using idle child ranks; law values PR2540 128, INIT64+d_A 3648 / 2496 / 1344, all-initial 3456 / 2304 / 1152, d_A 960, X_(k,U) last writes; Theorem B by split enumeration (own-bank 1344 / 1216 / 800 / 608), nearest-consumer delivery (count-only 608 / 544 / 112 / 0) and a direct cut loop (one level 1952 / 1824); zero-advance window; per-family hosted height replay of the #1094 template in all 16 replicas at the 21 route instants: the 12 capture and P_early instants under both equal-time conventions, the 9 time-88 and all-initial instants after their time settles (PROOF.md Fact T); window holds in 12 replicas; Decimal-80 moment break-evens 573/71, exact-rational 896 threshold and route verdicts without ceiling.py; echelon-basis Dijkstra on 2,432 GF(2)^2 record/partner instances; 2 controls rejected for their stated reasons." + } + ] +} diff --git a/research/retained-array-catch-up/independent_check.py b/research/retained-array-catch-up/independent_check.py new file mode 100644 index 0000000000..85dbe162ce --- /dev/null +++ b/research/retained-array-catch-up/independent_check.py @@ -0,0 +1,525 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent second method for the retained-array catch-up package. + +Shares no code with verify.py and does not import ceiling.py. + + A. Frames as explicit coordinate sets. The base (non-replica) template schedule, read from a + byte-identical copy (same sha256) of the base member in the PR2346-pinned #1042 archive, is + replayed with each pair's applied coordinates stored as a Python set: a local call applies its + stage's eight coordinates; an idle sweep applies rank/8 stage blocks taken from the idle child + RANKS (its from/to level fields are only cross-checked, not used). A record snapshots its + family's set; catch-up = |consumer set - record set| x rows (the PR1664 nested-frame distance). + Recomputes PR2540, INIT64, d_A, the all-initial variant at three consumer timings (end, the + earliest timing the observed Y_(k,U) fields allow under final-value reads, and P_early: each bank + right after its last local call), the zero-advance window and the lagging-record example. Theorem B floors are recomputed by explicit + enumeration of the per-bank splits of the 62 rows (own-bank premise), by nearest-consumer + delivery (count only) and by a direct cut loop (one consumer level). + B. Hosted heights per family, in all 16 replicas. The selected #1094 hosted template is replayed + family by family (local call +8, idle child +remaining rank, pooled slot +width at its own + time), under both tie conventions for slots and events at equal times. Every capture, consumer + and read instant used by the routes must see one uniform height 8 x (level + 1) on all 224 + families of its pair, in every replica; the zero-advance window is reported per replica. + C. Moment arithmetic with decimal.Decimal at 80 digits (ln/exp from the decimal module): + the no-saving threshold, the #1166 break-evens 573 / 71 against PR2474, and the route verdicts. + D. Exact frame model by a different algorithm: Dijkstra over per-level reduced echelon bases + (membership by Gaussian elimination, not span enumeration), with the meeting-level formula + computed from ranks by elimination, on the complete GF(2)^2 / 4-level record-partner domain. + +Run from the repository root: python3 -I -B research/retained-array-catch-up/independent_check.py +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). +""" +import gzip +import hashlib +import heapq +import io +import itertools +import json +import sys +import tarfile +from decimal import Decimal as D, getcontext +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +ARCHIVE = ("research/community-frontier1042-audit/selected-replay.tar.gz", + "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754") +MEMBER = ("t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz", + "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518") +HOSTED = ("research/community-frontier1094-audit/selected-replay.tar.gz", + "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz", + "2acf02b418078e37090495c601fe550448751d4f35912757b13a1f778efc7760") +PR2540_PROOF = ("research/qq16-complete-native-decoder/PROOF.md", + "09d587f1d6bc250e90e29fa8751a40f45be79f1a8a56af0b645c144cefaefa46") + + +class Fail(Exception): + pass + + +def need(ok, message): + if not ok: + raise Fail(message) + + +# ------------------------------------------------------------------ A. coordinate sets +def template(): + raw = (ROOT / ARCHIVE[0]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == ARCHIVE[1], "archive pin") + with tarfile.open(fileobj=io.BytesIO(raw), mode="r:gz") as tar: + member = tar.getmember(MEMBER[0]) + data = tar.extractfile(member).read() + need(hashlib.sha256(data).hexdigest() == MEMBER[1], "template member pin") + return json.loads(gzip.decompress(data)) + + +def pr2540_frames(): + text = (ROOT / PR2540_PROOF[0]).read_text(encoding="utf-8") + need(hashlib.sha256(text.encode("utf-8")).hexdigest() == PR2540_PROOF[1], "PR2540 proof pin") + need("F_L=product_(j=0,...,8)" in text and "U1=" in text, "PR2540 frame statements") + f_l = set(range(0, 8 + 1)) # axes e0..e8 + f_u1 = set(range(0, 16 + 1)) # axes e0..e16 + need(f_l < f_u1, "nested frames") + return len(f_u1 - f_l) + + +def coordinate_replay(t): + stage_pair = {} + for e in t["recipe"]: + if e["kind"] == "local": + stage_pair[e["stage"]] = e["pair"] + rank = {c["child"]: c["rank"] for c in t["idle_children"] if c["port"] == 0} + applied = {p: set() for p in range(4)} # applied (stage block, axis) coordinates + next_block = {p: 0 for p in range(4)} # stage blocks are applied in order 0..8 + snapshots = [("entry", {p: frozenset(s) for p, s in applied.items()})] + for e in t["execution_schedule"][:30]: + kind = e["kind"] + if kind == "local_cover_sweep": + p = stage_pair[e["stage"]] + need(next_block[p] == e["stage"], "local call applies the next stage block") + applied[p] |= {(e["stage"], a) for a in range(8)} + next_block[p] += 1 + elif kind == "idle_cover_sweep": + p = e["pair"] + ranks = [rank.get(c, 0) for c in e["child_indices"]] + need(ranks[0] == ranks[1] and ranks[0] % 8 == 0, "idle child pair of equal multiple-of-8 rank") + blocks = ranks[0] // 8 + need(e["from_level"] + 1 == next_block[p] and e["to_level"] == next_block[p] - 1 + blocks, + "declared idle levels agree with rank/8 blocks") + for b in range(next_block[p], next_block[p] + blocks): + applied[p] |= {(b, a) for a in range(8)} + next_block[p] += blocks + snapshots.append((kind, {p: frozenset(s) for p, s in applied.items()})) + need(all(len(s) == 72 for s in applied.values()), "every pair ends with 72 applied coordinates") + return snapshots, stage_pair + + +def law(snapshots, stage_pair, t): + sched = t["execution_schedule"][:30] + end = snapshots[-1][1] + before = lambda i: snapshots[i][1] # state before schedule entry i + after = lambda i: snapshots[i + 1][1] + gap = lambda rec, cons, p: len(cons[p] - rec[p]) + local_idx = {k: [i for i, e in enumerate(sched) if e["kind"] == "local_cover_sweep" + and stage_pair[e["stage"]] == k] for k in range(4)} + out = {"PR2540": 16 * gap(after(0), after(1), 0)} + out["INIT"] = [16 * gap(before(local_idx[k][0]), end, k) for k in range(4)] + out["dA"] = [8 * gap(after([i for i in local_idx[k] if sched[i]["stage"] % 2][0]), end, k) for k in range(3)] + last = {k: after(local_idx[k][-1]) for k in range(4)} + init_early = [gap(before(local_idx[k][0]), last[k], k) for k in range(4)] + da_early = [gap(after([i for i in local_idx[k] if sched[i]["stage"] % 2][0]), last[k], k) for k in range(3)] + out["early"] = 16 * sum(init_early) + 8 * sum(da_early) + # All-initial variant: bank k reads the initial X_(k+1,U); pair k+1's set may be taken at any + # snapshot before its first call (no bridge writes X_(k+1,U) before it). + reads_final, reads_early = [], [] + for k in range(3): + first = local_idx[k + 1][0] + need(not any(e["kind"] == "bridge" and e["dst"] == k + 1 for e in sched[:first]), "X_(k+1,U) initial") + held = [snapshots[i][1][k + 1] for i in range(first + 1)] + reads_final.append(len(end[k] - before(first)[k + 1])) # coordinates per row + reads_early.append(min(len(last[k][k] ^ h) for h in held)) + out["allinit_final"] = 16 * sum(len(end[k] - before(local_idx[k][0])[k]) for k in range(4)) + 8 * sum(reads_final) + out["allinit_early"] = 16 * sum(init_early) + 8 * sum(reads_early) + out["allinit_reads"] = (reads_final, reads_early) + # P_Y: bank k's observed field Y_(k,U) = -final X_(k,U) is final only after the last write of X_(k,U) + # (local calls on pair k overwrite it; bridges with dst = k add into it). + last_write = [max(i for i, e in enumerate(sched) + if (e["kind"] == "local_cover_sweep" and stage_pair[e["stage"]] == k) + or (e["kind"] == "bridge" and e["dst"] == k)) for k in range(4)] + out["last_write"] = last_write + ycons = {k: after(last_write[k]) for k in range(4)} + out["y_levels"] = [len(ycons[k][k]) // 8 - 1 for k in range(4)] + init_rec = {k: before(local_idx[k][0]) for k in range(4)} + da_rec = {k: after([i for i in local_idx[k] if sched[i]["stage"] % 2][0]) for k in range(3)} + out["y_mass"] = (16 * sum(gap(init_rec[k], ycons[k], k) for k in range(4)) + + 8 * sum(gap(da_rec[k], ycons[k], k) for k in range(3))) + reads_y = [] + for k in range(3): + held = [snapshots[i][1][k + 1] for i in range(local_idx[k + 1][0] + 1)] + reads_y.append(min(len(ycons[k][k] ^ h) for h in held)) + out["allinit_y"] = 16 * sum(gap(init_rec[k], ycons[k], k) for k in range(4)) + 8 * sum(reads_y) + # Theorem B floors. Rows: (bank, count, list of admissible record coordinate sets of the source pair). + original = [(k, 16, [init_rec[k][k]]) for k in range(4)] + [(k, 8, [da_rec[k][k]]) for k in range(3)] + variant = [(k, 16, [init_rec[k][k]]) for k in range(4)] + [(k, 8, [snapshots[i][1][k + 1] for i in range(local_idx[k + 1][0] + 1)]) for k in range(3)] + timings = {"final": {k: end[k] for k in range(4)}, "Y": {k: ycons[k][k] for k in range(4)}, + "early": {k: last[k][k] for k in range(4)}} + out["thmB"] = {(name, label): thm_b(rows, cons) for name, cons in timings.items() + for label, rows in (("original", original), ("all_initial", variant))} + # Lagging example: the last write of X_(0,U) (local calls on pair 0, bridges into pair 0). + out["x0_last_write"] = max(i for i, e in enumerate(sched) + if (e["kind"] == "local_cover_sweep" and stage_pair[e["stage"]] == 0) + or (e["kind"] == "bridge" and e["dst"] == 0)) + out["x0_levels_after_13"] = len(end[0] - after(13)[0]) // 8 + touch = min(i for i, e in enumerate(sched) if + (e["kind"] == "local_cover_sweep" and stage_pair[e["stage"]] == 3) or + (e["kind"] == "idle_cover_sweep" and e["pair"] == 3 and e["to_level"] > e["from_level"]) or + (e["kind"] == "bridge" and 3 in (e["src"], e["dst"]))) + out["zero_witness"] = (gap(snapshots[0][1], before(touch), 3), + sum(1 for e in sched[:touch] if e["kind"] == "local_cover_sweep")) + return out + + +def thm_b(rows, cons, need_rows=62): + """(own-bank floor, count-only delivery, one-level cut sum or None) from coordinate sets.""" + own_costs = {} + for bank, n, recs in rows: + below = [len(cons[bank] - r) for r in recs if r <= cons[bank]] + need(below, "own-bank capture below its consumer") + own_costs.setdefault(bank, []).extend([min(below)] * n) + prefix = {b: [sum(sorted(c)[:i]) for i in range(len(c) + 1)] for b, c in own_costs.items()} + banks = sorted(prefix) + own = min(sum(prefix[b][i] for b, i in zip(banks, split)) + for split in itertools.product(*[range(len(prefix[b])) for b in banks]) if sum(split) == need_rows) + free = sorted(min(len(c ^ r) for c in cons.values() for r in recs) for _, n, recs in rows for _ in range(n)) + count_only = sum(free[:need_rows]) + one_level = None + if len({frozenset(c) for c in cons.values()}) == 1: + top = len(next(iter(cons.values()))) + heights = [(n, max(len(r) for r in recs)) for _, n, recs in rows] + one_level = sum(max(0, need_rows - sum(n for n, h in heights if h >= j)) for j in range(1, top + 1)) + return own, count_only, one_level + + +# ------------------------------------------------------------------ B. Decimal moments +getcontext().prec = 80 +M, W = D(73), D(896) / D(9) +R_IDLE = 51 + + +def child(r, a): + return (D(r) / M) ** (1 - a) if r else D(0) + + +def relax(local, extra_rank8, extra_units, a): + """Per-call moment: QQ16 5F+4B words, extra mass, idle remainder as rank-51 mass.""" + total = 72 * W + extra_units + mass = sum(D(r) * n for r, n in local.items()) + 8 * extra_rank8 + idle = total - mass + need(idle >= 0, "coverage law") + s = sum(n * child(r, a) for r, n in local.items()) + extra_rank8 * child(8, a) + idle / R_IDLE * child(R_IDLE, a) + return s / W + + +def qq16_words(): + core = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82} + return {r: (5 * (n + (8 if r == 1 else 0)) + 4 * (n + (24 if r == 1 else 0))) / D(9) for r, n in core.items()} + + +def gains(units, pricing, kappa): + a = kappa / (1 - kappa) + local = qq16_words() + per_call = D(units) / D(9) + value = relax(local, per_call / 8 if pricing == "rank8" else D(0), per_call, a) + return value < 1, abs(value - 1) + + +def decimal_checks(): + pr2474 = D("0.001703676387993676") + out = {} + for pricing, step, expect in (("idle", 1, 573), ("rank8", 8, 71)): + ok_lo, m_lo = gains(expect * step, pricing, pr2474) + ok_hi, m_hi = gains((expect + 1) * step, pricing, pr2474) + need(ok_lo and not ok_hi, "break-even %s = %d" % (pricing, expect)) + need(min(m_lo, m_hi) > D(10) ** -40, "decision margin far above precision") + out["breakeven_" + pricing] = expect + # No positive saving, exactly (rationals): at a = 0 every child costs r/m, so the moment is + # total/(m w) = (72 w + u/9)/(73 w), which is >= 1 iff u >= 9 w = 896 units per replica; and + # every child cost (r/m)^(1-a) >= r/m for a >= 0, so the moment only grows with a. + from fractions import Fraction as F + w = F(896, 9) + need(all(((72 * w + F(u, 9)) / (73 * w) >= 1) == (u >= 896) for u in range(0, 2000)), "896 threshold") + local = qq16_words() + for units in (3648, 3712, 2496, 1344, 960, 3456, 2304, 1152, 1952, 1824, 1216): + need(relax(local, 0, D(units) / 9, D(0)) > 1, "no saving at %d" % units) + sel = D("0.001672660197076918") + a_sel = sel / (1 - sel) + for units in (800, 608): # own-bank P_early floors; 608 is also the count-only P_Y original + need(relax(local, 0, D(units) / 9, D(0)) < 1 and relax(local, 0, D(units) / 9, a_sel) > 1, + "%d units: positive ceiling, but cannot reach the selected kappa (Decimal)" % units) + for units in (544, 112, 0): # count-only deliveries: the count alone does not decide + need(relax(local, 0, D(units) / 9, a_sel) < 1, "%d units still beat the selected kappa" % units) + ok, _ = gains(464, "idle", D("0.00221")) + need(ok, "S-priced 464 array-calls keeps a ceiling above 0.00221 (the price gate's read-invoice value)") + out["threshold"] = 896 + return out + + +# ------------------------------------------------------------------ C. echelon Dijkstra +P = 2 + + +def pivot(row): + return next(i for i, x in enumerate(row) if x) + + +def reduce(basis, v): + """Reduce v by a fully reduced GF(2) echelon basis (distinct pivots, zero pivot columns elsewhere).""" + v = list(v) + for row in basis: + if v[pivot(row)]: + v = [(x + y) % P for x, y in zip(v, row)] + return tuple(v) + + +def insert(basis, v): + r = reduce(basis, v) + if not any(r): + return basis + k = pivot(r) + rows = [tuple((x + y) % P for x, y in zip(row, r)) if row[k] else row for row in basis] + return tuple(sorted(rows + [r], key=pivot)) + + +def rank(vectors): + b = () + for v in vectors: + b = insert(b, v) + return len(b) + + +def members(basis): + out = set() + for coeffs in itertools.product(range(P), repeat=len(basis)): + v = tuple(0 for _ in range(2)) + for c, row in zip(coeffs, basis): + v = tuple((x + c * y) % P for x, y in zip(v, row)) + out.add(v) + return out + + +def dijkstra(entry, demand, H): + start = [()] * (H + 1) + for v, h in entry: + start[h] = insert(start[h], v) + start = tuple(start) + best = {start: 0} + heap = [(0, start)] + while heap: + d, s = heapq.heappop(heap) + if d > best[s]: + continue + if all(not any(reduce(s[h], v)) for v, h in demand): + return d + for h in range(H + 1): + for v in members(s[h]): + if not any(v): + continue + for g in (h - 1, h + 1): + if 0 <= g <= H and any(reduce(s[g], v)): + n = list(s) + n[g] = insert(s[g], v) + n = tuple(n) + if d + 1 < best.get(n, 10 ** 9): + best[n] = d + 1 + heapq.heappush(heap, (d + 1, n)) + need(False, "unreachable") + + +def frame_checks(): + vecs = [v for v in itertools.product(range(P), repeat=2) if any(v)] + spaces = [()] + [(v,) for v in vecs] + [tuple(vecs[:2])] + count = 0 + H = 3 + for R in spaces: + for Pp in spaces: + if rank(list(R) + list(Pp)) != len(R) + len(Pp): + continue + b = () + for v in list(R) + list(Pp): + b = insert(b, v) + whole = members(b) + for O in spaces: + if not O or not all(v in whole for v in O): + continue + rho_r = rank(list(Pp) + list(O)) - rank(list(Pp)) + rho_p = rank(list(R) + list(O)) - rank(list(R)) + rho_o = rank(list(O)) + for hr, hp, hc in itertools.product(range(H + 1), repeat=3): + entry = [(v, hr) for v in R] + [(v, hp) for v in Pp] + demand = [(v, hc) for v in O] + opt = dijkstra(entry, demand, H) + formula = min(rho_r * abs(x - hr) + rho_p * abs(x - hp) + rho_o * abs(x - hc) + for x in range(H + 1)) + need(opt == formula, "meeting formula = Dijkstra optimum at %s" % ((R, Pp, O, hr, hp, hc),)) + count += 1 + return count + + +def hosted_template(): + raw = (ROOT / HOSTED[0]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == HOSTED[1], "hosted archive pin") + with tarfile.open(fileobj=io.BytesIO(raw), mode="r:gz") as tar: + data = tar.extractfile(tar.getmember(HOSTED[2])).read() + need(hashlib.sha256(data).hexdigest() == HOSTED[3], "hosted template pin") + return json.loads(gzip.decompress(data)) + + +def hosted_heights(h, replica): + """Per-family height (applied coordinates) of every family of one replica at the route instants.""" + sched = [e for e in h["execution_schedule"] if e.get("replica") == replica] + need([e["source_event"] for e in sched] == list(range(30)), "replica schedule of 30 events") + pair_of_stage = {e["stage"]: e["pair"] for e in h["recipe"] if e["kind"] == "local"} + base = 896 * replica + by_child = {} + for c in h["idle_children"]: + if c["replica"] == replica: + by_child.setdefault(c["child"], []).append(c) + steps = {f: [] for f in range(896)} # (time, event index or None, delta) + for i, e in enumerate(sched): + if e["kind"] == "local_cover_sweep": + p = pair_of_stage[e["stage"]] + for f in range(224 * p, 224 * p + 224): + steps[f].append((e["time"], i, 8)) + elif e["kind"] == "idle_cover_sweep": + for c in e["child_indices"]: + for row in by_child.get(c, []): + steps[row["family"] - base].append((e["time"], i, row["rank"])) + for slot in h["hosting"]["pooled_slots"]: + if slot["owner_replica"] == replica: + steps[slot["family"] - base].append((slot["time"], None, slot["width"])) + need(all(sum(d for _, _, d in steps[f]) == 72 for f in steps), "every family ends with 72 coordinates") + + def height(f, idx, after, tie): + """Just before (after=False) or after event idx; tie 0 puts equal-time slots first, tie 1 last.""" + t = sched[idx]["time"] + total = 0 + for time, i, d in steps[f]: + if i is not None: + total += d if (i < idx or (after and i == idx)) else 0 + elif time < t or (time == t and tie == 0): + total += d + return total + + def settled(f, t): + """After every event and slot at times <= t.""" + return sum(d for time, _, d in steps[f] if time <= t) + + def uniform(values): + vals = set(values) + need(len(vals) == 1, "one uniform height on the pair at a route instant (replica %d)" % replica) + return vals.pop() + + fams = lambda p: range(224 * p, 224 * p + 224) + out = {} + for tie in (0, 1): + out["INIT", tie] = [uniform(height(f, i, False, tie) for f in fams(k)) for k, i in enumerate((0, 7, 13, 19))] + out["dA", tie] = [uniform(height(f, i, True, tie) for f in fams(k)) for k, i in enumerate((1, 7, 13))] + out["early", tie] = [uniform(height(f, i, True, tie) for f in fams(k)) for k, i in enumerate((4, 10, 16, 20))] + # P_Y: bank 0 right after event 6; banks 1-3 after bridges 27/26/25, read once their time (the final + # sweeps' time) has settled, since residual slots at that time belong to the final sweeps. + out["Y", tie] = [uniform(height(f, 6, True, tie) for f in fams(0))] + \ + [uniform(settled(f, sched[i]["time"]) for f in fams(k)) for k, i in ((1, 27), (2, 26), (3, 25))] + out["y3_window", tie] = {height(f, 14, False, tie) for f in range(784, 896)} + times = [sched[i]["time"] for i in (5, 11, 17)] + out["allinit_read"] = [uniform(settled(f, t) for f in fams(k + 1)) for k, t in enumerate(times)] + out["allinit_consumer"] = [uniform(settled(f, t) for f in fams(k)) for k, t in enumerate(times)] + t14 = sched[14]["time"] - sched[0]["time"] + out["t14"] = t14 + out["x3_early"] = sum(1 for slot in h["hosting"]["pooled_slots"] + if slot["owner_replica"] == replica and 672 <= slot["family"] - base < 784 + and slot["time"] < sched[14]["time"]) + return out + + +def controls(t): + """Negative/positive controls for the independent method (each must behave as stated).""" + rejected = 0 + need(dijkstra([((1, 0), 0)], [((1, 0), 3)], 3) == 3, "positive control: one row climbs three levels") + need(dijkstra([((1, 0), 0), ((0, 1), 3)], [((1, 1), 3)], 3) == 3, "positive control: record climb to partner") + need(dijkstra([((1, 0), 0), ((0, 1), 3)], [((1, 1), 0)], 3) == 3, "positive control: partner descent") + bad = json.loads(json.dumps(t)) + sweep = next(e for e in bad["execution_schedule"][:30] if e["kind"] == "idle_cover_sweep" and 4 in e["child_indices"]) + for e in bad["idle_children"]: + if e["port"] == 0 and e["child"] in sweep["child_indices"]: + e["rank"] -= 8 # drop one stage block from both children of pair 2's first idle sweep + try: + coordinate_replay(bad) + except Fail as exc: + need(str(exc) == "declared idle levels agree with rank/8 blocks", "control 1 rejected for the stated reason") + rejected += 1 + # A formula without the output-transport term must disagree with the optimum somewhere. + wrong = sum(1 for hr, hp, hc in itertools.product(range(4), repeat=3) + if dijkstra([((1, 0), hr), ((0, 1), hp)], [((1, 1), hc)], 3) + != min(abs(x - hr) + abs(x - hp) for x in range(4))) + need(wrong > 0, "negative control: dropping the output term must fail") + rejected += 1 + return rejected + + +def main(): + t = template() + snapshots, stage_pair = coordinate_replay(t) + v = law(snapshots, stage_pair, t) + need(pr2540_frames() == 8 and v["PR2540"] == 128, "PR2540: 16 x |F_U1 - F_L| = 16 x 8 = 128") + need(v["INIT"] == [1152, 768, 512, 256] and v["dA"] == [448, 320, 192], "INIT / d_A climbs") + total = sum(v["INIT"]) + sum(v["dA"]) + need(total == 3648, "INIT64 + d_A = 3648") + need(sum(v["dA"]) == 960, "d_A alone 960") + need(v["last_write"] == [6, 27, 26, 25] and v["y_levels"] == [2, 8, 8, 8] and v["y_mass"] == 2496, + "X_(k,U) last written at events 6/27/26/25; earliest Y-allowed consumers 2/8/8/8; 2496") + need(v["early"] == 1344, "P_early 1344") + need(v["allinit_reads"] == ([48, 32, 16], [0, 0, 0]), "all-initial reads: 8 x 48/32/16 at the end, 0 at P_early") + need((v["allinit_final"], v["allinit_y"], v["allinit_early"]) == (3456, 2304, 1152), "all-initial variant 3456 / 2304 / 1152") + tb = v["thmB"] + need(tb["final", "original"] == (1952, 1952, 1952) and tb["final", "all_initial"] == (1824, 1824, 1824), + "Theorem B, one consumer level: cut loop = own-bank = count-only = 1952 / 1824") + need((tb["Y", "original"], tb["Y", "all_initial"], tb["early", "original"], tb["early", "all_initial"]) + == ((1344, 608, None), (1216, 544, None), (800, 112, None), (608, 0, None)), + "Theorem B own-bank 1344/1216 (Y), 800/608 (early); count-only 608/544 (Y), 112/0 (early)") + need(v["x0_last_write"] == 6 and v["x0_levels_after_13"] == 6, "X_(0,U) last written at event 6 (lagging example)") + need(v["zero_witness"] == (0, 6), "zero-advance window: no coordinate applied to pair 3 across six calls") + dec = decimal_checks() + n = frame_checks() + rejected = controls(t) + need(rejected == 2, "both independent controls rejected") + h = hosted_template() + window_ok = [] + for replica in range(16): + hh = hosted_heights(h, replica) + for tie in (0, 1): + need(hh["INIT", tie] == [0, 24, 40, 56] and hh["dA", tie] == [16, 32, 48] + and hh["early", tie] == [24, 40, 56, 72] and hh["Y", tie] == [24, 72, 72, 72], + "hosted heights at captures and consumers (replica %d, tie convention %d)" % (replica, tie)) + need(hh["allinit_read"] == [24, 40, 56] and hh["allinit_consumer"] == [24, 40, 56], + "all-initial read and consumer at one level after the sweep time settles (replica %d)" % replica) + if hh["y3_window", 0] == hh["y3_window", 1] == {0}: + window_ok.append(replica) + if replica == 0: + need((hh["t14"], hh["x3_early"]) == (40, 160), "window ends at time 40; pair-3 X streams host 160 residuals in it") + need(window_ok == [0, 1, 2, 3, 7, 8, 9, 10, 12, 13, 14, 15], + "zero-advance window on the pair-3 Y streams holds in 12 replicas (not 4, 5, 6, 11)") + n_inst = sum(len(hh[key]) for key in (("INIT", 0), ("dA", 0), ("early", 0), ("Y", 0), "allinit_read", "allinit_consumer")) + need(n_inst == 21, "21 route instants at exact hosted heights") + print("PASS_RETAINED_ARRAY_CATCH_UP_INDEPENDENT pr2540=128 init64_dA=%d/2496/1344 all_initial=3456/2304/1152 dA_only=960 " + "thmB_one_level=1952/1824 thmB_own_bank=1344/1216/800/608 thmB_count_only=608/544/112/0 zero_advance_calls=6 " + "zero_advance_replicas=%d/16 hosted_route_instants=%dx16 breakeven_S=%d breakeven_C=%d no_saving=%d " + "echelon_dijkstra_instances=%d controls_rejected=%d" + % (total, len(window_ok), n_inst, dec["breakeven_idle"], dec["breakeven_rank8"], dec["threshold"], n, rejected)) + + +if __name__ == "__main__": + try: + main() + except Fail as exc: + print("FAIL:", exc) + sys.exit(1) diff --git a/research/retained-array-catch-up/verify.py b/research/retained-array-catch-up/verify.py new file mode 100644 index 0000000000..3e4d65696e --- /dev/null +++ b/research/retained-array-catch-up/verify.py @@ -0,0 +1,1167 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Primary verifier: retained-array coordinate catch-up in the scalar common-frame transport model. + +Checks (exact arithmetic; standard library only): + 1. Source pins and verbatim premise lines. + 2. Level timeline of the pinned selected #1094 hosted GLOBAL-TEMPLATE (replica 0). Every local + call advances its pair one level; idle sweeps advance their declared levels; one level is + eight coordinates (base-template idle child rank = 8 x levels; hosted children never exceed it). + Every bridge joins two pairs at equal levels. + 3. The catch-up law (PROOF.md Corollary 4) on controls: PR2540 128, PR2197 144, PR2678 + 1792/3696, centre path 576 per replica. + 4. The #1166 routes under the stated observation contract (P_obs) and capture times: + INIT64 + d_A = 3648 (end decoder, P_final) / 2496 (earliest timing the observed Y_(k,U) fields + allow under the final-value read convention, P_Y: X_(k,U) is last written at events 6/27/26/25) / + 1344 (each bank after its last local call, P_early; a lower bound for decoders with the + decoder-timing premise P_dec); + d_A alone 960; the all-initial variant of #2074 c18950926 3456 / 2304 / 1152; Theorem B per cut: + one consumer level (P_final) 1952 / 1824, own-bank premise 1344 / 1216 (P_Y) and 800 / 608 + (P_early), count-only deliveries 608 / 544 (P_Y) and 112 / 0 (P_early); (S)/(C) array-calls 464 + published / 456 uniform; the zero-advance window; the lagging-family example (the record + duplicates an observed row, so the law charges 0). Without P_dec: 512 (decoders right after + each bank's own last capture) and 640 (right after each backward call). Bank 0's INIT rows via + f0: 3520 / 2368 / 1216 (all-initial 3328 / 2176 / 1024). Revival terms: d_A 960 / 576 / 192 and + all-initial reads 768 / 384 / 0. Forward add-on f2..f8: 768-1024 / 384-640 / 0-256. Hosting (replica 0): every capture, + consumer and read instant sits at an exact level, checked in both directions. + 5. Pricing with the pinned ceiling.py: exact 896 no-saving threshold, break-evens 573 / 71 + against PR2474 (reproducing the #1166 price gate and its PRICE-GATE.json storage ceiling), + break-evens against other targets. + 6. Exact frame model: breadth-first minimum paid mass equals the per-cut rank bound (Lemma 1) + and the meeting-level formula (Proposition 3) on complete finite domains; Lemma 1 is sound + on general instances. + 7. Two-call rational tensor toy: omitting catch-up gives a wrong output; paid catch-up (or + partner descent) repairs it. + 8. Negative controls: mutated levels, rows, windows, incidences, lifetimes, read levels, + formulas, toy repairs and prices must fail. + +Run from the repository root: python3 -I -B research/retained-array-catch-up/verify.py +--write regenerates RESULT.json (refuses to replace a differing file unless --force is given). +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). +""" +import gzip +import hashlib +import io +import itertools +import json +import math +import random +import sys +import tarfile +from collections import deque +from fractions import Fraction as Q +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + +PINS = { + "research/complex-local-word-ceiling/ceiling.py": + "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc", + "research/complex-local-word-ceiling/README.md": + "b60be039cb0e03e064a27407d0bce9e58908d793da5ee405c876de5aebfa5f81", + "research/dirty-host-cutrank-audit/PROOF.md": + "2921c2c741ab5086a87c53340f18180ecc55675ca7dadc49579da32aba71d2f5", + "research/idle-axis-hosting/PROOF.md": + "cfe34bf0b64259661312dae22c3a23adc5bf6f6326951eee5c1488ccfc347542", + "research/qq16-complete-native-decoder/PROOF.md": + "09d587f1d6bc250e90e29fa8751a40f45be79f1a8a56af0b645c144cefaefa46", + "research/qq16-entry-frame-tariff/README.md": + "cb0e658cfbdd3fb74a43b195665d3b13d5eb8e74294831daa05165128ad9ef5d", + "research/qq16-private-da-frame-floor-seed81b017/README.md": + "8e4c3f1d2e76b110ef47aecdce8098c84403b969f8d6e386b0ecabb8173f091b", + "research/qq16-final-record-obstruction/PROOF.md": + "109490f1d9c4288445e11e65e77616d84555ce9f212df97c81e6efde0c2ebf43", + "research/selected-centre-quarter-native/README.md": + "bfae0aff6aefc90b2afb8da76bc6d07b698deeabdbd758d01910d9fdb937ec72", + "research/centre-owner-observation-floor/README.md": + "5f9079af7f45bff8d0b0acc8366f9c0def90fad9c8a38bab772b0ef13e3d5be0", + "research/selected-centre-chrono-source-census/README.md": + "0db44f2ce702ee1e5b11c9f8cd05517593bd259f45ae897437c58a1bd81b2943", + "research/joint-query/README.md": + "419f076e46f5a6ce43efe30a608baed0a535034c388e1ac76a29a2026685ba77", + "research/joint-query/evidence/CONSERVED-QQ16.md": + "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb", + "research/community-frontier1094-audit/selected-replay.tar.gz": + "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "certificates/selected-result.json": + "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "research/qq16-cut-retention-census/README.md": + "796636d4d9824bc4959b00d9d2cbbfafec07c14e6845a1e238fb668a2f3d8adf", +} +HOSTED_MEMBER = ("candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz", + "2acf02b418078e37090495c601fe550448751d4f35912757b13a1f778efc7760") +BASE_MEMBER = ("candidate/strict/global/base/split-centres/GLOBAL-TEMPLATE.json.gz", + "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518") + +ANCHORS = { + "research/dirty-host-cutrank-audit/PROOF.md": [ + "Its paid mass c is at least |nu(A)-nu(B)|.", + "D_j\\ \\ge\\ \\dim(W_j^0+\\operatorname{span}Q_j)-\\dim W_j^0. \\tag{C-down}", + "M\\ge\\sum_j(D_j+U_j). \\tag{A}", + "The retained history is a mathematical device, not free physical storage.", + "Any pre-existing side information belongs to the entry state.", + ], + "research/qq16-complete-native-decoder/PROOF.md": [ + "`F_L=product_(j=0,...,8) C_(d e_j)`", + "`U1=`", + "This costs sixteen rank-eight children and puts x1_V in frame F_U1.", + ], + "research/qq16-entry-frame-tariff/README.md": [ + "| Common `F_L`, `F_L` | 224 H8 | 1,792 |", + "| F0 gauges `F_L`, `F_L C_q^-1` | 112 H8 + 112 H9 | 1,904 |", + "| Original entry gauges `C_q`, `I` | 112 H16 + 112 H17 | 3,696 |", + ], + "research/qq16-private-da-frame-floor-seed81b017/README.md": [ + "each differs from I in exactly 18 one-term Z4 entries.", + "frames therefore needs at least 8 × 18 = 144 line calls.", + ], + "research/qq16-final-record-obstruction/PROOF.md": [ + " 0, 0, 0, 1, 1, 2, 2, 3, 3.", + "Even stages are forward F_s; odd stages are backward B_(s,s+1).", + "pair 0: B0 X_(0,U), B2 X_(0,U);", + "pair 1: B3 X_(1,U), B4 X_(1,U);", + " X_j,U += c X_i,U;", + " Y_i,U -= c Y_j,U.", + "base contract. The final ordinary terminal is `(X_U,Y_U) -> (Y_U,-X_U)`.", + "2. Every final completed-X ordinary field, namely final Y_(k,U).", + "former-Y ordinary endpoint, or additional ordinary read is observed.", + "former-Y ordinary endpoints, final X_(0,U)=z0 and final X_(1,U)=z1.", + ], + "research/joint-query/evidence/CONSERVED-QQ16.md": [ + " x'_U=x_U-y_U,", + " x'_U=x_U-K_(s,U)f,", + ], + "research/idle-axis-hosting/PROOF.md": [ + "1. ι is an invocation on another pair, and nothing touches F between ι and τ.", + ], + "research/complex-local-word-ceiling/README.md": [ + "`{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}`, local mass 5,586.", + ], + "research/joint-query/README.md": [ + "| B_s_t | 214986 | 24 | 5546 | 528 | 48 |", + "| F_s, s > 0 | 211210 | 8 | 5530 | 288 | 16 |", + ], + "research/selected-centre-chrono-source-census/README.md": [ + "2. **Every dependent pair has rank 16 (1,539 pairs).**", + "b5->f6, b7->f8 and f0->f2.", + "projection. It is not a native obstruction, not a formal proof and not a new kappa. The selected frontier", + " - *First step:* for the 16 f0->f2 pairs (shared 88 destination owners), compute the output-increment", + ], + "research/selected-centre-quarter-native/README.md": [ + "nevertheless `1/4` at the identity owner.", + ], + "research/centre-owner-observation-floor/README.md": [ + "**104 additional scalar coordinates at every old cover owner**, if each extra", + ], + "research/qq16-cut-retention-census/README.md": [ + "| C=0, centre-like copy | 111 | 71 | 120 / 1688: no saving at either (L2 variant: 32) |", + ], +} + +COORDS_PER_LEVEL = 8 +M, FAMILIES, STAGES = 73, 896, 9 +SELECTED_KAPPA = Q("0.001672660197076918") # #1094, selected-result.json +PR2474_KAPPA = Q("0.001703676387993676") # pending (PR2474) +PR2843_KAPPA = Q("0.00171865827784172") # pending (PR2843 title value) +PR2848_KAPPA = Q("0.00171865850830493") # pending (PR2848 title value) +PR2857_KAPPA = Q("0.00172009662868483") # pending (PR2857 title value; opened after the base) +BIT_ENDPOINT = Q("0.001733427039589844234749") # PR589 bit supplier saving +GRID = Q(1, 10 ** 12) +SELECTED = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} +# Philippe Van Velzen's price gate, read as data (never executed) from +# philippeVV/integer-mult-bounds@9fcd3d899cc5bad2e27ab1d3d64d241cbfe30793, +# research/joint-query-first-pair-catalogue/final-record/: +# price_gate.py docstring: "bank k first call stage: 0, 3, 5, 7. INIT records of bank k are read +# just before that call."; constants INIT_AC = 16 * (9 + 6 + 4 + 2) and DA_AC = 8 * (8 + 5 + 3); +# PRICE-GATE.json fields storage_readsFalse, breakeven_storage and breakeven_centre. +PRICE_GATE_INIT_LIFETIMES = (9, 6, 4, 2) +PRICE_GATE_DA_LIFETIMES = (8, 5, 3) +PRICE_GATE_STORAGE_READS_FALSE = Q(2285992139, 1002285992139) +PRICE_GATE_BREAKEVENS = (573, 71) + + +class CheckFailure(Exception): + pass + + +def need(ok, message): + if not ok: + raise CheckFailure(message) + + +# ------------------------------------------------------------------ 1. sources +def check_sources(): + for rel, pin in PINS.items(): + need(hashlib.sha256((ROOT / rel).read_bytes()).hexdigest() == pin, "source hash mismatch: " + rel) + for rel, lines in ANCHORS.items(): + text = (ROOT / rel).read_text(encoding="utf-8") + for line in lines: + need(line in text, "premise anchor missing in %s: %r" % (rel, line)) + return {"pinned_files": len(PINS), "anchored_premise_lines": sum(len(v) for v in ANCHORS.values())} + + +def load_templates(): + raw = (ROOT / "research/community-frontier1094-audit/selected-replay.tar.gz").read_bytes() + out = [] + with tarfile.open(fileobj=io.BytesIO(raw), mode="r:gz") as archive: + for name, pin in (HOSTED_MEMBER, BASE_MEMBER): + found = [m for m in archive.getmembers() if m.name == name] + need(len(found) == 1 and found[0].isfile(), "one regular member: " + name) + data = archive.extractfile(found[0]).read() + need(hashlib.sha256(data).hexdigest() == pin, "member hash: " + name) + out.append(json.loads(gzip.decompress(data))) + return out + + +# ------------------------------------------------------------------ 2. level timeline +def replica_events(hosted, base, replica=0): + events = [e for e in hosted["execution_schedule"] if e.get("replica") == replica] + need(len(events) == 30 and [e["source_event"] for e in events] == list(range(30)), "replica-0 events") + need(hosted["live"] == 14336 and hosted["m"] == 73, "selected live families / width") + need(all(b == 0 for b in hosted["hosting"]["banks"]), "selected template has no helper banks") + strip = ("replica", "replicas", "source_event", "time", "provider_id", "entry_exit_phase_adapters") + base_events = [{k: v for k, v in e.items() if k not in strip} for e in base["execution_schedule"][:30]] + host_events = [{k: v for k, v in e.items() if k not in strip} for e in events] + need(base_events == host_events, "hosted replica-0 schedule equals the base template schedule") + return events + + +def level_timeline(hosted, base, events, mutate=None): + """timeline[k] = (kind, source_event, levels of pairs 0..3 after it); timeline[0] = entry.""" + recipe = hosted["recipe"] + local_pairs = [e["pair"] for e in recipe if e["kind"] == "local"] + need(local_pairs == [0, 0, 0, 1, 1, 2, 2, 3, 3], "literal local pair binding (PR2346 recipe)") + need(all(e["reverse"] == (e["stage"] % 2 == 1) for e in recipe if e["kind"] == "local"), + "odd stages backward") + stage_pair = dict(enumerate(local_pairs)) + base_rank = {c["child"]: c["rank"] for c in base["idle_children"] if c["port"] == 0} + hosted_total = {} + for c in hosted["idle_children"]: + hosted_total.setdefault(c["child"], set()).add(c["hosted"] + c["rank"]) + level = [-1, -1, -1, -1] + timeline = [("entry", None, tuple(level))] + for e in events: + if e["kind"] == "local_cover_sweep": + p = stage_pair[e["stage"]] + need(level[p] == e["stage"] - 1, "local stage %d starts one level below" % e["stage"]) + level[p] = e["stage"] + elif e["kind"] == "idle_cover_sweep": + p, frm, to = e["pair"], e["from_level"], e["to_level"] + if mutate == "idle_to_level" and e["source_event"] == 5: + to += 1 + need(level[p] == frm and to >= frm, "idle sweep continues the pair's level") + if to > frm: + want = COORDS_PER_LEVEL * (to - frm) + need([base_rank[c] for c in e["child_indices"]] == [want, want], + "base idle children: eight coordinates per level (event %d)" % e["source_event"]) + for c in e["child_indices"]: + need(all(t <= want for t in hosted_total.get(c, {want})), + "hosted + remaining rank never exceeds the base child rank") + level[p] = to + elif e["kind"] == "bridge": + need(level[e["src"]] == level[e["dst"]], "bridge %d joins two pairs at equal levels" % e["source_event"]) + timeline.append((e["kind"], e["source_event"], tuple(level))) + need(level == [8, 8, 8, 8], "every pair ends at level 8 (nine levels = 72 paid coordinates)") + return timeline, stage_pair + + +def lv_before(timeline, event): + return timeline[event][2] + + +def lv_after(timeline, event): + return timeline[event + 1][2] + + +def catch_up(cap, cons, pair, rows): + gap = cons[pair] - cap[pair] + need(gap >= 0, "consumer frame at or above the capture frame") + return COORDS_PER_LEVEL * gap * rows + + +def routes(timeline, events, stage_pair, mutate=None): + end = timeline[-1][2] + locals_of = {k: [e["source_event"] for e in events if e["kind"] == "local_cover_sweep" + and stage_pair[e["stage"]] == k] for k in range(4)} + out = {} + rows = 15 if mutate == "pr2540_rows" else 16 + after_b1 = lv_after(timeline, 4 if mutate == "pr2540_incidence" else 1) + out["PR2540_early_records"] = {"rows": 16, "capture": "after F0 (event 0)", "consumer": "F_U1 after B1 (event 1)", + "capture_level": lv_after(timeline, 0)[0], "consumer_level": after_b1[0], + "mass": catch_up(lv_after(timeline, 0), after_b1, 0, rows)} + # Capture premise (PROOF.md section 7.2): X_(k,U) keeps its initial logical row until bank k's first + # local call. Local calls overwrite X_U (CONSERVED-QQ16 (1) and (3)) and no bridge writes X_(k,U) + # before that call, so the stated INIT capture just before it is the latest one without other reads. + for k in range(4): + need(not any(e["kind"] == "bridge" and e["dst"] == k for e in events[:locals_of[k][0]]), + "no bridge writes X_(%d,U) before bank %d's first call" % (k, k)) + init = [] + for k in range(4): + ev = locals_of[k][0] + lv = list(lv_before(timeline, ev)) + if mutate == "init_capture_level" and k == 1: + lv[1] = -1 + init.append({"bank": k, "capture_before_event": ev, "capture_level": lv[k], "rows": 16, + "consumer_level": end[k], "mass": catch_up(lv, end, k, 16)}) + da = [] + for k in range(3): + ev = [x for x in locals_of[k] if events[x]["stage"] % 2 == 1][0] + lv = lv_after(timeline, ev) + da.append({"bank": k, "capture_after_event": ev, "capture_level": lv[k], "rows": 8, + "consumer_level": end[k], "mass": catch_up(lv, end, k, 8)}) + out["INIT64"], out["d_A"] = init, da + out["INIT64_plus_dA_mass"] = sum(r["mass"] for r in init + da) + out["d_A_only_mass"] = sum(r["mass"] for r in da) + need(sum(r["rows"] for r in init + da) == 88, "88 stated arrays per owner per replica") + # P_Y: the contract observes final Y_(k,U) = -final X_(k,U) (terminal relabel). Local calls on pair k + # overwrite X_(k,U) and a bridge with dst = k adds into it, so no decoder of bank k can use its + # observed field before the last such write (final-value read convention of P_obs). Its level there + # lower-bounds every P_obs-admissible current-frame consumer of bank k that uses its own Y_(k,U) + # (other observations can only delay the decoder). + last_write = [max(e["source_event"] for e in events + if (e["kind"] == "local_cover_sweep" and stage_pair[e["stage"]] == k) + or (e["kind"] == "bridge" and e["dst"] == k)) for k in range(4)] + out["x_last_write_event"] = last_write + out["x_last_write_levels_all_pairs"] = [list(lv_before(timeline, ev)) for ev in last_write] + y_levels = [lv_after(timeline, last_write[k])[k] for k in range(4)] + out["y_consumer_levels"] = y_levels + out["INIT64_plus_dA_y_mass"] = sum(catch_up([r["capture_level"]] * 4, y_levels, r["bank"], r["rows"]) + for r in init + da) + # P_early: decode each bank at its own frame right after its last local call. Under P_obs with + # final-value reads this is not attainable for banks 1-2 (their observed fields are final only at + # level 8). Above the captures catch-up only grows with the consumer level, so it lower-bounds every + # current-frame timing at or after each bank's last local call (the decoder-timing premise P_dec); + # it does not bound earlier decoders (see without_decoder_timing_premise below). Favourable to the + # route: the corrected fields are assumed to ride the inherited idle sweep to level 8 at no extra mass. + early = [] + for r in init + da: + k = r["bank"] + last = lv_after(timeline, locals_of[k][-1]) + cap = [None] * 4 + cap[k] = r["capture_level"] + early.append(catch_up(cap, last, k, r["rows"])) + out["INIT64_plus_dA_early_consumer_mass"] = sum(early) + out["early_consumer_levels"] = [lv_after(timeline, locals_of[k][-1])[k] for k in range(4)] + out["early_consumer_after_events"] = [locals_of[k][-1] for k in range(4)] + # All-initial variant (#2074 c18950926 item 2): the d_A records are swapped for the reads + # B2 X_1U, B4 X_2U and B6 X_3U. X_(k+1,U) keeps its initial row until pair k+1's first local call, + # so the read may be taken at any level pair k+1 holds before that call. Pairs at equal levels + # share a frame (every bridge joins pairs at equal levels; checked in level_timeline). + reads = [] + for k in range(3): + src = k + 1 + first = locals_of[src][0] + need(not any(e["kind"] == "bridge" and e["dst"] == src for e in events[:first]), + "no bridge writes X_(%d,U) before its first call" % src) + held = sorted({timeline[i][2][src] for i in range(first + 1)}) # entry .. just before the first call + if mutate == "allinit_read_level" and k == 0: + held = [h for h in held if h != out["early_consumer_levels"][0]] + latest = lv_before(timeline, first)[src] + cons = out["early_consumer_levels"][k] + best = min(held, key=lambda h: abs(cons - h)) + reached = [e["source_event"] for e in events[:first] + if e["kind"] == "idle_cover_sweep" and e["pair"] == src and e["to_level"] == best] + reads.append({"bank": k, "read": "B%d X_(%d,U)" % (2 * k + 2, src), "rows": 8, + "levels_held_while_initial": held, "latest_read_level": latest, + "final_mass": COORDS_PER_LEVEL * 8 * (end[k] - latest), + "early_consumer_level": cons, "early_read_level": best, + "early_read_after_event": reached[0] if reached else None, + "early_mass": COORDS_PER_LEVEL * 8 * abs(cons - best), + "y_mass": COORDS_PER_LEVEL * 8 * min(abs(y_levels[k] - h) for h in held)}) + init_early = early[:4] + out["all_initial_variant"] = { + "source": "#2074 c18950926 item 2: the d_A records swapped for the reads B2 X_1U, B4 X_2U and B6 X_3U", + "reads": reads, + "final_mass": sum(r["mass"] for r in init) + sum(x["final_mass"] for x in reads), + "y_mass": sum(catch_up([r["capture_level"]] * 4, y_levels, r["bank"], 16) for r in init) + + sum(x["y_mass"] for x in reads), + "early_mass": sum(init_early) + sum(x["early_mass"] for x in reads)} + # Theorem B (#2074 c18940190): any repair needs >= 62 independent rows per owner per replica. Restricted + # to the stated captures (each array supplies at most one row per owner; P_obs; P4), see PROOF.md 7.2. + original = [(r["bank"], r["rows"], [r["capture_level"]]) for r in init + da] + variant = [(r["bank"], 16, [r["capture_level"]]) for r in init] + \ + [(x["bank"], 8, x["levels_held_while_initial"]) for x in reads] + timings = {"P_final": list(end), "P_Y": y_levels, "P_early": out["early_consumer_levels"]} + out["theorem_B"] = {name: {"original": theorem_b(original, cons), "all_initial": theorem_b(variant, cons)} + for name, cons in timings.items()} + # Forward histories f2, f4, f6, f8 (the tail identity C_k = w_k + K_(2k+2) f_(2k+2) of #2074 c18950926 uses + # f_(2k+2) for every bank, f8 for bank 3; not in the 464 array-calls). If each is retained as one 8-row array + # captured at its forward call's output or input level, the law adds the following; the totals only grow. + fwd = {"P_final": [], "P_Y": [], "P_early": []} + for k in range(4): + ev = [x for x in locals_of[k] if events[x]["stage"] == 2 * k + 2][0] + lo, hi = lv_before(timeline, ev)[k], lv_after(timeline, ev)[k] + for name, cons in (("P_final", end), ("P_Y", y_levels), ("P_early", out["early_consumer_levels"])): + fwd[name].append((cons[k] - hi, cons[k] - lo)) + out["forward_histories_addon"] = { + "histories": "f2, f4, f6, f8: one 8-row array each, captured at the forward call's output (low end) or input level", + **{name.replace("P_final", "final").replace("P_Y", "y").replace("P_early", "early") + "_mass_range": + [COORDS_PER_LEVEL * 8 * sum(a for a, _ in v), COORDS_PER_LEVEL * 8 * sum(b for _, b in v)] + for name, v in fwd.items()}, + "f2_f4_f6_only": {name: [COORDS_PER_LEVEL * 8 * sum(a for a, _ in v[:3]), COORDS_PER_LEVEL * 8 * sum(b for _, b in v[:3])] + for name, v in fwd.items()}} + # One P_rank law for any consumer vector (uncompressed delivery of every stated array to its own bank's + # consumer; reads at their best held level, either direction). It must reproduce the totals above. + def law_mass(cons, variant, init_levels=None): + caps = init_levels or [r["capture_level"] for r in init] + total = sum(catch_up([caps[k]] * 4, cons, k, 16) for k in range(4)) + if variant == "original": + return total + sum(catch_up([r["capture_level"]] * 4, cons, r["bank"], 8) for r in da) + return total + sum(COORDS_PER_LEVEL * 8 * min(abs(cons[x["bank"]] - h) for h in x["levels_held_while_initial"]) + for x in reads) + for name, cons in (timings.items() if mutate is None else ()): # mutations are judged by their own checks + need(law_mass(cons, "original") == {"P_final": out["INIT64_plus_dA_mass"], "P_Y": out["INIT64_plus_dA_y_mass"], + "P_early": out["INIT64_plus_dA_early_consumer_mass"]}[name] + and law_mass(cons, "all_initial") == {"P_final": out["all_initial_variant"]["final_mass"], + "P_Y": out["all_initial_variant"]["y_mass"], + "P_early": out["all_initial_variant"]["early_mass"]}[name], + "one law_mass reproduces both variants at " + name) + # Decoder-timing premise (P_dec) is load-bearing: decoders placed right after each bank's own last stated + # capture, or right after each backward call, are current-frame consumers that P_obs alone does not exclude. + own_last = [max([r["capture_level"] for r in init + da if r["bank"] == k]) for k in range(4)] + after_back = [lv_after(timeline, [x for x in locals_of[k] if events[x]["stage"] % 2 == 1][0])[k] for k in range(4)] + out["without_decoder_timing_premise"] = { + "after_own_last_capture": {"consumer_levels": own_last, "original": law_mass(own_last, "original"), + "all_initial": law_mass(own_last, "all_initial")}, + "after_backward_call": {"consumer_levels": after_back, "original": law_mass(after_back, "original"), + "all_initial": law_mass(after_back, "all_initial")}} + # Bank 0's INIT rows via f0 (CONSERVED-QQ16 (3): z = w + K_(s,U) f, and f0 is an observation under P_obs): + # B_t X_(0,U)(initial) = B_t X'_(0,U) + B_t K_(0,U) f0 can be formed at F0's output frame. Banks 1-3 start + # with a backward call, whose inverse needs the transient y_U, so their stated captures stay the latest. + f0_init = [lv_after(timeline, locals_of[0][0])[0]] + [r["capture_level"] for r in init[1:]] + need(events[locals_of[0][0]]["stage"] == 0 and all(events[locals_of[k][0]]["stage"] % 2 == 1 for k in (1, 2, 3)), + "bank 0 starts with forward F0; banks 1-3 start with a backward call") + original_f0 = [(0, 16, [f0_init[0]])] + original[1:] + variant_f0 = [(0, 16, [f0_init[0]])] + variant[1:] + out["init0_via_f0"] = { + "init_capture_levels": f0_init, + "original": {name: law_mass(cons, "original", f0_init) for name, cons in timings.items()}, + "all_initial": {name: law_mass(cons, "all_initial", f0_init) for name, cons in timings.items()}, + "thmB_own_bank": {name: {"original": theorem_b(original_f0, cons)["own_bank"], + "all_initial": theorem_b(variant_f0, cons)["own_bank"]} for name, cons in timings.items()}, + "thmB_one_level_end": {"original": theorem_b(original_f0, end)["one_level_cut_sum"], + "all_initial": theorem_b(variant_f0, end)["one_level_cut_sum"]}} + # Revival terms: what remains if the INIT information were free. + out["revival_terms"] = { + "dA_term": {name: sum(catch_up([r["capture_level"]] * 4, cons, r["bank"], 8) for r in da) + for name, cons in timings.items()}, + "all_initial_reads_term": {name: sum(COORDS_PER_LEVEL * 8 * min(abs(cons[x["bank"]] - h) + for h in x["levels_held_while_initial"]) + for x in reads) for name, cons in timings.items()}} + touch = min(e["source_event"] for e in events + if (e["kind"] == "local_cover_sweep" and stage_pair[e["stage"]] == 3) + or (e["kind"] == "idle_cover_sweep" and e["pair"] == 3 and e["to_level"] > e["from_level"]) + or (e["kind"] == "bridge" and 3 in (e["src"], e["dst"]))) + if mutate == "witness_window": + touch += 1 + calls = [e["stage"] for e in events if e["kind"] == "local_cover_sweep" and e["source_event"] < touch] + out["zero_witness"] = {"pair": 3, "side": "Y (replica-0 families 784..895)", "capture": "entry", + "consumer_before_event": touch, "consumer_before_time": events[touch]["time"], + "calls_in_window": calls, + "levels_advanced": lv_before(timeline, touch)[3] - timeline[0][2][3], + "record_copies_an_untouched_stream": True, + "law_mass_per_array": catch_up(timeline[0][2], lv_before(timeline, touch), 3, 1), + "S_per_array": len(calls), "C_mass_per_array": 8 * len(calls)} + # Lagging-pair records do not separate the law from (C): a pair-0 X_(0,U) record captured after event 13 + # and consumed at the end advances six levels in three calls, but X_(0,U) is last written at event 6; afterwards only + # idle sweep 21 (a transport: the logical row is kept), bridge 27 with src = 0 (reads X_(0,U)) and + # the terminals act on it. The record duplicates -final Y_(0,U), which the contract observes, so + # rho_r = 0 and the law charges 0, not 48. + x0_writes = [e["source_event"] for e in events + if (e["kind"] == "local_cover_sweep" and stage_pair[e["stage"]] == 0) + or (e["kind"] == "bridge" and e["dst"] == 0)] + after = [e["kind"] + ("" if e["kind"] != "bridge" else " src=%d dst=%d" % (e["src"], e["dst"])) + for e in events[14:] + if (e["kind"] == "idle_cover_sweep" and e["pair"] == 0) + or (e["kind"] == "bridge" and 0 in (e["src"], e["dst"])) or e["kind"].startswith("terminal")] + out["lagging_record_example"] = { + "record": "X_(0,U) captured after event 13, consumed at the end", + "capture_level": lv_after(timeline, 13)[0], "levels_advanced": end[0] - lv_after(timeline, 13)[0], + "calls_after_capture": sum(1 for e in events[14:] if e["kind"] == "local_cover_sweep"), + "last_write_event_of_X0": max(x0_writes), "pair0_events_after_capture": after, + "law_mass_if_independent_row": catch_up(lv_after(timeline, 13), end, 0, 1), + "law_mass": 0, "C_mass": 8 * 3} + return out + + +def theorem_b(captures, consumers, mutate=None, need_rows=62): + """Theorem-B delivery floors (coordinates per owner per replica) for one consumer timing. + + captures: (bank, rows, admissible capture levels); consumers: consumer level of each bank. + - one_level_cut_sum: Lemma 1 summed over the cuts, sum_j max(0, 62 - n+_j), with n+_j the stated rows + captured at or above cut j (each capture at its most favourable admissible level). Valid only when every + bank decodes at one level; None otherwise. + - own_bank: each capture serves only the bank whose derived decoder uses it and the 62 rows split freely + over the banks: the cheapest 62 own-bank climbs (equal to the minimum over splits, as each bank's + cost is a sum of its cheapest rows). + - count_only: no assignment premise; each row may go to any consumer in either direction (P_glob): the + cheapest delivery of 62 rows that would meet Theorem B's count if the captures are independent. An + argument using only the count and the capture heights cannot force more than this at that timing. + """ + own, free = [], [] + for bank, rows, levels in captures: + climbs = [consumers[bank] - h for h in levels if h <= consumers[bank]] + need(climbs, "every stated capture has an admissible level at or below its own bank's consumer") + own += [COORDS_PER_LEVEL * min(climbs)] * rows + free += [COORDS_PER_LEVEL * min(abs(c - h) for c in consumers for h in levels)] * rows + if mutate == "thmB_free_assignment": + own = free + own.sort() + free.sort() + need(len(own) == 88, "88 stated arrays per owner per replica") + out = {"own_bank": sum(own[:need_rows]), "count_only": sum(free[:need_rows]), "one_level_cut_sum": None} + if len(set(consumers)) == 1: + top = COORDS_PER_LEVEL * (consumers[0] + 1) + heights = [(rows, COORDS_PER_LEVEL * (max(h for h in levels if h <= consumers[0]) + 1)) + for _, rows, levels in captures] + out["one_level_cut_sum"] = sum(max(0, need_rows - sum(n for n, h in heights if h >= j)) + for j in range(1, top + 1)) + return out + + +def hosting_checks(hosted, r, mutate=None): + """Hosted helper residuals also change idle frames (idle-axis hosting moves factors to their + invocation time), so part of a later level can land on an idle family early. Every instant the + routes use must sit at an exact level, checked in both directions (replica 0): + - no overshoot: each residual hosted on the pair by then belongs to a sweep that has already + reached that level; + - no undershoot: each residual of a sweep that has already reached that level has landed. + The witness streams host nothing in their window. independent_check.py replays per-family heights + (both tie conventions, all 16 replicas) as a second method.""" + slots = [dict(x) for x in hosted["hosting"]["pooled_slots"] if x["owner_replica"] == 0] + sweep_to = {} + for e in hosted["execution_schedule"]: + if e.get("replica") == 0 and e["kind"] == "idle_cover_sweep": + for c in e["child_indices"]: + sweep_to[c] = (e["pair"], e["from_level"], e["to_level"], e["source_event"]) + if mutate == "undershoot": # delay one pair-1 residual of sweep 2 (levels -1 -> 1) to time 25 + x = next(x for x in slots if 224 <= x["family"] < 448 and sweep_to[x["child"]][3] == 2) + x["time"] = 25 + idle = {(c["family"], c["child"]): c for c in hosted["idle_children"] if c["replica"] == 0} + zw = r["zero_witness"] + limit = zw["consumer_before_time"] + (17 if mutate == "hosting_window" else 0) + y3 = range(784, 896) + early_y3 = [x for x in slots if x["family"] in y3 and x["time"] < limit] + need(not early_y3, "no hosted residual on pair-3 Y families before the witness consumer") + need(all(idle[(f, 10)]["hosted"] == 0 and idle[(f, 10)]["rank"] == 48 for f in y3), + "pair-3 Y sweep -1 -> 5 is an unhosted rank-48 idle child") + early_x3 = [x for x in slots if 672 <= x["family"] <= 783 and x["time"] < limit] + times = {e["source_event"]: e["time"] for e in hosted["execution_schedule"] if e.get("replica") == 0} + instants = [("INIT capture", x["bank"], times[x["capture_before_event"]], x["capture_level"]) for x in r["INIT64"]] + instants += [("d_A capture", x["bank"], times[x["capture_after_event"]], x["capture_level"]) for x in r["d_A"]] + instants += [("P_early consumer", k, times[ev], lv) + for k, (ev, lv) in enumerate(zip(r["early_consumer_after_events"], r["early_consumer_levels"]))] + for x in r["all_initial_variant"]["reads"]: + t = times[x["early_read_after_event"]] + instants.append(("all-initial read", x["bank"] + 1, t, x["early_read_level"])) + instants.append(("all-initial consumer", x["bank"], t, x["early_consumer_level"])) + instants += [("P_Y consumer", k, times[ev], lv) + for k, (ev, lv) in enumerate(zip(r["x_last_write_event"], r["y_consumer_levels"]))] + over = under = 0 + distinct = set() + for label, pair, t, level in instants: + for i, x in enumerate(slots): + if not 224 * pair <= x["family"] < 224 * (pair + 1): + continue + sp, frm, to, _ = sweep_to[x["child"]] + if x["time"] <= t: + need(sp == pair and to <= level, "hosted residual before a %s belongs to an already-reached level" % label) + over += 1 + distinct.add(i) + elif sp == pair and frm < to <= level: + raise CheckFailure("hosted residual of an already-reached level lands after a %s (undershoot)" % label) + else: + under += 1 + return {"pair3_Y_hosted_slots_in_window": 0, "pair3_X_hosted_slots_in_window": len(early_x3), + "instants_checked": len(instants), "slot_instant_checks": over, "undershoot_slot_checks": under, + "distinct_slots_checked": len(distinct), + "route_capture_slot_checks": sum(1 for label, pair, t, level in instants[:7] for x in slots + if 224 * pair <= x["family"] < 224 * (pair + 1) and x["time"] <= t)} + + +def array_calls(dA_lifetimes=(8, 5, 3)): + return 16 * (9 + 6 + 4 + 2) + 8 * sum(dA_lifetimes) + + +# ------------------------------------------------------------------ 5. pricing +def load_ceiling(): + sys.path.insert(0, str(ROOT / "research/complex-local-word-ceiling")) + try: + import ceiling + finally: + sys.path.pop(0) + need(hashlib.sha256(Path(ceiling.__file__).read_bytes()).hexdigest() == + PINS["research/complex-local-word-ceiling/ceiling.py"], "imported ceiling.py is the pinned file") + return ceiling + + +def qq16_profile(): + core = {r: n for r, n in SELECTED.items() if r != 8} + need(sum(r * n for r, n in core.items()) == 5522, "retained QQ16 core mass 5522") + back = dict(core) + back[1] += 24 + fwd = dict(core) + fwd[1] += 8 + need(sum(r * n for r, n in back.items()) == 5546 and sum(r * n for r, n in fwd.items()) == 5530, + "QQ16 native masses 5546 (B) / 5530 (F)") + return {r: Q(5 * fwd[r] + 4 * back[r], 9) for r in core} + + +def priced(units, pricing): + local = dict(qq16_profile()) + n = Q(units, STAGES) + if pricing == "rank8": + local[8] = local.get(8, 0) + n / 8 + elif pricing != "idle": + raise ValueError(pricing) + return local, n + + +def kappa_cap(C, units, pricing): + local, centre = priced(units, pricing) + try: + a = C.ceiling(local, M, FAMILIES, STAGES, centre, grid=GRID)[1] + except ValueError: + return None + return a / (1 + a) + + +def beats(C, units, pricing, kappa): + """Certified: does the stated relaxation exceed `kappa` (relax(a_t) < 1 at a_t = kappa/(1-kappa))?""" + local, centre = priced(units, pricing) + try: + lo, hi = C.relax(local, M, FAMILIES, STAGES, centre, kappa / (1 - kappa)) + except ValueError: + return False # local word pays more than the coverage law allows + need(hi < 1 or lo > 1, "enclosure separates the comparison point") + return hi < 1 + + +def breakeven(C, pricing, kappa, step): + lo, hi = 0, 1 << 13 + need(beats(C, 0, pricing, kappa) and not beats(C, hi * step, pricing, kappa), "bracket") + while hi - lo > 1: + mid = (lo + hi) // 2 + if beats(C, mid * step, pricing, kappa): + lo = mid + else: + hi = mid + return lo + + +def pricing_checks(C, route_mass): + out = {} + free = kappa_cap(C, 0, "idle") + need(abs(free - Q("0.0047020509675915")) < Q(1, 10 ** 13), "free-controller cap 0.0047020509675915") + out["free_controller_C0_kappa_cap"] = "%.16f" % free + need(kappa_cap(C, 895, "idle") is not None and kappa_cap(C, 896, "idle") is None, "896 threshold (idle)") + # PR2470 (qq16-cut-retention-census) screened retained copies under the assumed centre-like convention: at C = 0 + # the last coordinate-call count with any positive saving is 111. Corollary 4 derives that convention for + # current-frame consumers; 8 x 111 = 888 < 896 <= 8 x 112 is the same exact threshold. + need(kappa_cap(C, 8 * 111, "rank8") is not None and kappa_cap(C, 8 * 112, "rank8") is None, + "896 threshold (rank-8) = PR2470's C = 0 centre-like limit of 111 coordinate-calls") + out["no_saving_threshold_units_per_replica"] = 896 + centre = kappa_cap(C, 576, "rank8") + local, _ = priced(576, "rank8") + need(local[8] == 8 and centre == (lambda a: a / (1 + a))( + C.ceiling({**qq16_profile(), 8: Q(8)}, M, FAMILIES, STAGES, 64, grid=GRID)[1]), + "576 rank-8 units per replica = eight rank-8 centre copies per call with C = 64") + out["centre_path_576_kappa_cap"] = "%.16f" % centre + be_s = breakeven(C, "idle", PR2474_KAPPA, 1) + be_c = breakeven(C, "rank8", PR2474_KAPPA, 8) + need((be_s, be_c) == PRICE_GATE_BREAKEVENS, "#1166 price-gate break-evens 573 (S) / 71 (C) reproduced") + need(kappa_cap(C, sum(16 * x for x in PRICE_GATE_INIT_LIFETIMES) + sum(8 * x for x in PRICE_GATE_DA_LIFETIMES), + "idle") == PRICE_GATE_STORAGE_READS_FALSE, + "S-priced 464 array-calls equals PRICE-GATE.json storage_readsFalse exactly") + need(kappa_cap(C, 573, "idle") > PR2474_KAPPA >= kappa_cap(C, 574, "idle"), "ceiling agrees at 573/574") + need(kappa_cap(C, 568, "rank8") > PR2474_KAPPA >= kappa_cap(C, 576, "rank8"), "ceiling agrees at 71/72") + out["breakeven_vs_PR2474"] = {"S_array_calls": be_s, "C_array_calls": be_c} + table = {} + for name, kappa in (("selected_1094", SELECTED_KAPPA), ("PR2474", PR2474_KAPPA), ("PR2843", PR2843_KAPPA), + ("PR2848", PR2848_KAPPA), ("PR2857", PR2857_KAPPA), ("bit_endpoint_PR589", BIT_ENDPOINT)): + table[name] = {"kappa": str(kappa), "idle_units": breakeven(C, "idle", kappa, 1), + "rank8_units": 8 * breakeven(C, "rank8", kappa, 8)} + rows = sorted(table.values(), key=lambda v: Q(v["kappa"])) + need(all(a["idle_units"] >= b["idle_units"] and a["rank8_units"] >= b["rank8_units"] for a, b in zip(rows, rows[1:])), + "break-even mass is non-increasing in the comparison kappa") + out["mass_breakeven_units_per_replica"] = table + out["routes"] = {} + for name, mass in route_mass.items(): + k_idle, k_r8 = kappa_cap(C, mass, "idle"), kappa_cap(C, mass, "rank8") + out["routes"][name] = {"units_per_replica": mass, + "idle_priced_kappa_cap": None if k_idle is None else "%.16f" % k_idle, + "rank8_priced_kappa_cap": None if k_r8 is None else "%.16f" % k_r8} + return out + + +# ------------------------------------------------------------------ 6. exact frame model +class Lattice: + """Subspaces of GF(p)^n, indexed; join with one vector; membership.""" + + def __init__(self, p, n): + self.p, self.n = p, n + self.vecs = list(itertools.product(range(p), repeat=n)) + self.zero = tuple([0] * n) + self.subs, self.index = [], {} + self._add(frozenset([self.zero])) + frontier = [0] + while frontier: + nxt = [] + for s in frontier: + for v in self.vecs: + t = self.close(self.subs[s] | {v}) + if t not in self.index: + nxt.append(self._add(t)) + frontier = nxt + self.join = [[self.index[self.close(s | {v})] for v in self.vecs] for s in self.subs] + self.vid = {v: i for i, v in enumerate(self.vecs)} + self.dim = [round(math.log(len(s), p)) for s in self.subs] + + def _add(self, s): + self.index[s] = len(self.subs) + self.subs.append(s) + return self.index[s] + + def close(self, vectors): + space = {self.zero} + changed = True + vectors = set(vectors) + while changed: + changed = False + for a in list(space): + for b in vectors: + for c in range(1, self.p): + w = tuple((x + c * y) % self.p for x, y in zip(a, b)) + if w not in space: + space.add(w) + changed = True + return frozenset(space) + + def span(self, vectors): + return self.index[self.close(set(vectors))] + + +def bfs_all(L, start, H): + dist = {start: 0} + queue = deque([start]) + while queue: + state = queue.popleft() + d = dist[state] + for h in range(H + 1): + for v in L.subs[state[h]]: + if v == L.zero: + continue + vi = L.vid[v] + for g in (h - 1, h + 1): + if 0 <= g <= H and v not in L.subs[state[g]]: + nxt = list(state) + nxt[g] = L.join[state[g]][vi] + nxt = tuple(nxt) + if nxt not in dist: + dist[nxt] = d + 1 + queue.append(nxt) + return dist + + +def min_mass(L, dist, demand): + best = None + for state, d in dist.items(): + if all(v in L.subs[state[h]] for v, h in demand) and (best is None or d < best): + best = d + need(best is not None, "demand unreachable") + return best + + +def cut_bound(L, entry, demand, H, directions=("up", "down")): + total = 0 + for j in range(1, H + 1): + for side, keep in (("up", lambda h: h >= j), ("down", lambda h: h < j)): + if side not in directions: + continue + e = [v for v, h in entry if keep(h)] + d = [v for v, h in demand if keep(h)] + total += L.dim[L.span(e + d)] - L.dim[L.span(e)] + return total + + +def meeting_formula(L, R, P, O, hr, hp, hc): + rho_r = L.dim[L.span(P + O)] - L.dim[L.span(P)] + rho_p = L.dim[L.span(R + O)] - L.dim[L.span(R)] + rho_o = L.dim[L.span(O)] + return min(rho_r * abs(x - hr) + rho_p * abs(x - hp) + rho_o * abs(x - hc) + for x in range(min(hr, hp, hc), max(hr, hp, hc) + 1)) + + +def basis(L, s): + out = [] + for v in sorted(L.subs[s]): + if v != L.zero and v not in L.subs[L.span(out)]: + out.append(v) + return out + + +def frame_model_checks(): + stats = {"domains": [], "record_partner_instances": 0, "general_instances": 0, + "general_tight": 0, "upward_only_failures": 0} + for p, n, H in ((2, 2, 3), (3, 2, 2), (2, 3, 2)): + L = Lattice(p, n) + pairs = [(a, b) for a, b in itertools.product(range(len(L.subs)), repeat=2) + if len(L.subs[a] & L.subs[b]) == 1] + stats["domains"].append({"field": "GF(%d)" % p, "dim": n, "levels": H + 1, "subspaces": len(L.subs), + "independent_RP_pairs": len(pairs), "coverage": "complete"}) + before = stats["record_partner_instances"] + for R_s, P_s in pairs: + R, P = basis(L, R_s), basis(L, P_s) + RP = L.subs[L.span(R + P)] + outs = [o for o in range(len(L.subs)) if L.subs[o] <= RP and L.dim[o] > 0] + for hr, hp in itertools.product(range(H + 1), repeat=2): + st = [L.span([])] * (H + 1) + st[hr] = L.span(R + (P if hp == hr else [])) + if hp != hr: + st[hp] = L.span(P) + dist = bfs_all(L, tuple(st), H) + entry = [(v, hr) for v in R] + [(v, hp) for v in P] + for o in outs: + O = basis(L, o) + for hc in range(H + 1): + demand = [(v, hc) for v in O] + [(v, hp) for v in P] + opt = min_mass(L, dist, demand) + lb = cut_bound(L, entry, demand, H) + mf = meeting_formula(L, R, P, O, hr, hp, hc) + need(lb <= opt, "Lemma 1 soundness") + need(opt == lb == mf, "Proposition 3 exactness %s" % ((p, n, H, hr, hp, hc),)) + if cut_bound(L, entry, demand, H, ("up",)) != opt: + stats["upward_only_failures"] += 1 + stats["record_partner_instances"] += 1 + stats["domains"][-1]["record_partner_instances"] = stats["record_partner_instances"] - before + if (p, n, H) == (2, 2, 3): + placed = [(v, h) for v in L.vecs if v != L.zero for h in range(H + 1)] + sets = list(itertools.chain(itertools.combinations(placed, 1), itertools.combinations(placed, 2))) + for e_rows in sets: + st = [L.span([])] * (H + 1) + for v, h in e_rows: + st[h] = L.join[st[h]][L.vid[v]] + dist = bfs_all(L, tuple(st), H) + avail = L.subs[L.span([v for v, _ in e_rows])] + for d_rows in sets: + if all(v in avail for v, _ in d_rows): + opt = min_mass(L, dist, list(d_rows)) + lb = cut_bound(L, list(e_rows), list(d_rows), H) + need(lb <= opt, "Lemma 1 soundness (general)") + stats["general_instances"] += 1 + stats["general_tight"] += int(lb == opt) + need(stats["upward_only_failures"] > 0, "negative control: an upward-only bound must fail somewhere") + return stats + + +# ------------------------------------------------------------------ 7. tensor toy +HAD = ((1, 1), (1, -1)) + + +def apply_axis(x, axis, inverse=False): + y = [Q(0)] * 4 + for i in range(4): + bits = [i & 1, (i >> 1) & 1] + for b in (0, 1): + jb = list(bits) + jb[axis] = b + y[i] += Q(HAD[bits[axis]][b]) * (Q(1, 2) if inverse else 1) * x[jb[0] + 2 * jb[1]] + return y + + +def in_frame(x, axes): + for a in axes: + x = apply_axis(x, a) + return x + + +def add(*xs): + return [sum(t) for t in zip(*xs)] + + +def tensor_toy(): + rng = random.Random(20261016) + naive_wrong = wrong_axis = 0 + trials = 25 + for _ in range(trials): + x = [Q(rng.randint(-9, 9), rng.randint(1, 5)) for _ in range(4)] + dx = [Q(rng.randint(-9, 9), rng.randint(1, 5)) for _ in range(4)] + record = in_frame(x, [0]) # captured after call 1 (axis 0 advanced) + current = in_frame(add(x, dx), [0, 1]) # after call 2 (axis 1 advanced) + want = in_frame(add(x, x, dx), [0, 1]) # consumer: x + (x + dx) in the current frame + naive_wrong += add(record, current) != want + need(add(apply_axis(record, 1), current) == want, "paid axis-1 catch-up repairs the output") + wrong_axis += add(apply_axis(record, 0), current) != want + down = apply_axis(current, 1, inverse=True) # partner descends to the record's frame + need(apply_axis(add(record, down), 1) == want, "partner descent + output climb also repairs it") + need(add(record, in_frame(x, [0])) == in_frame(add(x, x), [0]), "same-frame consumer needs no catch-up") + need(naive_wrong == trials, "negative control: omitting catch-up must give a wrong output") + need(wrong_axis == trials, "negative control: catch-up on the wrong axis must fail") + return {"trials": trials, "naive_wrong": naive_wrong, "wrong_axis_wrong": wrong_axis, "repaired_correct": trials} + + +# ------------------------------------------------------------------ 8. negative controls +def expect_failure(label, fn, reason): + """A negative control must fail, and for its stated reason (the message must contain `reason`).""" + try: + fn() + except CheckFailure as exc: + need(reason in str(exc), "negative control %r failed for another reason: %s" % (label, exc)) + return label + raise CheckFailure("negative control unexpectedly passed: " + label) + + +def equal(name, got, want): + need(got == want, "%s = %r (expected %r)" % (name, got, want)) + + +def negative_controls(hosted, base, events, C): + tl, sp = level_timeline(hosted, base, events) + + def mutated(kind): + return routes(tl, events, sp, mutate=kind) + + r = routes(tl, events, sp) + original = [(x["bank"], x["rows"], [x["capture_level"]]) for x in r["INIT64"] + r["d_A"]] + reversed27 = [dict(e, src=1, dst=0) if e["source_event"] == 27 else e for e in events] + out = [ + expect_failure("idle sweep to_level +1", lambda: level_timeline(hosted, base, events, "idle_to_level"), + "base idle children: eight coordinates per level (event 5)"), + expect_failure("PR2540 rows 16 -> 15", + lambda: equal("PR2540 mass", mutated("pr2540_rows")["PR2540_early_records"]["mass"], 128), + "PR2540 mass = 120"), + expect_failure("PR2540 two incidences", + lambda: equal("PR2540 mass", mutated("pr2540_incidence")["PR2540_early_records"]["mass"], 128), + "PR2540 mass = 256"), + expect_failure("INIT bank-1 capture level -1", + lambda: equal("INIT64 + d_A mass", mutated("init_capture_level")["INIT64_plus_dA_mass"], 3648), + "INIT64 + d_A mass = 4032"), + expect_failure("zero witness extended past first pair-3 touch", + lambda: equal("zero-advance law mass per array", + mutated("witness_window")["zero_witness"]["law_mass_per_array"], 0), + "zero-advance law mass per array = 48"), + expect_failure("uniform lifetimes give 464 array-calls", lambda: equal("array-calls", array_calls((7, 5, 3)), 464), + "array-calls = 456"), + expect_failure("witness window stretched into pair-3 Y hosting (time + 17)", + lambda: hosting_checks(hosted, r, mutate="hosting_window"), + "no hosted residual on pair-3 Y families before the witness consumer"), + expect_failure("hosted residual of sweep 2 delayed to time 25 (undershoot)", + lambda: hosting_checks(hosted, r, mutate="undershoot"), + "(undershoot)"), + expect_failure("895 units/replica has no saving", + lambda: equal("no saving at 895 units", kappa_cap(C, 895, "idle") is None, True), + "no saving at 895 units = False"), + expect_failure("break-even 574 (S) against PR2474", + lambda: equal("beats PR2474 at 574 idle units", beats(C, 574, "idle", PR2474_KAPPA), True), + "beats PR2474 at 574 idle units = False"), + expect_failure("all-initial read of X_(1,U) barred from bank 0's consumer level", + lambda: equal("all-initial early mass", + mutated("allinit_read_level")["all_initial_variant"]["early_mass"], 1152), + "all-initial early mass = 1216"), + expect_failure("bridge 27 reversed (dst = 0): X_(0,U) written after the capture", + lambda: equal("last write of X_(0,U)", + routes(tl, reversed27, sp)["lagging_record_example"]["last_write_event_of_X0"], 6), + "last write of X_(0,U) = 27"), + expect_failure("Theorem B at P_early without the own-bank premise", + lambda: equal("Theorem B P_early floor", + theorem_b(original, r["early_consumer_levels"], "thmB_free_assignment")["own_bank"], 800), + "Theorem B P_early floor = 112"), + expect_failure("P_early as a floor for decoders without the decoder-timing premise", + lambda: need(r["without_decoder_timing_premise"]["after_own_last_capture"]["original"] + >= r["INIT64_plus_dA_early_consumer_mass"], + "P_early bounds decoders right after each bank's own last capture"), + "P_early bounds decoders right after each bank's own last capture"), + ] + return out + + +# ------------------------------------------------------------------ main +def main(argv): + result = {"schema": "retained-array-catch-up/1", "sources": check_sources()} + hosted, base = load_templates() + events = replica_events(hosted, base) + timeline, stage_pair = level_timeline(hosted, base, events) + result["levels"] = [{"after": "entry" if s is None else "event %d %s" % (s, k), "pairs_0_3": list(lv)} + for k, s, lv in timeline] + r = routes(timeline, events, stage_pair) + need(r["PR2540_early_records"]["mass"] == 128, "PR2540: 16 records x one level = 128 (its 16 H8)") + need([x["capture_level"] for x in r["INIT64"]] == [-1, 2, 4, 6], "INIT capture levels -1/2/4/6") + need([x["mass"] for x in r["INIT64"]] == [1152, 768, 512, 256], "INIT climbs 72/48/32/16 per array") + need([x["capture_level"] for x in r["d_A"]] == [1, 3, 5], "d_A capture levels 1/3/5") + need([x["mass"] for x in r["d_A"]] == [448, 320, 192], "d_A climbs 56/40/24 per array") + need(r["INIT64_plus_dA_mass"] == 3648 and r["d_A_only_mass"] == 960, "INIT64 + d_A 3648; d_A alone 960") + need(r["x_last_write_event"] == [6, 27, 26, 25] and r["y_consumer_levels"] == [2, 8, 8, 8] + and all(r["x_last_write_levels_all_pairs"][k] == [8, 8, 8, 8] for k in (1, 2, 3)), + "X_(k,U) last written at events 6/27/26/25; bridges 25-27 run with every pair at level 8 (P_Y levels 2/8/8/8)") + need(r["INIT64_plus_dA_y_mass"] == 2496, "earliest timing the observed Y fields allow (P_Y): 2496") + need(r["early_consumer_levels"] == [2, 4, 6, 8] and r["INIT64_plus_dA_early_consumer_mass"] == 1344, + "P_early (each bank after its last local call): 1344 = 8 per later data incidence") + tb = r["theorem_B"] + need(tb["P_final"]["original"] == {"one_level_cut_sum": 1952, "own_bank": 1952, "count_only": 1952} + and tb["P_final"]["all_initial"] == {"one_level_cut_sum": 1824, "own_bank": 1824, "count_only": 1824}, + "Theorem B per cut with one consumer level (P_final): 1952 / 1824 (= cheapest 62 climbs)") + need((tb["P_Y"]["original"]["own_bank"], tb["P_Y"]["all_initial"]["own_bank"], + tb["P_early"]["original"]["own_bank"], tb["P_early"]["all_initial"]["own_bank"]) == (1344, 1216, 800, 608), + "Theorem B with the own-bank premise: 1344 / 1216 (P_Y), 800 / 608 (P_early)") + need((tb["P_Y"]["original"]["count_only"], tb["P_Y"]["all_initial"]["count_only"], + tb["P_early"]["original"]["count_only"], tb["P_early"]["all_initial"]["count_only"]) == (608, 544, 112, 0), + "Theorem B count-only deliveries: 608 / 544 (P_Y), 112 / 0 (P_early)") + need(all(tb[t][v]["one_level_cut_sum"] is None for t in ("P_Y", "P_early") for v in ("original", "all_initial")), + "the one-level cut sum is not applied to multi-level timings") + zw = r["zero_witness"] + need(zw["law_mass_per_array"] == 0 and zw["calls_in_window"] == [0, 1, 2, 3, 4, 5] + and zw["consumer_before_event"] == 14, "zero witness: pair 3 untouched through stages 0..5") + need(zw["levels_advanced"] == 0, "zero-advance window: pair 3 stays at level -1") + lag = r["lagging_record_example"] + need(lag["last_write_event_of_X0"] == 6 and lag["levels_advanced"] == 6 and lag["calls_after_capture"] == 3 + and lag["law_mass_if_independent_row"] == 48 and lag["C_mass"] == 24 + and lag["pair0_events_after_capture"] == ["idle_cover_sweep", "bridge src=0 dst=1", + "terminal_Y_translations", "terminal"], + "lagging example: X_(0,U) last written at event 6, so the record duplicates an observed row") + ai = r["all_initial_variant"] + need([x["final_mass"] for x in ai["reads"]] == [384, 256, 128] and [x["early_mass"] for x in ai["reads"]] == [0, 0, 0] + and [x["early_read_level"] for x in ai["reads"]] == [2, 4, 6] + and [x["early_read_after_event"] for x in ai["reads"]] == [5, 11, 17], + "all-initial reads: 384/256/128 at the end; 0 at P_early (pair k+1 reaches bank k's level first)") + need((ai["final_mass"], ai["y_mass"], ai["early_mass"]) == (3456, 2304, 1152) + and [x["y_mass"] for x in ai["reads"]] == [0, 256, 128], "all-initial variant 3456 / 2304 / 1152") + fh = r["forward_histories_addon"] + need(fh["final_mass_range"] == [768, 1024] and fh["y_mass_range"] == [384, 640] and fh["early_mass_range"] == [0, 256] + and fh["f2_f4_f6_only"] == {"P_final": [768, 960], "P_Y": [384, 576], "P_early": [0, 192]}, + "forward histories f2/f4/f6/f8 would add 768..1024 (P_final), 384..640 (P_Y), 0..256 (P_early)") + wo = r["without_decoder_timing_premise"] + need(wo == {"after_own_last_capture": {"consumer_levels": [1, 3, 5, 6], "original": 512, "all_initial": 512}, + "after_backward_call": {"consumer_levels": [1, 3, 5, 7], "original": 640, "all_initial": 640}}, + "without the decoder-timing premise: 512 (after own last capture) / 640 (after each backward call)") + f0 = r["init0_via_f0"] + need(f0["init_capture_levels"] == [0, 2, 4, 6] + and f0["original"] == {"P_final": 3520, "P_Y": 2368, "P_early": 1216} + and f0["all_initial"] == {"P_final": 3328, "P_Y": 2176, "P_early": 1024} + and f0["thmB_own_bank"]["P_Y"] == {"original": 1216, "all_initial": 1088} + and f0["thmB_own_bank"]["P_early"] == {"original": 800, "all_initial": 608} + and f0["thmB_one_level_end"] == {"original": 1952, "all_initial": 1824}, + "bank 0's INIT via f0: every P_rank total falls by 128; own-bank P_Y 1216 / 1088; others unchanged") + rt = r["revival_terms"] + need(rt == {"dA_term": {"P_final": 960, "P_Y": 576, "P_early": 192}, + "all_initial_reads_term": {"P_final": 768, "P_Y": 384, "P_early": 0}}, + "revival terms: d_A 960 / 576 / 192; all-initial reads 768 / 384 / 0") + r["hosting"] = hosting_checks(hosted, r) + need(r["hosting"]["pair3_X_hosted_slots_in_window"] == 160, "pair-3 X streams host 160 residuals in the window") + need(r["hosting"]["route_capture_slot_checks"] == 4173 and r["hosting"]["instants_checked"] == 21, + "hosting checked at 21 instants (4,173 slot checks at the seven route captures)") + centre_path = 8 * 8 * STAGES + pr2197 = 8 * 18 + h_U1, h_L, h_q, h_I = 17, 9, 1, 0 + need(centre_path == 576 and pr2197 == 144, "centre path 576 / PR2197 144") + need(224 * (h_U1 - h_L) == 1792 and 112 * (h_U1 - h_q) + 112 * (h_U1 - h_I) == 3696, "PR2678 1792 / 3696") + need(h_L == 9 and h_U1 - h_L == COORDS_PER_LEVEL, "PR2540 frames: F_L nine axes, F_U1 seventeen (one level)") + published, uniform = array_calls(), array_calls((7, 5, 3)) + need(published == 464 and uniform == 456 and 8 * uniform == r["INIT64_plus_dA_mass"], + "array-calls 464 published / 456 uniform; law = 8 x uniform array-calls") + r["array_calls"] = {"published": published, "uniform_lifetime": uniform, "S_units_published": published, + "C_mass_published": 8 * published, "C_mass_uniform": 8 * uniform} + r["controls"] = {"PR2540": 128, "PR2197": pr2197, "PR2678_common_FL": 1792, "PR2678_entry": 3696, + "centre_path_per_replica": centre_path} + # Re-check only of #2707's own published comparison (research/qq16-line-normalized-decoder, incorporated on + # main after this package's base): 336 H1 versus PR2540's 224 H1 + 16 H8 differ by 112 H1 - 16 H8, and + # 16 * 8^(1-a) > 112 for 0 <= a <= 1/16 because 8^(15/16) > 7, i.e. 8^15 > 7^16 (exact integers). + need(8 ** 15 > 7 ** 16 and 336 - 224 == 112 and 16 * 8 == 128, "PR2707 numerator sign: 8^15 > 7^16") + r["qq16_gate"] = {"retained_caller_retention_mass": 128, "retained_caller_H8": 16, + "zero_retention_H1_minus_retained_H1": 112, "sign_certificate": "8^15 > 7^16"} + result["routes"] = r + C = load_ceiling() + tb = r["theorem_B"] + result["pricing"] = pricing_checks(C, { + "INIT64_plus_dA_law": r["INIT64_plus_dA_mass"], "d_A_only_law": r["d_A_only_mass"], + "INIT64_plus_dA_earliest_Y_law": r["INIT64_plus_dA_y_mass"], + "INIT64_plus_dA_early_relaxation_law": r["INIT64_plus_dA_early_consumer_mass"], + "INIT64_plus_dA_S_published": published, "INIT64_plus_dA_C_published": 8 * published, + "all_initial_law": ai["final_mass"], "all_initial_earliest_Y_law": ai["y_mass"], + "all_initial_early_relaxation_law": ai["early_mass"], + "thmB_one_level_end": tb["P_final"]["original"]["one_level_cut_sum"], + "all_initial_thmB_one_level_end": tb["P_final"]["all_initial"]["one_level_cut_sum"], + "thmB_own_bank_earliest_Y": tb["P_Y"]["original"]["own_bank"], + "all_initial_thmB_own_bank_earliest_Y": tb["P_Y"]["all_initial"]["own_bank"], + "thmB_own_bank_early_relaxation": tb["P_early"]["original"]["own_bank"], + "all_initial_thmB_own_bank_early_relaxation": tb["P_early"]["all_initial"]["own_bank"], + "thmB_count_only_earliest_Y": tb["P_Y"]["original"]["count_only"], + "all_initial_thmB_count_only_earliest_Y": tb["P_Y"]["all_initial"]["count_only"], + "thmB_count_only_early_relaxation": tb["P_early"]["original"]["count_only"], + "all_initial_thmB_count_only_early_relaxation": tb["P_early"]["all_initial"]["count_only"], + "without_P_dec_after_own_last_capture": wo["after_own_last_capture"]["original"], + "without_P_dec_after_backward_call": wo["after_backward_call"]["original"], + "init0_via_f0_law": f0["original"]["P_final"], "init0_via_f0_earliest_Y_law": f0["original"]["P_Y"], + "init0_via_f0_early_law": f0["original"]["P_early"], + "all_initial_init0_via_f0_law": f0["all_initial"]["P_final"], + "all_initial_init0_via_f0_earliest_Y_law": f0["all_initial"]["P_Y"], + "all_initial_init0_via_f0_early_law": f0["all_initial"]["P_early"], + "init0_via_f0_thmB_own_bank_earliest_Y": f0["thmB_own_bank"]["P_Y"]["original"], + "all_initial_init0_via_f0_thmB_own_bank_earliest_Y": f0["thmB_own_bank"]["P_Y"]["all_initial"], + "revival_dA_term_end": rt["dA_term"]["P_final"], "revival_dA_term_earliest_Y": rt["dA_term"]["P_Y"], + "revival_all_initial_reads_end": rt["all_initial_reads_term"]["P_final"], + "revival_all_initial_reads_earliest_Y": rt["all_initial_reads_term"]["P_Y"]}) + routes_priced = result["pricing"]["routes"] + result_table = result["pricing"]["mass_breakeven_units_per_replica"] + for name in ("INIT64_plus_dA_law", "d_A_only_law", "INIT64_plus_dA_earliest_Y_law", "INIT64_plus_dA_C_published", + "INIT64_plus_dA_early_relaxation_law", "all_initial_law", "all_initial_earliest_Y_law", + "all_initial_early_relaxation_law", "thmB_one_level_end", "all_initial_thmB_one_level_end", + "thmB_own_bank_earliest_Y", "all_initial_thmB_own_bank_earliest_Y", "init0_via_f0_law", + "init0_via_f0_earliest_Y_law", "init0_via_f0_early_law", "all_initial_init0_via_f0_law", + "all_initial_init0_via_f0_earliest_Y_law", "all_initial_init0_via_f0_early_law", + "init0_via_f0_thmB_own_bank_earliest_Y", "all_initial_init0_via_f0_thmB_own_bank_earliest_Y", + "revival_dA_term_end"): + need(routes_priced[name]["idle_priced_kappa_cap"] is None and routes_priced[name]["rank8_priced_kappa_cap"] is None, + name + ": no positive saving") + for name in ("thmB_own_bank_early_relaxation", "all_initial_thmB_own_bank_early_relaxation", "thmB_count_only_earliest_Y", + "without_P_dec_after_backward_call", "revival_all_initial_reads_end"): + cap = routes_priced[name] + need(cap["idle_priced_kappa_cap"] is not None and Q(cap["idle_priced_kappa_cap"]) < SELECTED_KAPPA + and Q(cap["rank8_priced_kappa_cap"]) < SELECTED_KAPPA, + name + ": positive ceiling, but below the selected kappa (and hence every pending claim)") + for name in ("all_initial_thmB_count_only_earliest_Y", "thmB_count_only_early_relaxation", + "all_initial_thmB_count_only_early_relaxation"): + need(Q(routes_priced[name]["idle_priced_kappa_cap"]) > SELECTED_KAPPA + and Q(routes_priced[name]["rank8_priced_kappa_cap"]) > SELECTED_KAPPA, + name + ": a delivery meeting Theorem B's count alone stays above the selected kappa (count does not decide)") + # The decoder-timing premise is load-bearing: decoders right after each bank's own last capture leave a cap + # above the selected kappa and above PR2474. + cap = routes_priced["without_P_dec_after_own_last_capture"] + need(Q(cap["idle_priced_kappa_cap"]) > PR2474_KAPPA and Q(cap["rank8_priced_kappa_cap"]) > PR2474_KAPPA, + "without P_dec, 512 units leave a cap above the selected kappa and PR2474 (the premise is load-bearing)") + # Revival: the original variant's d_A term at P_Y (576) beats the selected record only, not PR2474 or any pending + # claim; the all-initial variant at P_Y leaves the INIT information a budget of break-even - 384. + need(beats(C, 576, "idle", SELECTED_KAPPA) and beats(C, 576, "rank8", SELECTED_KAPPA) + and not beats(C, 576, "idle", PR2474_KAPPA) and not beats(C, 576, "rank8", PR2474_KAPPA), + "d_A term at P_Y (576): beats the selected record (at its rank-8 break-even), not PR2474") + be_sel, be_2474 = (result_table["selected_1094"]["idle_units"], result_table["PR2474"]["idle_units"]) + need((be_sel - 384, be_2474 - 384) == (195, 189), "all-initial at P_Y: INIT budget 195 (selected) / 189 (PR2474) units") + result["frame_model"] = frame_model_checks() + result["tensor_toy"] = tensor_toy() + result["negative_controls_rejected"] = negative_controls(hosted, base, events, C) + n_neg = len(result["negative_controls_rejected"]) + 3 # + upward-only bound + two toy controls + fm = result["frame_model"] + status = ("PASS_RETAINED_ARRAY_CATCH_UP pr2540=128 init64_dA=3648/2496/1344 all_initial=3456/2304/1152 dA_only=960 " + "thmB_one_level=1952/1824 thmB_own_bank=1344/1216/800/608 thmB_count_only=608/544/112/0 " + "without_P_dec=512/640 init0_via_f0=3520/2368/1216 " + "array_calls=464/456 no_saving=896 breakeven_S=573 breakeven_C=71 zero_advance_calls=6 " + "hosted_instants=%d frame_instances=%d/%d negative_controls=%d no_new_kappa" + % (r["hosting"]["instants_checked"], fm["record_partner_instances"], fm["general_instances"], n_neg)) + result["status"] = status + text = json.dumps(result, indent=1, sort_keys=True) + "\n" + target = PACKAGE / "RESULT.json" + if "--write" in argv: + if target.exists() and target.read_text() != text and "--force" not in argv: + raise CheckFailure("RESULT.json differs; use --write --force to replace it") + target.write_text(text) + elif target.exists(): + need(json.loads(target.read_text()) == json.loads(text), "RESULT.json matches the recomputation") + print(status) + + +if __name__ == "__main__": + try: + main(sys.argv[1:]) + except CheckFailure as exc: + print("FAIL:", exc) + sys.exit(1)