From 5f9fb0a77a3a4678105f53fcd457adaff97021d8 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 29 Oct 2026 21:50:54 +0000 Subject: [PATCH 1/3] Add P104 owned-lineage factorization and scoped review of PR6170's owned-layer floor Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011VhYm9sv5h3SL8idn3hUem --- .../p104-owned-lineage-floor-review/PROOF.md | 116 +++++ .../p104-owned-lineage-floor-review/README.md | 105 +++++ .../RESULT.json | 208 +++++++++ .../SOURCES.json | 60 +++ .../p104-owned-lineage-floor-review/TASK.json | 81 ++++ .../VERIFY.json | 35 ++ .../p104-owned-lineage-floor-review/verify.py | 424 ++++++++++++++++++ 7 files changed, 1029 insertions(+) create mode 100644 research/p104-owned-lineage-floor-review/PROOF.md create mode 100644 research/p104-owned-lineage-floor-review/README.md create mode 100644 research/p104-owned-lineage-floor-review/RESULT.json create mode 100644 research/p104-owned-lineage-floor-review/SOURCES.json create mode 100644 research/p104-owned-lineage-floor-review/TASK.json create mode 100644 research/p104-owned-lineage-floor-review/VERIFY.json create mode 100644 research/p104-owned-lineage-floor-review/verify.py diff --git a/research/p104-owned-lineage-floor-review/PROOF.md b/research/p104-owned-lineage-floor-review/PROOF.md new file mode 100644 index 0000000000..4fc49ba1c8 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/PROOF.md @@ -0,0 +1,116 @@ +# 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) + +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. [] + +## 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. diff --git a/research/p104-owned-lineage-floor-review/README.md b/research/p104-owned-lineage-floor-review/README.md new file mode 100644 index 0000000000..4fc4c58c83 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/README.md @@ -0,0 +1,105 @@ +# 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). + +## 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. + +## 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. +- No independent human or proof-kernel 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. diff --git a/research/p104-owned-lineage-floor-review/RESULT.json b/research/p104-owned-lineage-floor-review/RESULT.json new file mode 100644 index 0000000000..b4071fb34b --- /dev/null +++ b/research/p104-owned-lineage-floor-review/RESULT.json @@ -0,0 +1,208 @@ +{ + "flats": { + "distinct_spans": 17, + "lines_with_dim8_span": 16, + "orbit_sizes": [ + 120960, + 120, + 1080, + 3360, + 34560, + 8640, + 241920, + 30240 + ], + "span_dims": { + "8": 16, + "9": 1 + }, + "span_pair_rank": { + "7": 64, + "8": 224, + "9": 1 + }, + "total_lines": 440880 + }, + "roots": { + "F1_distinct_dim8_spans": 16, + "F1_root_lines": { + "(False, 52, 8)": 16, + "(True, 49, 9)": 104 + }, + "F2_pair_rank": { + "(7, False, False)": 64, + "(8, False, False)": 192, + "(8, False, True)": 1664, + "(8, True, False)": 1664, + "(9, True, True)": 10816 + }, + "F3_branch_landing_min_span": { + "(8, False, True)": 29, + "(8, True, False)": 35, + "(8, True, True)": 384, + "(9, False, False)": 120, + "(9, False, True)": 737, + "(9, True, False)": 863, + "(9, True, True)": 4972 + }, + "root_lines": 120 + }, + "words": { + "5907": { + "NEED": 4992, + "PUB_plus_C_eq_I": true, + "R1_violations": 0, + "R3_violations": 0, + "STRICT_edges": 0, + "X_Gamma_eq_I_violations": 0, + "Z": 0, + "branching_symbols": 0, + "cost_bound_holds": true, + "lineage_paid": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "lineage_rankF2": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "lineages": 8, + "merges": 0, + "orthogonal_ordered_pairs": 4992, + "owned_paid": 56, + "rankQ_C": 8, + "rankQ_X": 8, + "rank_one_mismatches": 0, + "symbols": 20 + }, + "6030": { + "NEED": 4992, + "PUB_plus_C_eq_I": true, + "R1_violations": 0, + "R3_violations": 0, + "STRICT_edges": 0, + "X_Gamma_eq_I_violations": 0, + "Z": 0, + "branching_symbols": 0, + "cost_bound_holds": true, + "lineage_paid": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "lineage_rankF2": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "lineages": 8, + "merges": 0, + "orthogonal_ordered_pairs": 4992, + "owned_paid": 56, + "rankQ_C": 8, + "rankQ_X": 8, + "rank_one_mismatches": 0, + "symbols": 20 + }, + "6144": { + "NEED": 4972, + "PUB_plus_C_eq_I": true, + "R1_violations": 0, + "R3_violations": 0, + "STRICT_edges": 0, + "X_Gamma_eq_I_violations": 0, + "Z": 20, + "branching_symbols": 0, + "cost_bound_holds": true, + "lineage_paid": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "lineage_rankF2": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "lineages": 8, + "merges": 0, + "orthogonal_ordered_pairs": 4992, + "owned_paid": 56, + "rankQ_C": 10, + "rankQ_X": 8, + "rank_one_mismatches": 0, + "symbols": 26 + }, + "6167": { + "NEED": 4972, + "PUB_plus_C_eq_I": true, + "R1_violations": 0, + "R3_violations": 0, + "STRICT_edges": 0, + "X_Gamma_eq_I_violations": 0, + "Z": 20, + "branching_symbols": 0, + "cost_bound_holds": true, + "lineage_paid": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "lineage_rankF2": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "lineages": 8, + "merges": 0, + "orthogonal_ordered_pairs": 4992, + "owned_paid": 56, + "rankQ_C": 10, + "rankQ_X": 8, + "rank_one_mismatches": 0, + "symbols": 25 + } + } +} diff --git a/research/p104-owned-lineage-floor-review/SOURCES.json b/research/p104-owned-lineage-floor-review/SOURCES.json new file mode 100644 index 0000000000..64b0a52d91 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-helper468-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "7ffe7b500b02b9d0de49a85ec53e36004f1a411f", + "sha256": "b69a9cb3a26d4f40aa7ad14f814b188fe16a782999f6f56292538e447d67b284" + }, + { + "path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-root-relay-descent-2/WORD.json.gz", + "usage": "input", + "git_blob": "69b70ee50c697b185ebf585fbe69f2487af32d1d", + "sha256": "c71985d96bf3d4a35aae111aaba87e376f7367efb4a5686278ef293732757533" + }, + { + "path": "research/p104-retained-operand-descent/WORD.json.gz", + "usage": "input", + "git_blob": "f2d3f98964f939e5ca652f9b1453a0604f15f829", + "sha256": "68d1ff048bc6d30d85ceaeb38e2557adab87b20a9c67cf73948f95f54104575f" + }, + { + "path": "research/p104-designer-toolkit-v2/P104-LEMMAS.md", + "usage": "provenance", + "git_blob": "129f28dd10c9e1c43d29a9dd280e022070288a73", + "sha256": "54263ecdcabb067b1f77749ae60cb1f430c02fd720b63e5e39f358f6bfee78ec" + }, + { + "path": "research/p104-designer-toolkit-v2/P104-THEORY.md", + "usage": "provenance", + "git_blob": "c97d5c20bc60f95df1b1907f31f35085f4b4e99d", + "sha256": "8087ef0533d36bf234916401dbdc6a49f23cceaf088c0b417d26d0b8d347fb4d" + }, + { + "path": "docs/research/pr-intake-decisions.json", + "usage": "provenance", + "git_blob": "4b2b3326428046716142a5bfe307263627161283", + "sha256": "5c978bcdfe2108d531becf790f4c6a7300f923676cb932a8f64627b5437ef7ab" + } + ] +} diff --git a/research/p104-owned-lineage-floor-review/TASK.json b/research/p104-owned-lineage-floor-review/TASK.json new file mode 100644 index 0000000000..d4b0a67dd5 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Scoped review of PR6170's owned-layer floor framework and an owned-lineage factorization: own exact P_M recount of the owned-delivery matrix C on PR5907, PR6030, PR6144 and PR6167; proof that a relay-free owned lineage contributes a rank-one term on every non-orthogonal pair with paid >= its F2 rank; floor owned paid >= 56 for relay-free, merge-free owned layers with exactly 8 leaves, branching included.", + "scope_change_reason": "The card asks whether a legal decoder change can improve the moment. PR6170 prices the owned layer through NEED and a floor LP whose positive values rest on measured scopes; its intake leaves independent review open. The factorization shows that the relay-free owned layer is the masked decoder problem C(P104) >= 56, and branching lineages (shared owned descents, outside the plain decoder model) are the remaining owned-cost lever at 8 terms.", + "bottleneck_link": "Side result for the decoder route: it closes shared owned descents as a way below 56 owned paid at 8 leaves (each owned rank is about 380 R0-equivalent in PR6170's fitted law). It does not change kappa.", + "budget_minutes": 240, + "stop_rule": "Stop when the recount, the factorization on all four words and the finite facts F1-F3 (and all one-dimensional flats) pass, or one fails with a counterexample; no search for new words.", + "outcome": "completed", + "evidence": "research/p104-owned-lineage-floor-review/RESULT.json", + "author": "Matarener", + "ai_assistance": "Prepared with Claude (Anthropic) via Claude Code.", + "open_questions": [ + { + "question": "Does the lineage factorization extend to merges and STRICT relays?", + "why_it_matters": "Together with the masked floor for 9+ terms it would give owned paid >= 56 for every owned layer.", + "first_step": "Treat one merged move: split its symbol content per ancestor, or lift PR6229's cumulative row-space invariant from its two-clique quotient to the full port set.", + "blocked_by": "No frontier word has merges or STRICT edges, so there is no test instance." + }, + { + "question": "Can the orthogonal entries of C be controlled lineage by lineage?", + "why_it_matters": "It is the gap between X and C and the missing link to PR6170's open premise NEED >= 3597.", + "first_step": "Classify the orthogonal pairs with e(i) > r(j) per lineage on PR6144 and count which can vanish.", + "blocked_by": "None; open." + } + ] +} \ No newline at end of file diff --git a/research/p104-owned-lineage-floor-review/VERIFY.json b/research/p104-owned-lineage-floor-review/VERIFY.json new file mode 100644 index 0000000000..e362fbd453 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.5.4" + ], + "inputs": [ + "research/p104-helper468-rung-removal/WORD.json.gz", + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-root-relay-descent-2/WORD.json.gz", + "research/p104-retained-operand-descent/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticated inputs; own exact real and P_M replay of the PR5907, PR6030, PR6144 and PR6167 words: owned-delivery matrix C, PUB + C = I, R1, R3, P3a, NEED, Z, rank C, owned paid, SAME/STRICT ancestry, merges and branching; lineage factorization (rank one on every non-orthogonal pair, lineage paid >= F2 rank, completion X with X o Gamma = I and rank 8); exact E8 root data from the PR6030 completion and finite facts F1-F3 on root directions; result equals RESULT.json." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--flats" + ], + "timeout_seconds": 600, + "checks": "Own exact P_M replay of the PR6030 word (source of the completion), exact E8 root data and finite facts F1-F3, plus all 440,880 one-dimensional flats of the E8 arrangement as W-orbits of the fundamental coweights (exact integers): support spans and all span-pair F2 ranks; result equals RESULT.json." + } + ] +} \ No newline at end of file diff --git a/research/p104-owned-lineage-floor-review/verify.py b/research/p104-owned-lineage-floor-review/verify.py new file mode 100644 index 0000000000..7964a9e891 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/verify.py @@ -0,0 +1,424 @@ +#!/usr/bin/env python3 +"""Owned-lineage factorization and scoped review of PR6170's owned-layer floor framework. Apache-2.0. + +Prepared for Matarener with Claude (Anthropic), via Claude Code. Python 3.12, standard library plus NumPy +(integer arithmetic only). Nothing is imported from PR6170. + +Layers: + 1. own exact replay of the PR5907, PR6030, PR6144 and PR6167 words in real values and in PR6170's P_M + accounting (every owned MOVE arrival becomes a fresh symbol): owned-delivery matrix C, PUB + C = I, + R1, R3, NEED, Z, rank C, owned paid, symbol ancestry (SAME/STRICT, merges, branching); + 2. lineage factorization (PROOF.md, Lemma 1): for every lineage, C^lineage = alpha_j beta_i on every + non-orthogonal pair, path paid >= rank_F2 Gamma[supp alpha, supp beta]; X = sum alpha beta^T agrees + with I on all non-orthogonal pairs and has rank 8; + 3. root data of the E8 completion (exact integers): Gram of the 104 roots from X, closure to 240 roots, + simple roots; facts F1 (support spans of root lines), F2 (pair ranks of root directions) and + F3 (branching landings of root-direction pairs); + 4. (--flats; replays only PR6030 and layers 3-4) all 440,880 one-dimensional flats of the E8 arrangement as W-orbits of the fundamental + coweights (exact integers): support spans and all span-pair ranks (fact F1 for every flat). +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import gzip, json, sys +import numpy as np + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORDS = {'5907': 'research/p104-helper468-rung-removal/WORD.json.gz', + '6030': 'research/p104-helper470-twin-rung-removal/WORD.json.gz', + '6144': 'research/p104-root-relay-descent-2/WORD.json.gz', + '6167': 'research/p104-retained-operand-descent/WORD.json.gz'} + + +def log(kind, **data): + print(kind, json.dumps(data, sort_keys=True, default=str)[:400], flush=True) + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def authenticate(): + for row in json.loads((HERE/'SOURCES.json').read_text())['files']: + if row['usage'] == 'input': + need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], 'source pin '+row['path']) + + +def span(basis): + s = {0} + for v in basis: + s |= {x ^ v for x in s} + return frozenset(s) + + +def reduce_basis(vecs): + """canonical reduced echelon basis of the F2 span (tuple, sorted)""" + piv = {} + for v in vecs: + for p in sorted(piv, reverse=True): + if (v >> p) & 1: + v ^= piv[p] + if v: + p = v.bit_length()-1 + for q in piv: + if (piv[q] >> p) & 1: + piv[q] ^= v + piv[p] = v + return tuple(sorted(piv.values())) + + +def f2rank(vecs): + return len(reduce_basis(vecs)) + + +def dot2(a, b): + return bin(a & b).count('1') & 1 + + +def qrank(rows): + M = [dict(r) for r in rows if r] + rank = 0 + for c in sorted({k for r in M for k in r}): + p = next((i for i in range(rank, len(M)) if M[i].get(c)), None) + if p is None: + continue + M[rank], M[p] = M[p], M[rank] + pr = M[rank] + for i in range(rank+1, len(M)): + a = M[i].get(c) + if a: + f = a/pr[c] + t = dict(M[i]) + for k, v in pr.items(): + t[k] = t.get(k, 0)-f*v + M[i] = {k: v for k, v in t.items() if v} + rank += 1 + return rank + + +def addrow(t, s, q): + t = dict(t) + for k, v in s.items(): + t[k] = t.get(k, 0)+q*v + return {k: v for k, v in t.items() if v} + + +# ---------------------------------------------------------------- layers 1-2 +def owned_layer(name): + w = json.loads(gzip.decompress((ROOT/WORDS[name]).read_bytes())) + F = w['frames'] + S = [span(f) for f in F] + n, m = w['public'], w['owned_fields'] + live, ports = list(w['live']), list(w['ports']) + need(len(live) == len(ports) == 104, 'P104 ports') + xidx = {x: j for j, x in enumerate(live)} + cur = list(w['initial'])+[None]*m + real = [{r: Q(1)} for r in range(n+m)] + pm = [{r: Q(1)} for r in range(n+m)] + sym = [] + for i, e in enumerate(w['program']): + op, r = e[0], e[1] + if op == 'MOVE': + a, b, private = e[2], e[3], e[4] + need(cur[r] == a and (S[b] < S[a] if private else S[a] < S[b]), 'nesting at %d' % i) + if private: + anc = sorted({k[1] for k in pm[r] if isinstance(k, tuple)}) + # P3a: public part of the mover's value has x-content on ports of the gather frame + need(all(ports[xidx[k]] in S[a] for k in pm[r] if k in xidx), 'P3a at %d' % i) + sym.append({'g': a, 'L': b, 'rho': dict(real[r]), 'anc': anc}) + pm[r] = {('s', len(sym)-1): Q(1)} + cur[r] = b + elif op in ('INIT', 'CLEAR'): + real[r], pm[r] = {}, {} + cur[r] = e[2] if op == 'INIT' else None + else: + q, f = Q(e[-2]), e[-1] + need(cur[r] == f, 'chart at %d' % i) + if op == 'SCALE': + real[r] = {k: q*v for k, v in real[r].items()} + pm[r] = {k: q*v for k, v in pm[r].items()} + else: + s = e[2] + need(cur[s] == f, 'common chart at %d' % i) + if op == 'COPY': + real[r] = {k: q*v for k, v in real[s].items()} + pm[r] = {k: q*v for k, v in pm[s].items()} + else: + real[r] = addrow(real[r], real[s], q) + pm[r] = addrow(pm[r], pm[s], q) + for x in live: + need(real[x+112] == {x+112: Q(1), x: Q(1)}, 'real Y final') + ns = len(sym) + U = [[pm[x+112].get(('s', k), Q(0)) for x in live] for k in range(ns)] + V = [[s['rho'].get(x, Q(0)) for x in live] for s in sym] + G = [[dot2(ports[j], ports[i]) for i in range(104)] for j in range(104)] + C = [[sum(U[k][j]*V[k][i] for k in range(ns)) for i in range(104)] for j in range(104)] + pub_ok = all(pm[x+112].get(xi, 0)+C[j][i] == (1 if i == j else 0) + for j, x in enumerate(live) for i, xi in enumerate(live)) + r3 = sum(1 for j in range(104) for i in range(104) if G[j][i] and C[j][i] != (1 if i == j else 0)) + orth = sum(1 for j in range(104) for i in range(104) if i != j and not G[j][i]) + needc = sum(1 for j in range(104) for i in range(104) if i != j and not G[j][i] and C[j][i]) + r1 = sum(1 for k, s in enumerate(sym) for j in range(104) if U[k][j] and any(dot2(b, ports[j]) for b in F[s['L']])) + strict = sum(1 for s in sym for a in s['anc'] if S[sym[a]['L']] != S[s['g']]) + merges = sum(1 for s in sym if len(s['anc']) > 1) + kids = Counter(a for s in sym for a in s['anc']) + branching = sum(1 for v in kids.values() if v > 1) + paid = sum(len(F[s['g']])-len(F[s['L']]) for s in sym) + out = {'symbols': ns, 'owned_paid': paid, 'rankQ_C': qrank([{i: C[j][i] for i in range(104) if C[j][i]} for j in range(104)]), + 'NEED': needc, 'Z': orth-needc, 'orthogonal_ordered_pairs': orth, 'PUB_plus_C_eq_I': pub_ok, + 'R1_violations': r1, 'R3_violations': r3, 'STRICT_edges': strict, 'merges': merges, 'branching_symbols': branching} + # lineages + child = {a: k for k, s in enumerate(sym) for a in s['anc']} + roots = [k for k, s in enumerate(sym) if not s['anc']] + paths = [] + for r0 in roots: + p, k = [], r0 + while k is not None: + p.append(k); k = child.get(k) + paths.append(p) + X = [[Q(0)]*104 for _ in range(104)] + mism, costs, ranks = 0, [], [] + for p in paths: + Cp = [[sum(U[k][j]*V[k][i] for k in p) for i in range(104)] for j in range(104)] + alpha, beta = {}, {} + rem = {(j, i) for j in range(104) for i in range(104) if G[j][i] and Cp[j][i]} + while rem: + j0, i0 = min(rem) + alpha[j0], beta[i0] = Q(1), Cp[j0][i0] + grown = True + while grown: + grown = False + for (j, i) in sorted(rem): + if j in alpha and i not in beta: + beta[i] = Cp[j][i]/alpha[j]; grown = True + elif i in beta and j not in alpha: + alpha[j] = Cp[j][i]/beta[i]; grown = True + if j in alpha and i in beta: + rem.discard((j, i)) + mism += sum(1 for j in range(104) for i in range(104) if G[j][i] and Cp[j][i] != alpha.get(j, 0)*beta.get(i, 0)) + Sa = sorted(j for j in alpha if alpha[j]); Tb = sorted(i for i in beta if beta[i]) + ranks.append(f2rank([sum(1 << t for t, i in enumerate(Tb) if G[j][i]) for j in Sa])) + costs.append(sum(len(F[sym[k]['g']])-len(F[sym[k]['L']]) for k in p)) + for j in Sa: + for i in Tb: + X[j][i] += alpha[j]*beta[i] + xg = sum(1 for j in range(104) for i in range(104) if G[j][i] and X[j][i] != (1 if i == j else 0)) + out.update({'lineages': len(paths), 'lineage_paid': sorted(costs), 'lineage_rankF2': sorted(ranks), + 'rank_one_mismatches': mism, 'cost_bound_holds': all(r <= c for r, c in zip(ranks, costs)), + 'X_Gamma_eq_I_violations': xg, + 'rankQ_X': qrank([{i: X[j][i] for i in range(104) if X[j][i]} for j in range(104)])}) + log('L1_L2', word=name, **out) + return out, X, ports + + +# ---------------------------------------------------------------- layer 3: exact root data +def root_data(X, ports): + n = 104 + G = [[0]*n for _ in range(n)] + for i in range(n): + need(X[i][i] == 1, 'unit diagonal') + G[i][i] = 2 + for j in range(n): + if i != j: + if X[i][j] == 0: + need(X[j][i] == 0, 'E8 completion zero pattern') + else: + need(X[i][j]*X[j][i] == Q(1, 4) and (X[i][j] > 0) == (X[j][i] > 0), 'E8 completion entries') + G[i][j] = 0 if X[i][j] == 0 else (1 if X[i][j] > 0 else -1) + # basis of 8 roots and rational coordinates of all 104 + piv = [] + for j in range(n): + cand = piv+[j] + if np.linalg.matrix_rank(np.array([[G[a][b] for b in cand] for a in cand], dtype=float)) == len(cand): + piv = cand + if len(piv) == 8: + break + Gb = [[Q(G[a][b]) for b in piv] for a in piv] + inv = invert(Gb) + coords = [tuple(sum(inv[r][c]*G[piv[c]][j] for c in range(8)) for r in range(8)) for j in range(n)] + ip = lambda u, v: sum(u[a]*Gb[a][b]*v[b] for a in range(8) for b in range(8)) + for j in range(n): + for k in range(n): + need(ip(coords[j], coords[k]) == G[j][k], 'root coordinates') + # reflection closure in exact integers: scale coordinates by the common denominator d + from math import lcm + d = lcm(*[x.denominator for c in coords for x in c]) + Gi = np.array([[int(x) for x in row] for row in Gb], dtype=np.int64) + Vs = np.array([[int(x*d) for x in c] for c in coords], dtype=np.int64) + Vs = np.unique(np.concatenate([Vs, -Vs]), axis=0) + while True: + IP = Vs @ Gi @ Vs.T + need((IP % (d*d) == 0).all(), 'integral inner products') + IP //= d*d + new = (Vs[None, :, :]-IP[:, :, None]*Vs[:, None, :]).reshape(-1, 8) + nxt = np.unique(np.concatenate([Vs, new]), axis=0) + if len(nxt) == len(Vs): + break + Vs = nxt + roots = {tuple(Q(int(x), d) for x in v) for v in Vs} + need(len(roots) == 240, 'E8 closure') + # simple roots for a generic functional, integer coordinates in the simple basis + gen = [Q(7**t+3*t, 1) for t in range(8)] + pos = [r for r in roots if sum(g*x for g, x in zip(gen, r)) > 0] + posset = set(pos) + simple = [r for r in pos if not any(tuple(r[t]-a[t] for t in range(8)) in posset for a in pos)] + need(len(simple) == 8, 'simple roots') + Cart = [[int(ip(a, b)) for b in simple] for a in simple] + Sinv = invert([[simple[c][r] for c in range(8)] for r in range(8)]) + to_simple = lambda v: tuple(sum(Sinv[r][c]*v[c] for c in range(8)) for r in range(8)) + allroots = [] + for r in roots: + s = to_simple(r) + need(all(x.denominator == 1 for x in s), 'integral root') + allroots.append(tuple(int(x) for x in s)) + p104 = [tuple(int(x) for x in to_simple(c)) for c in coords] + return np.array(Cart, dtype=np.int64), allroots, p104 + + +def invert(M): + k = len(M) + A = [list(M[i])+[Q(int(i == j)) for j in range(k)] for i in range(k)] + for c in range(k): + p = next(i for i in range(c, k) if A[i][c]) + A[c], A[p] = A[p], A[c] + A[c] = [x/A[c][c] for x in A[c]] + for i in range(k): + if i != c and A[i][c]: + A[i] = [x-A[i][c]*y for x, y in zip(A[i], A[c])] + return [row[k:] for row in A] + + +def canon_line(v): + v = np.asarray(v, dtype=np.int64) + nz = np.nonzero(v)[0] + if v[nz[0]] < 0: + v = -v + g = np.gcd.reduce(np.abs(v[nz])) + return tuple((v//g).tolist()) + + +def layer3(Cart, allroots, p104, ports): + R = np.array(p104, dtype=np.int64) # 104 x 8, simple coordinates + lines = sorted({canon_line(r) for r in allroots}) + need(len(lines) == 120, 'root lines') + inP = [canon_line(r) in {canon_line(q) for q in p104} for r in [np.array(l) for l in lines]] + vals = (np.array(lines) @ Cart) @ R.T # + supp = [np.nonzero(row)[0].tolist() for row in vals] + keys = [reduce_basis([ports[j] for j in s]) for s in supp] + f1 = Counter((p, len(s), len(k)) for p, s, k in zip(inP, supp, keys)) + dim8 = {k for k in keys if len(k) == 8} + pair = Counter() + for a in range(120): + for b in range(120): + if set(supp[a]) & set(supp[b]): + r = f2rank([sum(1 << t for t, i in enumerate(supp[b]) if dot2(ports[j], ports[i])) for j in supp[a]]) + pair[(r, inP[a], inP[b])] += 1 + # F3: branching landings, z = y_a - mu y_b perpendicular to some P104 root (mu != 0) + tree = Counter() + for a in range(120): + for b in range(a+1, 120): + best = 9 + for k in range(104): + pa, pb = int(vals[a][k]), int(vals[b][k]) + if pa == 0 or pb == 0: + continue + z = pb*np.array(lines[a], dtype=np.int64)-pa*np.array(lines[b], dtype=np.int64) + s = np.nonzero((z @ Cart) @ R.T)[0].tolist() + best = min(best, f2rank([ports[j] for j in s])) + tree[(best, inP[a], inP[b])] += 1 + out = {'root_lines': 120, 'F1_root_lines': {str(k): v for k, v in sorted(f1.items())}, + 'F1_distinct_dim8_spans': len(dim8), + 'F2_pair_rank': {str(k): v for k, v in sorted(pair.items())}, + 'F3_branch_landing_min_span': {str(k): v for k, v in sorted(tree.items())}} + log('L3', **out) + return out + + +# ---------------------------------------------------------------- layer 4: all flats +def layer4(Cart, allroots, p104, ports): + R = np.array(p104, dtype=np.int64) + pos = np.array(sorted({canon_line(r) for r in allroots}), dtype=np.int64) # 120 reflections + Cinv = np.round(np.linalg.inv(Cart.astype(float))).astype(np.int64) + need((Cinv @ Cart == np.eye(8, dtype=np.int64)).all(), 'unimodular Cartan') + spans, total, orbit_sizes = {}, 0, [] + for k in range(8): + start = np.array(canon_line(Cinv[k]), dtype=np.int64) # fundamental coweight in root coordinates + enc = lambda A: ((A.astype(np.int64)+64) * (128**np.arange(8, dtype=np.int64))).sum(axis=1) + seen = enc(start[None, :]) + layer, allv = start[None, :], [start[None, :]] + while len(layer): + cand = [] + for c0 in range(0, len(layer), 2000): + part = layer[c0:c0+2000] + ip = part @ Cart @ pos.T # (l, 120) + new = (part[:, None, :]-ip[:, :, None]*pos[None, :, :]).reshape(-1, 8) + nz = (new != 0).argmax(axis=1) + new = new*np.sign(new[np.arange(len(new)), nz])[:, None] + new = new//np.gcd.reduce(np.abs(new), axis=1)[:, None] + need((np.abs(new) < 64).all(), 'coordinate range for keys') + kk, idx = np.unique(enc(new), return_index=True) + cand.append((kk, new[idx])) + keys = np.concatenate([c[0] for c in cand]); rows = np.concatenate([c[1] for c in cand]) + keys, idx = np.unique(keys, return_index=True); rows = rows[idx] + fresh = ~np.isin(keys, seen, assume_unique=True) + layer = rows[fresh] + seen = np.union1d(seen, keys[fresh]) + if len(layer): + allv.append(layer) + L = np.concatenate(allv) + orbit_sizes.append(len(L)); total += len(L) + masks, counts = np.unique(np.packbits((L @ Cart) @ R.T != 0, axis=1), axis=0, return_counts=True) + for mk, cnt in zip(masks, counts): + s = np.nonzero(np.unpackbits(mk)[:104])[0] + key = reduce_basis([ports[j] for j in s]) + spans[key] = spans.get(key, 0)+int(cnt) + log('L4_orbit', coweight=k, lines=len(L), distinct_spans=len(spans)) + keys = list(spans) + pr = Counter() + for A in keys: + for B in keys: + pr[f2rank([sum(1 << t for t, b in enumerate(B) if dot2(a, b)) for a in A])] += 1 + out = {'total_lines': total, 'orbit_sizes': orbit_sizes, 'distinct_spans': len(keys), + 'span_dims': dict(sorted(Counter(len(k) for k in keys).items())), + 'lines_with_dim8_span': sum(v for k, v in spans.items() if len(k) == 8), + 'span_pair_rank': dict(sorted(pr.items()))} + log('L4', **out) + return out + + +def main(): + authenticate() + res = {'words': {}} + X30 = ports30 = None + flats = '--flats' in sys.argv and '--write' not in sys.argv + for name in (['6030'] if flats else WORDS): + out, X, ports = owned_layer(name) + res['words'][name] = out + if name == '6030': + X30, ports30 = X, ports + Cart, allroots, p104 = root_data(X30, ports30) + res['roots'] = layer3(Cart, allroots, p104, ports30) + if '--flats' in sys.argv: + res['flats'] = layer4(Cart, allroots, p104, ports30) + got = json.loads(json.dumps(res, sort_keys=True, default=str)) + if '--write' in sys.argv: + (HERE/'RESULT.json').write_text(json.dumps(got, indent=1, sort_keys=True)+'\n') + print('WROTE RESULT.json') + return + want = json.loads((HERE/'RESULT.json').read_text()) + if flats: # --flats replays only PR6030 (source of the completion) and adds layer 4 + need(got['words']['6030'] == want['words']['6030'], 'result differs from RESULT.json: words.6030') + got.pop('words') + else: + need('flats' in want, 'RESULT.json lacks layer 4') + want = {k: v for k, v in want.items() if k != 'flats'} + for key in got: + need(got[key] == want[key], 'result differs from RESULT.json: '+key) + print('PASS_P104_OWNED_LINEAGE_FLOOR_REVIEW' + ('_WITH_FLATS' if '--flats' in sys.argv else '')) + + +if __name__ == '__main__': + main() From b235f3b8ecb1c5ccddfbe66ca8cf77c83f1e20bc Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Fri, 30 Oct 2026 21:43:02 +0000 Subject: [PATCH 2/3] P104 owned-lineage review: direct reads of X are covered by P3a fragmentation-ceiling lists decoders that read X directly (breaking P-ATOM) as an open door. In the P_M accounting a read of X at frame g brings only x-content on ports of g (P3a), which Lemma 1 already allows, so the 8-leaf floor of 56 holds whoever the lineage reads. Only STRICT relays remain open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011VhYm7mMPx9hftdqgAF8he --- research/p104-owned-lineage-floor-review/PROOF.md | 14 ++++++++++++++ research/p104-owned-lineage-floor-review/README.md | 6 ++++++ .../p104-owned-lineage-floor-review/SOURCES.json | 6 ++++++ 3 files changed, 26 insertions(+) diff --git a/research/p104-owned-lineage-floor-review/PROOF.md b/research/p104-owned-lineage-floor-review/PROOF.md index 4fc49ba1c8..cfb57ee669 100644 --- a/research/p104-owned-lineage-floor-review/PROOF.md +++ b/research/p104-owned-lineage-floor-review/PROOF.md @@ -105,6 +105,20 @@ Two leaves on removed-line directions cannot share that step (F3: the landing wo 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 diff --git a/research/p104-owned-lineage-floor-review/README.md b/research/p104-owned-lineage-floor-review/README.md index 4fc4c58c83..6ecf7a092b 100644 --- a/research/p104-owned-lineage-floor-review/README.md +++ b/research/p104-owned-lineage-floor-review/README.md @@ -66,6 +66,12 @@ leave the block span. Both are local 8-port statements. This package works on th 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: diff --git a/research/p104-owned-lineage-floor-review/SOURCES.json b/research/p104-owned-lineage-floor-review/SOURCES.json index 64b0a52d91..30fdabdfeb 100644 --- a/research/p104-owned-lineage-floor-review/SOURCES.json +++ b/research/p104-owned-lineage-floor-review/SOURCES.json @@ -55,6 +55,12 @@ "usage": "provenance", "git_blob": "4b2b3326428046716142a5bfe307263627161283", "sha256": "5c978bcdfe2108d531becf790f4c6a7300f923676cb932a8f64627b5437ef7ab" + }, + { + "path": "research/fragmentation-ceiling/PROOF.md", + "usage": "provenance", + "git_blob": "c4033090d7cd35d9c80744922c587ae115b1de8a", + "sha256": "28be45a551ed8491be1ebb8c64acba2834aaa402452cb02e3c71c83e49232264" } ] } From 57aeceb6800e0137c85841b354648a153ef62ee7 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Fri, 30 Oct 2026 21:48:38 +0000 Subject: [PATCH 3/3] P104 owned-lineage review: Lean formalisation of Lemma 1 Abstract lineage factorization (rank one on non-orthogonal pairs), support conditions, the rank bound dim G1 - dim L and SAME telescoping, for any value field and any bilinear pairing. Standard axioms only, no sorry. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011VhYm7mMPx9hftdqgAF8he --- .../p104-owned-lineage-floor-review/PROOF.md | 3 + .../p104-owned-lineage-floor-review/README.md | 21 ++- .../lean/.gitignore | 1 + .../lean/Lineage.lean | 1 + .../lean/Lineage/Basic.lean | 160 ++++++++++++++++++ .../lean/lake-manifest.json | 117 +++++++++++++ .../lean/lakefile.toml | 10 ++ .../lean/lean-toolchain | 1 + 8 files changed, 313 insertions(+), 1 deletion(-) create mode 100644 research/p104-owned-lineage-floor-review/lean/.gitignore create mode 100644 research/p104-owned-lineage-floor-review/lean/Lineage.lean create mode 100644 research/p104-owned-lineage-floor-review/lean/Lineage/Basic.lean create mode 100644 research/p104-owned-lineage-floor-review/lean/lake-manifest.json create mode 100644 research/p104-owned-lineage-floor-review/lean/lakefile.toml create mode 100644 research/p104-owned-lineage-floor-review/lean/lean-toolchain diff --git a/research/p104-owned-lineage-floor-review/PROOF.md b/research/p104-owned-lineage-floor-review/PROOF.md index cfb57ee669..59ab4c8a27 100644 --- a/research/p104-owned-lineage-floor-review/PROOF.md +++ b/research/p104-owned-lineage-floor-review/PROOF.md @@ -23,6 +23,9 @@ 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 diff --git a/research/p104-owned-lineage-floor-review/README.md b/research/p104-owned-lineage-floor-review/README.md index 6ecf7a092b..48afe322ac 100644 --- a/research/p104-owned-lineage-floor-review/README.md +++ b/research/p104-owned-lineage-floor-review/README.md @@ -48,6 +48,25 @@ finite facts F1-F3 for root directions. Layer 4 (`--flats`) enumerates all 440,8 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 @@ -93,7 +112,7 @@ PR6030 and runs layers 3-4 (about 2 minutes). Markers: `PASS_P104_OWNED_LINEAGE_ - 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. -- No independent human or proof-kernel review is claimed. +- Lemma 1 is machine-checked in Lean (see Lean); the rest is not. No independent human review is claimed. ## Open next questions diff --git a/research/p104-owned-lineage-floor-review/lean/.gitignore b/research/p104-owned-lineage-floor-review/lean/.gitignore new file mode 100644 index 0000000000..01f8cdb637 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/lean/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/research/p104-owned-lineage-floor-review/lean/Lineage.lean b/research/p104-owned-lineage-floor-review/lean/Lineage.lean new file mode 100644 index 0000000000..3543a63eff --- /dev/null +++ b/research/p104-owned-lineage-floor-review/lean/Lineage.lean @@ -0,0 +1 @@ +import Lineage.Basic diff --git a/research/p104-owned-lineage-floor-review/lean/Lineage/Basic.lean b/research/p104-owned-lineage-floor-review/lean/Lineage/Basic.lean new file mode 100644 index 0000000000..293f8465a5 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/lean/Lineage/Basic.lean @@ -0,0 +1,160 @@ +import Mathlib + +/-! +# Owned-lineage factorization (P104, PR6170 P_M accounting) + +Abstract form of Lemma 1 of `PROOF.md`. A lineage has moves `1..t`. Move `l` gathers at +frame `G l` and lands at `G (l+1)` (SAME hand-offs), so the frames are antitone. Values live +in a field `K` (the rationals in the paper), frames are subspaces of an `F`-space `V` +(`F₂⁹` in the paper) with a bilinear pairing `B` (the F₂ inner product of port labels). + +* `val c w l` is the mover's port content after move `l`: + `val 0 = 0`, `val (l+1) = c (l+1) • val l + w (l+1)`. +* `hw` is P3a: content injected at move `k` lies on ports whose label is in `G k`. + It does not matter which register supplied it (a port, a helper or a live `X`). +* `hu` is R1: if move `l` delivers to `Y_j`, its landing lies in `p_j^⊥`. + +`factor` : on every non-orthogonal pair the lineage's delivery is `α j * β i`. +`rank_le` : the F-rank of the pairing on `supp α × supp β` is at most `dim G 1 - dim G (t+1)`. +-/ + +open Finset + +namespace Lineage + +variable {K : Type*} [Field K] + +/-- Content of the mover after move `l`. -/ +def val {ι : Type*} (c : ℕ → K) (w : ℕ → ι → K) : ℕ → ι → K + | 0 => fun _ => 0 + | l + 1 => fun i => c (l + 1) * val c w l i + w (l + 1) i + +/-- Product of the scalars `c 1 ⋯ c l`. -/ +def pr (c : ℕ → K) (l : ℕ) : K := ∏ k ∈ Icc 1 l, c k + +lemma pr_succ (c : ℕ → K) (l : ℕ) : pr c (l + 1) = pr c l * c (l + 1) := by + unfold pr + rw [prod_Icc_succ_top (by omega)] + +lemma pr_ne_zero {c : ℕ → K} (hc : ∀ k, c k ≠ 0) (l : ℕ) : pr c l ≠ 0 := + prod_ne_zero_iff.mpr fun k _ => hc k + +/-- Closed form of the content. -/ +lemma val_eq {ι : Type*} {c : ℕ → K} (hc : ∀ k, c k ≠ 0) (w : ℕ → ι → K) (l : ℕ) (i : ι) : + val c w l i = pr c l * ∑ k ∈ Icc 1 l, w k i / pr c k := by + induction l with + | zero => simp [val] + | succ l ih => + have h1 := pr_ne_zero hc l + have h2 := hc (l + 1) + show c (l + 1) * val c w l i + w (l + 1) i = _ + rw [ih, pr_succ, sum_Icc_succ_top (by omega), pr_succ] + field_simp + +variable {F : Type*} [Field F] {V : Type*} [AddCommGroup V] [Module F V] {ι : Type*} + +/-- **Lemma 1 (i)**: rank one on every non-orthogonal pair. -/ +theorem factor (G : ℕ → Submodule F V) (hG : Antitone G) (p : ι → V) + (B : V →ₗ[F] V →ₗ[F] F) (c : ℕ → K) (hc : ∀ k, c k ≠ 0) (w u : ℕ → ι → K) + (hw : ∀ k i, w k i ≠ 0 → p i ∈ G k) + (hu : ∀ l j, u l j ≠ 0 → ∀ x ∈ G (l + 1), B (p j) x = 0) (t : ℕ) : + ∀ i j, B (p j) (p i) ≠ 0 → + ∑ l ∈ Icc 1 t, u l j * val c w l i = + (∑ l ∈ Icc 1 t, u l j * pr c l) * (∑ k ∈ Icc 1 t, w k i / pr c k) := by + intro i j hji + rw [sum_mul] + refine sum_congr rfl fun l hl => ?_ + by_cases hul : u l j = 0 + · simp [hul] + rw [val_eq hc, mul_assoc] + congr 2 + have hlt : l ≤ t := (mem_Icc.mp hl).2 + refine sum_subset (Icc_subset_Icc le_rfl hlt) fun k hk hk' => ?_ + have hkl : l + 1 ≤ k := by + simp only [mem_Icc, not_and, not_le] at hk hk' + exact hk' hk.1 + by_contra hne + have hwk : w k i ≠ 0 := fun h => hne (by simp [h]) + exact hji (hu l j hul _ (hG hkl (hw k i hwk))) + +/-- **Lemma 1 (ii)**, source side: `β i ≠ 0` forces `p i ∈ G 1`. -/ +theorem beta_support (G : ℕ → Submodule F V) (hG : Antitone G) (p : ι → V) + (w : ℕ → ι → K) (pc : ℕ → K) (hw : ∀ k i, w k i ≠ 0 → p i ∈ G k) (t : ℕ) (i : ι) + (h : ∑ k ∈ Icc 1 t, w k i / pc k ≠ 0) : p i ∈ G 1 := by + obtain ⟨k, hk, hne⟩ := exists_ne_zero_of_sum_ne_zero h + have hwk : w k i ≠ 0 := fun h0 => hne (by simp [h0]) + exact hG (mem_Icc.mp hk).1 (hw k i hwk) + +/-- **Lemma 1 (ii)**, receiver side: `α j ≠ 0` forces `G (t+1) ⊆ p_j^⊥`. -/ +theorem alpha_support (G : ℕ → Submodule F V) (hG : Antitone G) (p : ι → V) + (B : V →ₗ[F] V →ₗ[F] F) (u : ℕ → ι → K) (pc : ℕ → K) + (hu : ∀ l j, u l j ≠ 0 → ∀ x ∈ G (l + 1), B (p j) x = 0) (t : ℕ) (j : ι) + (h : ∑ l ∈ Icc 1 t, u l j * pc l ≠ 0) : ∀ x ∈ G (t + 1), B (p j) x = 0 := by + obtain ⟨l, hl, hne⟩ := exists_ne_zero_of_sum_ne_zero h + have hul : u l j ≠ 0 := fun h0 => hne (by simp [h0]) + intro x hx + exact hu l j hul x (hG (by have := (mem_Icc.mp hl).2; omega) hx) + +/-- **Lemma 1 (iii)**: the pairing between ports in `G1` and ports whose hyperplane contains +`L ≤ G1` has rank at most `dim G1 - dim L`. -/ +theorem rank_le [FiniteDimensional F V] (G1 L : Submodule F V) (hL : L ≤ G1) (p : ι → V) + (B : V →ₗ[F] V →ₗ[F] F) (R A : Type*) [Fintype R] [Fintype A] (fR : R → ι) (fA : A → ι) + (hA : ∀ a, p (fA a) ∈ G1) (hR : ∀ r, ∀ x ∈ L, B (p (fR r)) x = 0) : + (Matrix.of fun (r : R) (a : A) => B (p (fR r)) (p (fA a))).rank + Module.finrank F L ≤ + Module.finrank F G1 := by + classical + set M := Matrix.of fun (r : R) (a : A) => B (p (fR r)) (p (fA a)) + -- T : G1 → (R → F), x ↦ (B (p r) x)_r + let T : G1 →ₗ[F] (R → F) := LinearMap.pi fun r => (B (p (fR r))).comp G1.subtype + have hspan : LinearMap.range M.mulVecLin ≤ LinearMap.range T := by + rw [Matrix.range_mulVecLin, Submodule.span_le] + rintro _ ⟨a, rfl⟩ + refine ⟨⟨p (fA a), hA a⟩, ?_⟩ + ext r + simp [T, M] + have hker : Submodule.comap G1.subtype L ≤ LinearMap.ker T := by + intro x hx + simp only [LinearMap.mem_ker, T] + ext r + simpa using hR r x hx + have e : Module.finrank F (Submodule.comap G1.subtype L) = Module.finrank F L := + (Submodule.comapSubtypeEquivOfLe hL).finrank_eq + have h1 : M.rank ≤ Module.finrank F (LinearMap.range T) := by + unfold Matrix.rank + exact Submodule.finrank_mono hspan + have h2 := LinearMap.finrank_range_add_finrank_ker T + have h3 := Submodule.finrank_mono hker + omega + + +/-- **Lemma 1 (iii), assembled**: with `α, β` the vectors of `factor`, the pairing on +`supp α × supp β` has rank at most `dim G 1 - dim G (t+1)`, the lineage's owned paid. -/ +theorem lineage_cost [FiniteDimensional F V] [Fintype ι] [DecidableEq K] + (G : ℕ → Submodule F V) (hG : Antitone G) (p : ι → V) + (B : V →ₗ[F] V →ₗ[F] F) (c : ℕ → K) (w u : ℕ → ι → K) + (hw : ∀ k i, w k i ≠ 0 → p i ∈ G k) + (hu : ∀ l j, u l j ≠ 0 → ∀ x ∈ G (l + 1), B (p j) x = 0) (t : ℕ) : + (Matrix.of fun (r : {j // ∑ l ∈ Icc 1 t, u l j * pr c l ≠ 0}) + (a : {i // ∑ k ∈ Icc 1 t, w k i / pr c k ≠ 0}) => B (p r.1) (p a.1)).rank + + Module.finrank F (G (t + 1)) ≤ Module.finrank F (G 1) := by + classical + exact rank_le (G 1) (G (t + 1)) (hG (by omega)) p B _ _ Subtype.val Subtype.val + (fun a => beta_support G hG p w (pr c) hw t a.1 a.2) + (fun r => alpha_support G hG p B u (pr c) hu t r.1 r.2) + +/-- Telescoping: the paid of a SAME lineage is `dim G 1 - dim G (t+1)` (R4). -/ +theorem paid_telescope [FiniteDimensional F V] (G : ℕ → Submodule F V) (t : ℕ) : + ∑ l ∈ Icc 1 t, ((Module.finrank F (G l) : ℤ) - Module.finrank F (G (l + 1))) = + (Module.finrank F (G 1) : ℤ) - Module.finrank F (G (t + 1)) := by + induction t with + | zero => simp + | succ t ih => rw [sum_Icc_succ_top (by omega), ih]; ring + +end Lineage + +#print axioms Lineage.factor +#print axioms Lineage.rank_le +#print axioms Lineage.beta_support +#print axioms Lineage.alpha_support +#print axioms Lineage.paid_telescope +#print axioms Lineage.lineage_cost diff --git a/research/p104-owned-lineage-floor-review/lean/lake-manifest.json b/research/p104-owned-lineage-floor-review/lean/lake-manifest.json new file mode 100644 index 0000000000..a9d9cd1a47 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/lean/lake-manifest.json @@ -0,0 +1,117 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "55b7917b472489c7c56a0fa6393af05cfd536599", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "55b7917b472489c7c56a0fa6393af05cfd536599", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0498c7c070c143a3bf7379f4d99a2c63bb9d9715", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "57d3325be72a842920813bcb40f96a6f7393c185", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2c810760f0a0c4536b397dbe30ca9b2f2f467366", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0-rc1", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "NetCode", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/research/p104-owned-lineage-floor-review/lean/lakefile.toml b/research/p104-owned-lineage-floor-review/lean/lakefile.toml new file mode 100644 index 0000000000..94b67c6350 --- /dev/null +++ b/research/p104-owned-lineage-floor-review/lean/lakefile.toml @@ -0,0 +1,10 @@ +name = "Lineage" +defaultTargets = ["Lineage"] + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "55b7917b472489c7c56a0fa6393af05cfd536599" + +[[lean_lib]] +name = "Lineage" diff --git a/research/p104-owned-lineage-floor-review/lean/lean-toolchain b/research/p104-owned-lineage-floor-review/lean/lean-toolchain new file mode 100644 index 0000000000..fd85b262bf --- /dev/null +++ b/research/p104-owned-lineage-floor-review/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.0-rc1