Execute the completion/splitting pass as a lockstep rule and prove nested owned-bank lifetimes (no new kappa)

research/lockstep-completion-pass/PROOF.md

@@ -0,0 +1,136 @@
+# The completion/splitting pass as a lockstep rule, and nested owned-bank lifetimes
+
+Two written lemmas with event-level corroboration. Both live inside the retained
+contract of `FINITE-PRECOMPILATION.md` (Jacob Alan Sussman's Theorem 1G flow, the
+integer batch clearing, source complements and exit substitution) and of
+`p7-TENSOR.md` / `higher-moment-strictification` (zxv: chronological product, paid
+completion of small targets on their own owners, disjoint splitting at a cutoff).
+Nothing here changes a raw native word, a paid invoice, a moment inequality or κ.
+
+Notation. A *rule* is a finite native unit: roles `(name_i, k_i)` on pairwise
+distinct arbitrary fields, an ordered list of paid rounds `(r_j, owner_j)` where
+`owner_j` is a role name or an owned bank name, and a fixed list of owned banks.
+Its compiled rank-`N` program is the lockstep flow executed by `executor.py`
+(derived from our `lockstep-live-role-audit/live_roles.py`, #4691), which keeps for
+every physical field the stack of live roles and checks I1–I6 at every event.
+
+## Lemma A. The pass produces a lockstep rule with an exact invoice
+
+Let `U` be a rule whose paid ranks may overlap its target ranks, let `m` be its
+ambient rank and choose integers `0 < J < L <= m`. Define `U' = pass(U, J, L)`:
+
+1. every role of rank `k_i < L` gets rank `L`;
+2. every original round `(r_j, owner_j)` is replaced by the consecutive rounds
+   `(J, owner_j) x q, (r, owner_j)` with `r_j = qJ + r`, `0 <= r < J` (the
+   remainder round is omitted when `r = 0`); the first of them is tagged `orig`,
+   the others `piece`;
+3. after all of these, for every role with `k_i < L`, the rounds
+   `(J, name_i) x q', (r', name_i)` with `L - k_i = q'J + r'`, tagged `completion`.
+
+**Claim.** (a) `U'` satisfies the hierarchy `r_max(U') <= J < L <= k_min(U')`, so the
+finite compiler and the executor apply to it. (b) Every compiled program of `U'`
+satisfies I1–I6; in particular every added job is a whole job on a field whose
+current owner is the issuing unit, so no completion or piece ever touches a parked
+ancestor, a sibling's field or an array outside the unit. (c) Rank-one mass:
+`T'_1 - P'_1 = T_1 - P_1`, and the added target mass equals the added paid mass
+`sum_{k_i<L} (L - k_i)`. For every `t` in `(0,1)`, the net-tax identity (1) of
+`net-tax-rank-compiler/PROOF.md` holds:
+`T'_t - P'_t = T_t - P_t - sum_j tau(r_j) - sum_{k_i<L} E(k_i)`. (d) Per unit
+instance the pass adds exactly `sum_j (ceil(r_j/J) - 1)` piece rounds,
+`sum_{k_i<L} ceil((L-k_i)/J)` completion rounds, `2 |{i : k_i < L}|` whole-job
+normalizer records (inverse map at the input, map at the output of a completed
+role) and one block-address relocation per piece or completion round. A compiled
+rank-`N` program contains `U_total(N)` unit instances (one lockstep copy has
+`sum_classes |C|` units; the program has `a` copies plus its nested complement and
+exit programs), so every count of the program is `U_total(N)` times the per-unit
+count plus the counts of the nested programs.
+
+*Proof.* (a) After step 2 every paid rank is at most `J`; after step 1 every target
+rank is at least `L > J`. (b) The compiler never looks at the owner of a round
+except to decide on which field the unit issues the job; the executor checks at
+every round that the field's top entry is the issuing unit (I3) and that the
+previous child class has returned (lockstep). A `piece` round has the same owner
+as its original job: between two pieces the child class of the first piece has
+returned, the unit is resumed and owns the field again, so the second piece is a
+legal round. A `completion` round of role `i` is issued on the role's own array
+after all original rounds; by I4 all children have returned, the unit is the top
+of that array's stack, and the job of rank `L - k_i` is served by a child class
+exactly like any other round (the Pascal matching only uses ranks). The disjoint
+axes `k_i .. L-1` exist on that array because its role now has rank `L` in `U'`:
+in the flow a role of rank `L` at column `col` is an `L col`-axis job on its
+array, of which the native word uses `k_i col` axes and the completion the rest
+(`p7-TENSOR.md` §2). The general induction of #4691 (fresh sources, one job per
+round on an owned field, distinct fields within a class, LIFO undoing) is
+unchanged, since the pass only changes ranks and adds rounds of the same shape.
+(c) Splitting preserves rank mass; completion adds `L - k_i` to the target and to
+the paid mass of the same unit. Identity (1) is the regrouping of the four sums by
+original job and by completed role; `verify.py` evaluates both sides exactly at
+`t = 1` and with 60 significant digits at `t = 1 - C`. (d) is the definition of
+the pass; the executor counts the records while it runs and the histogram-level
+counter multiplies the per-unit counts by `U_total`; both agree on every case.
+
+**Scope.** Lemma A is about the rule and the compiled flow. The native content of
+a completion job (a positive transform on `L - k_i` disjoint axes) and of the
+whole-job normalizers is the inherited all-column hypothesis; the identity
+`(A tensor B) = (A tensor I)(I tensor B)` behind splitting is hypothesis 2 of
+`FINITE-PRECOMPILATION.md` §1. The strict moment inequality that makes the
+completed unit profitable is zxv's theorem; it is not re-proved here.
+
+## Lemma B. Owned-bank lifetimes are nested; the stack allocation is sufficient
+
+`FINITE-PRECOMPILATION.md` §6 allocates one owned-centre bank per compiled unit
+instance ("the safe finite allocation"), notes that one bank per recursion depth is
+insufficient, and says that a smaller reuse allocation "requires its own lifetime
+proof". This is that proof for the lockstep schedule.
+
+**Claim.** In the executed rank-`N` program, at every event the set of unit
+instances holding live owned banks is exactly the union of the classes on the
+current class path `C_0, C_1, ..., C_d` of the current program together with the
+same sets of every program on the current nesting chain (an exit or complement
+program running inside a round). Consequently bank lifetimes are properly nested
+and a single LIFO stack of bank slots suffices; its peak occupancy is
+
+```
+peak(N) = max( max_s peak(N-s) ,
+               max_path ( a * nb * sum_{j=0..G} |C_j(path)| + max_{r paid} peak(r * dil(path)) ) ),
+```
+
+with `nb` banks per unit, `a` the replication factor, `|C_j|` the class sizes of
+one lockstep copy and `dil(path)` the product of the paid ranks along the path, so
+that the exit programs of a path have ranks `r * dil(path)` (`counts.py`,
+`Counts.banks`; `FlowCounts.exit_paths` keeps, for each deepest dilation, the
+largest live inventory of a path reaching it). The maximum is over compatible
+(path, exit) pairs: the path inventory and the exit rank are tied by the same paid
+ranks, and adding the two separate maxima can overestimate (review of #5443: a
+two-generation rule at N = 45 executes with peak 2048, the decoupled sum gives 2050;
+it is a regression case in `verify.py` and a control in `test_verify.py`). The total number of instances is
+`total(N) = a nb sum_classes |C| + sum_s (a S_s / B_{N-s}) total(N-s) + sum_e (a t_e / B_e) total(e)`.
+
+*Proof.* A class allocates the banks of all its units when it starts and frees them
+when it ends. A child class starts inside one round of its parent class and ends
+before the parent advances to the next round (lockstep: the executor rejects an
+eager parent). An exit program starts inside the last round of the deepest class
+and returns before the next exit group; a complement program runs before the flow
+and returns before any class starts. Every program restores all stacks on return
+(I4). Hence the live set at any event is as claimed, allocation and release are
+LIFO, and the peak over the execution is the maximum over the finitely many
+(path, nested chain) combinations of the live counts, where a nested exit
+program belongs to the path whose deepest class runs it; this is the displayed
+recursion. The executor implements the stack allocator (`owned_policy="stack"`),
+requires at every class end that the class's banks are exactly the top of the
+stack (I7) and that a bank is free when allocated (its live-role stack is empty,
+which is the erasure contract: a bank is cleared by its unit before release), and
+records the peak; `verify.py` requires the measured peak and total to equal the
+recursion on every executed case, in full-width and in partial (two-copy) mode.
+
+**What it buys.** The owned-field inventory `O` in the retained storage count
+`Z = W + O` can be the peak instead of the number of instances, with no change to
+`G`, `E` or any moment. For the selected #5413 profile after the pass at `v = 1`
+(`J = 20`, `L = 21`, 77,204 rounds per unit) and top rank `N = 3045` (one
+generation), one lockstep copy has 84,996 unit instances but at most 7,793 live
+at once; including replication and nested programs the ratio total/peak is 346
+(RESULT.json). For `v = 1024` the recursion is defined but not evaluated.
+
+**Rejected alternatives.** One bank per depth aliases simultaneously live units
+(rejected, as in #4691). Releasing a class's banks before its rounds lets a child
+class reuse a bank the parent still uses for a paid job (rejected by I3).

research/lockstep-completion-pass/README.md

@@ -0,0 +1,120 @@
+# Literal completion/splitting pass and nested owned-bank lifetimes in the lockstep compiler
+
+**Scoped positive result; no new κ.** Target 10 of zxv's #5428 asks for a uniform
+fixed-tape compiler theorem and suggests starting with "one chronological
+completion/splitting pass" and "owner allocation/erasure". This package supplies two
+narrow pieces of that foundation, both executed event by event rather than only
+counted:
+
+1. **The pass is a rule.** Completion of every small target to the floor `L` on its
+   own owner, followed by splitting of every paid job at the cutoff `J`
+   (`p7-TENSOR.md` §§2–3, `higher-moment-strictification` §1), is a transformation
+   `U -> U'` of finite native units. `U'` satisfies the lockstep hierarchy, every
+   compiled program of `U'` passes the ownership invariants I1–I6 of our #4691
+   executor, every added job is a whole job on a field its unit owns, the rank-one
+   surplus is preserved exactly, the net-tax identity (1) holds, and the added
+   records (pieces, completions, normalizer pairs, relocations) have a closed
+   per-unit count that the executor reproduces. [PROOF.md](PROOF.md), Lemma A.
+2. **Owned-bank lifetimes are nested.** `FINITE-PRECOMPILATION.md` §6 allocates one
+   owned bank per compiled unit instance and says a smaller reuse allocation
+   "requires its own lifetime proof". In the lockstep schedule the live units are
+   exactly the classes on the current path plus the nested programs, so a LIFO stack
+   of bank slots suffices; its peak is an explicit recursion. The executor runs the
+   stack allocator with invariant I7 (a finishing class's banks are the top of the
+   stack) and its measured peak equals the recursion on every case. Lemma B.
+
+## Evidence (`verify.py`, standard library, CPython 3.12)
+
+- **Counting parity.** The histogram-level counter (`counts.py`, no unit
+  enumeration) equals #4691's unit-level counting compiler on the toy rule at
+  N = 4..64 and the BIT-shaped rule at N = 50, 400, 3200, and reproduces the
+  FINITE-DAG-AUDIT receipt at toy rank 40.
+- **Complete profiles, histogram level.** For the p7 invoice (`c=10, b=15`,
+  C = 0.00268648) and the selected #5413 invoice (`c=20, b=21`, C = κ) at tensor
+  powers v = 1, 2, 3: identity (1) holds to 40 digits, the rank-one surplus is
+  unchanged (608 for p7, 752 for the selected profile, raised to the power v), the
+  added target and paid masses agree, and `max paid <= J < L <= min target`
+  afterwards. At v = 1 the selected unit has 77,204 rounds after the pass:
+  64,260 original, 5,152 pieces and 7,792 completions on the 7,792 fields of rank
+  4, 7, 8, 9 and 17; 15,584 normalizer records and 12,944 relocations.
+- **Event-level execution with the stack allocator.** Toy rule (N = 7..28, full
+  width), an overlapping toy rule after the pass (`J=4, L=5`, N = 40 and 64, full
+  width: 12,048 and 112,738 bank allocations with peaks 732 and 8,751), two
+  p7-shaped rules (`J=10, L=15`, N = 1815) and three selected-shaped rules with the
+  caller's chronology shape and random, all-on-centre and one-owner chronologies
+  (`J=20, L=21`, N = 3045), and a two-generation rule with path-dependent class
+  sizes and exit ranks (N = 45 and 69, full width, peaks 2048 and 16,386). Peak, total, unit instances, pieces, completions,
+  normalizer and relocation records all equal the formulas.
+- **Complete profiles, compiled counts.** p7 at N = 1815 and the selected profile
+  at N = 3045 (one generation each): width, leaves, units per copy, peak units per
+  copy and the total/peak bank ratio (346 for the selected profile), with a hash of
+  the exact integers.
+- **Controls** (`test_verify.py`): the overlapping rule is not a lockstep rule
+  before the pass; a cutoff not below the floor, a dropped split remainder and a
+  short completion are rejected or break the mass law; a foreign completion owner
+  is refused; the release-early allocator, the per-depth allocation, an eager
+  parent and a repeated exit field are rejected; the peak recursion without its
+  nested term undercounts, and the one that adds the largest path to the largest
+  exit peak from a different path overcounts (2050 against the executed 2048); a wrong tax breaks identity (1); a tampered
+  RESULT.json is rejected.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/lockstep-completion-pass
+```
+
+## Scope and limits
+
+- The pass and the compiler are executed on reduced-multiplicity rules with the
+  real rank sets and on the complete profiles at histogram level. The literal
+  chronology of the 64,260 paid calls of #5413 (which call acts on which field)
+  is not bound here; the shaped rules use the caller's event structure (LOCAL
+  blocks of small-rank jobs on helper fields and the owned centre, IDLE jobs of
+  rank 16..72 on main fields, rank-one queries on the owned bank) with random and
+  adversarial owners.
+- Record counts are exact; their tape prices are the retained primitive prices
+  (a child call on a contiguous axis block, a block address permutation, a whole-job
+  normalizer record), not re-derived. No numerical movement bill is claimed.
+- The native content of completion jobs and normalizers, the all-column lift, the
+  strict moment inequality, precision, analytic recovery and the selected κ are
+  inherited and unchanged. The v = 1024 selected template is not materialized;
+  the recursions of Lemma B are stated for it but evaluated only at v = 1.
+
+## Relation to the physical half of `native_all_columns`
+
+PR #5442 (`research/allwidth-caller-certificate`) closes the algebraic half of
+`native_all_columns`: the caller's identities hold at every column width `f`. Its
+physical half stays open: executing `g^(tensor f)` and the port adapters on a fixed
+number of tapes, for all `f` columns at once with one fixed primitive list, without
+disturbing spectator fields, at the retained tariff. Lemmas A and B do **not** supply
+that. They are statements at the level of the rule and the compiled flow: they fix
+*which* records the pass and the compiler add (child calls on contiguous axis
+blocks, block relocations, normalizer pairs, bank initialisation and erasure), how
+many of them one unit instance and one compiled program contain, and on which
+owned fields they act. The `f`-dependent tape price of each such record type is
+exactly the open physical obligation named in #5442; this package gives it an
+exact record count to multiply, not the price. The element inventory of the selected
+caller that such a price would have to cover is listed by PR #5442 (port wrappers,
+`D`, `C0`, `X0`, the helper alias monomials and the 145-axis `J` routes); the tariff
+domain `f <= p` is recorded in `research/final4610-independent-admission/SPECIALIZATION.md` §3.
+
+## Open next questions
+
+1. Bind the actual owners of the selected caller's paid calls (`invoice.json`
+   chronology plus the #5402 provider schedule) and execute the literal 77,204-round
+   rule at two lockstep copies. First step: extract per-event owner fields from
+   `NEUTRAL-BACKWARD-v16c.json`.
+2. Price the added records with the retained native tariff to obtain a numeric
+   movement bill per unit instance. First step: the 171-record monomial bound of
+   the #4610 review for the normalizer pairs.
+3. Evaluate `peak(N)` and `total(N)` for larger N (two generations) with
+   memoisation over dilations; the present recursion over all sub-ranks is slow
+   beyond one generation for the selected profile.
+
+## Credit
+
+Jacob Alan Sussman (Theorem 1G lockstep flow), Cinna Davis (PR4412/4414/4416
+product and completion), zxv (`higher-moment-strictification`, `net-tax-rank-compiler`,
+#5428), Nick Petalas (#4832 sharp split charge), Chris R / Clear1nsight (#5413),
+Dillon (#5402), Ali Romman (#5383/#5398), Cao Yifan (#4610), and our own #4691
+executor. Prepared by Mark (Matarener) with substantial Claude Code assistance.
+Apache-2.0. No independent human review or formal-kernel verification is claimed.