Add P104 owned-lineage factorization and scoped review of PR6170's owned-layer floor

research/p104-owned-lineage-floor-review/PROOF.md

@@ -0,0 +1,133 @@
+# Proofs: owned-lineage factorization, tree branching, eight-lineage floor
+
+Notation follows DreamingOfClouds' [PR6170](https://github.com/CrocSwap/integer-mult-bounds/pull/6170)
+`research/p104-designer-toolkit-v2/P104-LEMMAS.md` (sections 0.2, 9-11). P_M accounting: every owned MOVE
+arrival becomes a fresh symbol sigma_mu with rho(sigma_mu) = the real value that moved. The move mu has a
+gather frame g_mu and a landing L_mu strictly inside g_mu. u_mu(j) is the coefficient of sigma_mu in the
+P_M final of Y_j, v_mu = x(rho sigma_mu), and C = sum_mu u_mu v_mu^T. Gamma_ji = p_j . p_i over F2, so the
+diagonal is 1 because ports have odd weight. A pair is *non-orthogonal* when Gamma_ji = 1.
+
+Facts used from PR6170, each recounted by `verify.py` with 0 violations on PR5907, PR6030, PR6144 and PR6167:
+- R1: u_mu(j) != 0 implies L_mu inside p_j^perp.
+- P3a: the x-content of the public part of any P_M value at frame g lies on ports of g.
+- R3: C = delta on every non-orthogonal pair.
+- R4: the gaps of the owned moves sum to owned paid.
+
+## Definitions
+
+The *ancestors* of a move are the symbols present in its mover's P_M value. An ancestry edge nu -> mu is
+**SAME** if L_nu = g_mu and **STRICT** otherwise; a STRICT edge is a public relay. An owned layer is
+**relay-free** if every edge is SAME, and **merge-free** if every move has at most one ancestor. A
+**lineage** is a root-to-leaf path of the resulting forest. *Branching* means one symbol is an ancestor of
+several moves.
+
+## Lemma 1 (lineage factorization)
+
+*Machine-checked in Lean: `lean/Lineage/Basic.lean` (`factor`, `alpha_support`, `beta_support`,
+`lineage_cost`, `paid_telescope`).*
+
+Let a lineage have moves 1..t, gathers g_l, landings L_l = g_{l+1}, and v_l = c_l v_{l-1} + w_l with
+w_l in X(g_l) (P3a), v_0 = 0 and c_l != 0. Then there are alpha, beta in Q^104 with
+
+(i) C^lineage_ji = alpha_j beta_i on every non-orthogonal pair (j, i);
+(ii) beta_i != 0 implies p_i in g_1, and alpha_j != 0 implies L_t inside p_j^perp;
+(iii) dim g_1 - dim L_t >= rank_F2 Gamma[supp alpha, supp beta], and the left side is the lineage's owned
+paid.
+
+*Proof.* Put e(i) = max{l : p_i in g_l} (0 if none) and r(j) = min{l : L_l inside p_j^perp}. Frames
+decrease, so p_i lies in g_l iff l <= e(i), and L_l lies in p_j^perp iff l >= r(j). So w_l(i) != 0 needs
+l <= e(i), and u_l(j) != 0 needs l >= r(j) by R1. For a non-orthogonal pair, e(i) >= r(j)+1 would put p_i in
+g_{r(j)+1} = L_{r(j)}, inside p_j^perp, so p_i . p_j = 0; hence e(i) <= r(j). For l >= e(i) no more
+coordinate i is injected, so v_l(i) = (pi_l/pi_{e(i)}) v_{e(i)}(i) with pi_l = c_1...c_l. Then
+
+C_ji = sum_{l >= r(j)} u_l(j) v_l(i) = (sum_l u_l(j) pi_l)(v_{e(i)}(i)/pi_{e(i)}) = alpha_j beta_i.
+
+(ii) is read off the definitions. For (iii), Gamma[supp alpha, supp beta] is part of the F2 pairing between
+L_t^perp and g_1, whose rank is at most dim g_1 - dim L_t because L_t lies inside g_1. Telescoping the SAME
+edges gives the lineage's paid (R4). []
+
+## Lemma 2 (trees)
+
+In a relay-free, merge-free owned forest (branching allowed) there is one pair (alpha^P, beta^P) per leaf P.
+On every non-orthogonal pair, C_ji = sum_P alpha^P_j beta^P_i, where beta^P_i = v_kappa(i)/pi_kappa and
+kappa is the deepest node on P's root path whose gather contains p_i. The path cost bound (iii) holds for
+every leaf.
+
+*Proof.* As in Lemma 1, for a node mu with u_mu(j) != 0 and a non-orthogonal pair, p_i is not in L_mu.
+So the deepest node kappa with p_i in its gather lies on mu's root path at or above mu. The same kappa
+serves every leaf below mu, and C^mu_ji = (u_mu(j) pi_mu) beta_i(kappa). Assign each node to one leaf
+below it and sum. []
+
+*Branching condition.* If leaves P, P' separate below a node with landing L, then beta^P_i = beta^P'_i
+for every port i outside L, since the deepest gather node is shared. So supp(beta^P - beta^P') lies in L
+and dim L >= dim span supp(beta^P - beta^P').
+
+## Corollary (completion form)
+
+X := sum over leaves of alpha^P beta^P^T agrees with C on every non-orthogonal pair. So X o Gamma = I by R3,
+rank X <= #leaves, and owned paid >= sum over leaves of rank_F2 Gamma[supp alpha^P, supp beta^P], with the
+tree's cost replacing the sum when leaves share a prefix (Theorem 4). Any 8-clique gives rank X >= 8, so
+there are at least 8 leaves. With exactly 8 leaves, X is a rank-8 completion of the P104 pattern, hence
+X = D M0 D^-1 (Theorem U, prior art #1212). Then alpha^P = A x_P and beta^P = B y_P for dual bases, where
+the rows of A and B are the roots up to the diagonal gauge.
+
+This is the repository's masked decoder problem (`C(P104) >= 56`). Lineages are terms and lineage paid is
+the term cost. For at most 8 terms the floor 56 is already known; Theorem 3 re-proves it here by a
+different finite input. The case of 9 or more terms is open and is not addressed.
+
+## Finite facts (verify.py, exact integer arithmetic on the PR6030 completion)
+
+- **F1.** The 120 root lines: the 104 P104 lines have support 49 and span F2^9. The 16 lines of the two
+  frames removed from E8 have support 52 and span 16 distinct hyperplanes. Over all 440,880 one-dimensional
+  flats (W-orbits of the 8 fundamental coweights, `--flats`), the support span is F2^9 except for these
+  16 lines.
+- **F2.** For pairs of root directions, rank_F2 Gamma[S(x), S(y)] = 7 only when both lie on removed lines
+  (64 pairs); otherwise it is >= 8. Over all span pairs of all flats the ranks are 7, 8 or 9 (`--flats`).
+- **F3.** For every pair of removed lines y, y' and every z = y - mu y' (mu != 0) perpendicular to a P104
+  root, supp(Bz) spans F2^9. For all other pairs of root lines the minimum span is >= 8.
+
+## Theorem 3 (eight leaves, no branching)
+
+A relay-free, merge-free path forest with exactly 8 lineages has owned paid >= 56.
+
+*Proof.* By the Corollary, each lineage costs at least rank_F2 Gamma[supp A x, supp B y]. Every vector lies
+in some flat, and a one-dimensional flat inside it has a smaller support, so the minimum is attained on
+one-dimensional flats. By F1, both spans have dimension >= 8 inside F2^9 with its nondegenerate form. Hence
+the pairing rank is >= 8 - dim(span)^perp >= 7. That bound uses only the span dimensions from F1; F2 states
+the same minimum directly. So 8 lineages pay >= 56. []
+
+## Theorem 4 (eight leaves, branching allowed)
+
+A relay-free, merge-free owned forest with exactly 8 leaves has owned paid >= 56.
+
+*Proof.* Take a branching landing L. By the branching condition and F1, supp B(y_P - y_P') has span >= 8:
+a vector whose support spans only a hyperplane must be a removed line. Otherwise its flat contains a line of
+span 9, or two removed lines with different spans. So dim L >= 8. A gather has dim <= 9 and a landing is
+strictly inside its gather, so branching can only occur directly below a root move F9 -> H with dim H = 8.
+Two leaves on removed-line directions cannot share that step (F3: the landing would need span 9). Every
+other leaf costs >= 8 along its root path (F2). A group of k leaves under one shared step therefore costs
+>= 1 + 6 + 7(k - 1) = 7k, unshared leaves cost >= 7, and the total is >= 56. []
+
+## Remark (direct reads of X are covered)
+
+`research/fragmentation-ceiling/PROOF.md` (section 5) proves its centre bound A30-CUT under the modelling
+step P-ATOM (carriers get port content only by reading the port) and lists "decoders that read X directly
+(breaking P-ATOM)" among the doors outside its scope (section 6.7). In the P_M accounting used here no such
+step is needed. X lives are public registers, so by P3a (proved in PR6170 from SPEC nesting) a read of any
+X at frame g contributes x-content in X(g), exactly as any other public read at g. Lemma 1 only uses
+w_l in X(g_l), not which register supplied w_l. So every owned lineage that reads X directly, at any frame
+and time, is still a lineage of Lemma 1, and Lemma 2, Theorems 3 and 4 hold unchanged: a relay-free,
+merge-free owned layer with 8 leaves pays >= 56 whoever it reads. The label table is F2^9 because every
+frame is a subspace of F2^9, so this does not open the rank >= 10 table cases of the decoder floor either.
+What remains of that door is the relay case: an X that has received owned content (a symbol) and is read
+again is a STRICT relay, which is outside Lemma 1 (see Scope).
+
+## Scope
+
+Not covered: merges, STRICT relays, 9 or more leaves, and the orthogonal entries of C. NEED counts the
+orthogonal entries; C and X can differ there, as in PR6144 and PR6167: X has rank 8, C has rank 10,
+NEED is 4972. So nothing here proves PR6170's open premise NEED >= 3597.
+
+Related: PR6229 (`research/p104-two-clique-relay-floor`) and `research/p104-ambient-relay-floor` prove an
+8-unit floor for one 8-port two-clique block in the confined and ambient REL models, merges included. They
+do not give the 104-port statement above, and this note does not give their merge case.

research/p104-owned-lineage-floor-review/README.md

@@ -0,0 +1,130 @@
+# Owned-lineage factorization and a scoped review of PR6170's owned-layer floor
+
+This package reviews the floor framework of DreamingOfClouds'
+[PR6170](https://github.com/CrocSwap/integer-mult-bounds/pull/6170). It has two parts. The first is a scoped
+independent recount: own code recomputes PR6170's owned-delivery matrix C on four frontier words. The
+second is a short structural result: in PR6170's P_M accounting, a relay-free owned lineage contributes a
+rank-one matrix on every non-orthogonal port pair, and its owned paid bounds the F2 rank of that term. The
+consequence proved here is that **a relay-free, merge-free owned layer with exactly 8 leaves pays owned
+paid >= 56, even when lineages branch and share a common descent**. Proofs are in [PROOF.md](PROOF.md).
+No new word or kappa is claimed.
+
+## Status of the PR6170 floor (read from its own files)
+
+PR6170 is merged for archive only. Its intake record says: "Independent scientific review and
+source-bound replay remain open". No later PR re-checks the floor.
+
+- `P104-THEORY.md` sec 7 quotes a proved floor of 794.53 R0 (about 10%). The same file's CHARTORB addendum
+  declares 794.53 and 813.31 invalid (the inherited cap48 row) and corrects the figure to 754.14.
+- `P104-LEMMAS.md` sec 6 corrects 754.14 to 751.46 (A1 correction). Its sections 9-11 state that no floor
+  above 0 rests on SPEC + paid + literals alone. Every positive floor carries the measured scope NEED = 4972
+  (Z <= 20) and own/owns/ownc = 22/18/64. With the proved bound NEED >= 90 the certificate gives 0.00, and the
+  floor turns positive only from NEED >= 3597, which is open.
+- The LP solver, the certificate and its recheck are not in the package, and the rows "capfix, mains,
+  cpres" are not written out. So the LP cannot be rebuilt from the text, and it is not re-solved here.
+- The kappa law 1/kappa = 130.27 + .02364 (R0 + 380 (paid - 56)) is a fit on 11 words. A floor on R0 is
+  therefore not a proved kappa ceiling.
+
+## Result and evidence
+
+[verify.py](verify.py) layers 1-2 run on canonical main for each word: an exact real replay, a parallel
+P_M replay, and the lineage factorization.
+
+| word | owned symbols | owned paid | rank C | NEED | Z | lineages | lineage paid | lineage rank_F2 | rank X |
+|---|---|---|---|---|---|---|---|---|---|
+| PR5907 | 20 | 56 | 8 | 4992 | 0 | 8 | 7 each | 7 each | 8 |
+| PR6030 | 20 | 56 | 8 | 4992 | 0 | 8 | 7 each | 7 each | 8 |
+| PR6144 | 26 | 56 | 10 | 4972 | 20 | 8 | 7 each | 7 each | 8 |
+| PR6167 | 25 | 56 | 10 | 4972 | 20 | 8 | 7 each | 7 each | 8 |
+
+The four words agree with PR6170's numbers (r245g is PR6144's line, with rank 10 and NEED 4972). On all
+four, PUB + C = I holds exactly, R1, R3 and P3a hold with 0 violations, there are 0 STRICT edges, 0 merges
+and 0 branchings, and the rank-one identity of Lemma 1 has 0 mismatches. In PR6144/PR6167 C has rank 10,
+but the completion X built from the lineage terms has rank 8, which is the E8 completion.
+
+Layer 3 derives the E8 root data exactly from the PR6030 completion. The Gram matrix is integral, the
+104 roots close to 240 under reflections, and simple roots are recovered. The layer then checks the
+finite facts F1-F3 for root directions. Layer 4 (`--flats`) enumerates all 440,880 one-dimensional flats
+as W-orbits of the fundamental coweights and checks F1 and the span-pair ranks for every flat. All numbers
+are in [RESULT.json](RESULT.json).
+
+## Lean
+
+[lean/Lineage/Basic.lean](lean/Lineage/Basic.lean) formalises Lemma 1 in the abstract form used by the
+proof: values in any field `K`, frames as subspaces of any finite-dimensional `F`-space with any bilinear
+pairing `B`, an antitone frame sequence (SAME hand-offs), P3a as the hypothesis `hw` and R1 as `hu`.
+`factor` is (i) with the explicit vectors alpha_j = sum_l u_l(j) pi_l and beta_i = sum_k w_k(i)/pi_k,
+`alpha_support` / `beta_support` are (ii), `rank_le` and `lineage_cost` are (iii), and `paid_telescope`
+is the telescoping of SAME gaps. Because `hw` only asks where injected content lies, the formal statement
+covers lineages that read X directly (Remark in PROOF.md). No `sorry`; `#print axioms` gives `propext`,
+`Classical.choice`, `Quot.sound` only. Build (Lean `v4.33.0-rc1`, Mathlib pinned in `lake-manifest.json`,
+the same revision as other Lean packages here):
+
+```sh
+cd research/p104-owned-lineage-floor-review/lean && lake exe cache get && lake build
+```
+
+Not formalised: Lemma 2, Theorems 3-4 and the finite facts F1-F3 (these are checked by `verify.py`), and
+the identification of word events with the abstract data (checked on four words by `verify.py`).
+
+## Relation to existing work
+
+Corollary (completion form) identifies the relay-free owned layer with the repository's masked decoder
+problem `C(P104) >= 56`: lineages are terms and lineage paid is the term cost. The floor for at most
+8 terms is already known, and Theorem 3 re-derives it by a different finite input. New here:
+(a) the derivation inside PR6170's P_M accounting, which connects its NEED/REL framework to the decoder
+floor; and (b) Theorem 4, where terms may share cost through branching. That sharing is absent from the
+plain decoder model, and it does not lower the floor at 8 leaves.
+
+Two later packages treat the same owned-cost question in PR6170's confined REL model.
+[PR6229](https://github.com/CrocSwap/integer-mult-bounds/pull/6229) (`research/p104-two-clique-relay-floor`, Nick
+Petalas) proves that a block of two orthogonal four-port cliques needs 8 owned paid units, with chains,
+branching, merging and re-ascents allowed, through a cumulative bound `rank_Q(C o Gamma) <= owned paid` on a
+binary quotient. `research/p104-ambient-relay-floor` (AAAmirinu) extends that 8-port floor to frames that
+leave the block span. Both are local 8-port statements. This package works on the whole 104-port owned
+layer of real words, lineage by lineage, and does not cover merges. The two results are complementary;
+PR6229's cumulative row-space invariant is the natural tool for the merge case left open here.
+
+**Direct reads of X.** `research/fragmentation-ceiling` proves its centre bound under P-ATOM and lists
+"decoders that read X directly" as an open door. In the P_M accounting this door is closed for the
+relay-free, merge-free layer: by PR6170's P3a a read of X at frame g brings only x-content on ports of g,
+which is what Lemma 1 already allows, so the 8-leaf floor of 56 holds for decoders that read X at any frame
+(PROOF.md, Remark). Only X reads that carry owned symbols (STRICT relays) remain open.
+
+## Reproduction
+
+From the repository root with CPython 3.12 and NumPy:
+
+```sh
+python3.12 -B research/p104-owned-lineage-floor-review/verify.py
+python3.12 -B research/p104-owned-lineage-floor-review/verify.py --flats
+```
+
+The first command runs layers 1-3 (about 40 seconds on one hosted Linux core). The second replays only
+PR6030 and runs layers 3-4 (about 2 minutes). Markers: `PASS_P104_OWNED_LINEAGE_FLOOR_REVIEW` and `..._WITH_FLATS`.
+
+## Limitations
+
+- Not covered: merges (a mover carrying two symbols), STRICT relays, 9 or more leaves. The case of 9 or
+  more terms is the open masked decoder floor.
+- Nothing here controls the orthogonal entries of C, so PR6170's open premise NEED >= 3597 stays open,
+  and its positive floors stay conditional.
+- own/owns are not recounted: their exact definition is not given in PR6170's text.
+- The finite facts are computed on the PR6030 completion. PR5907, PR6144 and PR6167 have the same port set
+  and completion rank 8, so Theorem U makes the root data identical up to the diagonal gauge.
+- Lemma 1 is machine-checked in Lean (see Lean); the rest is not. No independent human review is claimed.
+
+## Open next questions
+
+- Does Lemma 1 extend to merges and STRICT relays? Start with one merged move: its symbol carries two
+  ancestor contents, and the rank-one form should split per ancestor.
+- Can the orthogonal entries of C be controlled lineage by lineage (pairs with e(i) > r(j))? That is the
+  gap between X and C, and the missing link to PR6170's NEED premise.
+
+## Credit
+
+DreamingOfClouds retains PR6170, its P_M accounting, the lemmas R1, P3a, R3, G1a, N1, N2 and N2(e), and the
+REL framework used here. Ali Romman retains PR6167; PR6030, PR6144 and PR5907 and their predecessors retain
+their attribution. Theorem U and the E8 completion are prior art (#1212). The masked decoder floor and its
+at-most-8-term case are prior repository work. Lemmas 1-2, Theorems 3-4 and the code are new, prepared for
+Matarener with Claude (Anthropic). New material is Apache-2.0.