diff --git a/research/complex-frame-pair-decoders/CLAIM.md b/research/complex-frame-pair-decoders/CLAIM.md new file mode 100644 index 0000000000..763c771c98 --- /dev/null +++ b/research/complex-frame-pair-decoders/CLAIM.md @@ -0,0 +1,36 @@ +# Local sprint claim (no pinned coordination issue exists) + +- Recorded: 2026-10-13T14:55Z (approx.) +- Track: 40-49, structural decoder research. Assignment seed **47**, drawn once with + `python -c "import secrets; print(secrets.randbelow(100))"` (OS randomness) at 2026-10-13T14:12:28Z. +- Base commit: `47481c89fd30a43f8f882eb4b391e89c29273fd0` (main, "Record publication and merge + confirmation for all eighteen PRs"). Selected kappa 0.001661957774647029 (PR890, complex-bound). +- Object: exact 8-term complex decoders (D = R A, T = R A^-T) in PR717's B14 decoder model + (E8 root lines, labels in F2^9, Theorem C pairing-rank cost), on punctures of the 120 lines. + This is the copied-information cost of the binding complex supplier (P112, cst 64). +- Question: what mechanism produces PR717 D3's P111 = 63 and P104 = 56 hits, which punctures + attain it, and what is the copy-ratio floor cst/v for exact 8-term decoders below a stated + puncture threshold? +- Method: pairing-rank linear algebra over F2^9; exhaustive violator census over the 8 + W(E8) hyperplane-flat types and all 511 hyperplanes / 43,435 codimension-2 subspaces of F2^9; + exhaustive frame-pair census; exact integer verification of explicit decoders; favorable-budget + pricing on the selected T21 profile with the pinned moment engine, including the bit-supplier cap. +- Candidates considered and not chosen: (1) mixed-beta n >= 9 decoders on P112 (PR717 open problem 1; + SAT attempts already killed, high risk); (2) non-B_K stage schedules (format-limits "not covered"; + legality not modelable without new spec work); (3) a further bit-side puncture census (crowded: + #631, #761, #875, #939, and the bit side does not bind). +- Expected deliverable: research note / scoped structural result. No kappa claim. +- Expected finish: same day. + +## Result (2026-10-13) + +- Delivered as `research/complex-frame-pair-decoders/` (research note / scoped structural result, no kappa claim). +- Mechanism: a term costs 7 exactly when its row and column normals are an odd root pair with both lines + punctured; PR717's D3 hits all have this form. +- Theorem (exact 8-term decoders, punctures p <= 24): cst >= 72 - p for p <= 15 and cst >= 56 for p <= 24, + both attained at every p; copy ratio >= 7/13, equality only at p = 16 (frame pairs; 896 of 1260 frames). +- Favorable budget (PR717 P1 knobs, pinned engines), first on T21 and after rebase on T37: P111 +0.67% b; + P104 +5.51% b, capped by the PR589 bit supplier at kappa 0.001730427469823602 (+4.12%). +- Rebased at 15:15Z onto bbc600db2fc15007b7c914f4f2b2ed55fa909c87 (T37 selected, PR942). +- Reproduce: `python3 -I -B research/complex-frame-pair-decoders/verify.py` (48 PASS, ~30 s, stdlib only). +- Submitted: https://github.com/CrocSwap/integer-mult-bounds/pull/968 (status: research note / scoped structural result). diff --git a/research/complex-frame-pair-decoders/PROOF.md b/research/complex-frame-pair-decoders/PROOF.md new file mode 100644 index 0000000000..889f3a653e --- /dev/null +++ b/research/complex-frame-pair-decoders/PROOF.md @@ -0,0 +1,195 @@ +# Exact 8-term copy-cost floor on punctured complex E8 units + +Every finite fact cited as **(Fk)** is checked by `verify.py`, using exact integer and F2 +arithmetic. The rest is written argument. One standard theorem is cited rather than recomputed +(see (F6)). + +## 1. Model + +This is PR717's B14 decoder model, in the D2/D3 scope (DreamingOfClouds, +`research/format-limits-2/s5-6-decoders-spec/checks/e8model.py` at `4a97676`). Take the 120 root +lines of E8 with representatives r_i of norm 2, and let G_ij = ⟨r_i, r_j⟩. A **puncture** P is a set +of p lines, and the **live** lines are the rest. Each line has a label u_i ∈ F2^9 with a symmetric +form S9. PR717's construction gives + + S9(u_i, u_j) = (⟨r_i, r_j⟩ + 1) mod 2, (1) + +because the first eight label coordinates carry the E8 form mod 2 and the ninth is a unit +coordinate equal to 1 on every line. `verify.py` uses (1) directly as its definition. + +An **exact 8-term decoder** is a pair of real matrices D and T, each of size live × 8, with +DTᵀ = 2G on all live pairs. Term k costs ρ_k: the F2 rank of the label pairing between its row +support R_k = {i : D_ik ≠ 0} and its column support A_k = {j : T_jk ≠ 0}. The copy cost is +cst = Σ_k ρ_k. On P112, the coordinate decoder has cst = 64. That is the value carried by the +selected complex supplier (T37 deficit 37·(8·112 − 9·64) = 11840). + +**Normal form.** Suppose the live lines span R^8. This always holds when p ≤ 56, because no +hyperplane contains more than 63 lines. Then rank 2G_live = 8. So D and T have rank 8, and +their column spaces equal that of R, the live-root matrix. Hence D = RA and T = RB with +ABᵀ = 2I. Write a_k and b_k for the columns of A and B. Then ⟨a_k, b_l⟩ = 2δ_kl, +R_k = live ∩ C(a_k) and A_k = live ∩ C(b_k), where C(a) is the set of lines not orthogonal to a. +Two consequences: + +- a_k ∦ b_l for k ≠ l; +- the a_k are pairwise non-parallel, and so are the b_k. + +Conversely, any pair of dual bases gives an exact decoder on every live set. + +## 2. Linear algebra over F2 + +(F0) The 120 × 120 pairing matrix (1) has F2 rank 9, and its 120 rows are distinct. So the labels +span a 9-dimensional space Λ on which S9 is nondegenerate. Distinct lines have distinct label +functionals λ_i = S9(u_i, ·). + +For a set X of lines, let V_X = span{u_i : i ∈ X}. The pairing rank satisfies + + ρ(X, Y) = dim V_X − dim(V_X ∩ V_Y^⊥) ≥ dim V_X + dim V_Y − 9. (2) + +For a root α, let H_α = ker λ_α. If V_X = H_α and V_Y = H_β, then H_β^⊥ = span(u_β), so + + ρ = 8 − [u_β ∈ H_α] = 8 − [⟨α, β⟩ odd]. (3) + +In particular α = β gives ρ = 8, because ⟨α, α⟩ = 2. + +**Violators.** dim V_X ≤ 8 exactly when some nonzero functional λ vanishes on X. Equivalently, +X avoids Viol(λ) = {i : λ(u_i) = 1}. So a side with normal a can be brought to an 8-dimensional +span only by puncturing all of Viol(λ) ∩ C(a), for some λ. Getting dim ≤ 7 requires puncturing +(Viol(λ1) ∪ Viol(λ2)) ∩ C(a), for some independent pair λ1, λ2. + +## 3. The finite census + +The pairing (1) depends only on inner products, so it is W(E8)-invariant. Every hyperplane flat +of the E8 arrangement is W-conjugate to one of the eight standard flats ω_i^⊥, where ω_i are the +fundamental weights (Bourbaki, *Lie Groups*, Ch. V §3; Orlik–Solomon). **(F6)** This is the one +premise that is cited rather than computed. + +For each type, `verify.py` checks all 511 hyperplanes and all 130,305 pairs of functionals. The +table gives |C(ω)|, the smallest and second-smallest |Viol(λ) ∩ C(ω)|, and the codimension-2 +minimum π7: + +| flat type | flat lines | C | min | next | π7 | +|---|---|---|---|---|---| +| E7 (root normal) | 63 | 57 | **1** | 24 | **25** | +| D7 | 42 | 78 | **14** | 34 | 42 | +| E6+A1 | 37 | 83 | 27 | 28 | 51 | +| A7 | 28 | 92 | 28 | 35 | 56 | +| D5+A2 | 23 | 97 | 33 | 41 | 61 | +| A6+A1 | 22 | 98 | 35 | 35 | 62 | +| A4+A3 | 16 | 104 | 40 | 43 | 68 | +| A4+A2+A1 | 14 | 106 | 43 | 43 | 70 | + +The checked facts: + +- **(F1)** Every C(ω) has a label span of dimension 9. +- **(F2)** This is checked for all 120 roots directly. For a root α, the unique 1-line violator + set is {α}, through λ_α. Every other λ needs ≥ 24 lines. +- **(F3)** The W-orbit of the D7 normal has 1080 directions, enumerated by reflections. Each has + a unique minimizing λ_ω with 14 violators, and the next has ≥ 34. Any two distinct D7 directions + have violator sets whose union is ≥ 21. No λ_ω equals a root functional λ_α. +- **(F4)** Every other hyperplane type needs at least 27 violators. +- **(F5)** Over all types, π7 ≥ 25. + +**Lemma 1 (non-hyperplane normals).** Suppose the roots orthogonal to a span at most 6 +dimensions. Then |Viol(λ) ∩ C(a)| ≥ 16 for every λ, and π7(a) ≥ 25. + +*Proof.* Let U be the span of the roots orthogonal to a, so dim U ≤ 6. Extend a root basis of U +by roots to a root basis of R^8. Dropping two different added roots gives two distinct +root-spanned hyperplanes H1 and H2, both containing U. Their normals ω1 and ω2 are hyperplane-flat +normals with C(ω_i) ⊆ C(a). So + + Viol(λ) ∩ C(a) ⊇ (Viol(λ) ∩ C(ω1)) ∪ (Viol(λ) ∩ C(ω2)). + +Suppose this set had at most 15 lines. Then, by the census, each (ω_i, λ) would be a pair +(root α_i, λ_{α_i}) or (D7 normal, its λ_ω). With the same λ for both, there are three cases: + +- two roots: λ_{α1} = λ_{α2} forces α1 = α2 by (F0), so H1 = H2; +- root and D7: impossible, since no λ_ω is a root functional (F3); +- two D7 normals: their violator sets have union ≥ 21 (F3). + +Each case is a contradiction. For π7, one containing hyperplane is enough, by (F5). ∎ + +## 4. Theorem + +Let P be a puncture with p = |P| ≤ 24, and let (A, B) be an exact 8-term decoder on the live +lines. + +**(a)** cst ≥ 56. + +**(b)** If p ≤ 15, then cst ≥ 72 − p. + +**(c)** Hence cst/v ≥ 7/13 for every p ≤ 24, where v = 120 − p. Equality holds exactly when +p = 16 and cst = 56. Both bounds are attained at every p: cst_min(p) = 72 − p for 0 ≤ p ≤ 16, and +cst_min(p) = 56 for 16 ≤ p ≤ 24. + +*Proof of (a).* By (F5) and Lemma 1, bringing any side down to a span of dimension ≤ 7 needs at +least 25 > p punctures. So every live support spans at least 8 dimensions, and (2) gives ρ_k ≥ 7. + +*Proof of (b).* Call a side **reduced** if its live label span has dimension 8. By (a), every +unreduced side has dimension 9. By (2), s_k := 9 − ρ_k is at most the number of reduced sides of +term k. A reduced side with normal a needs some λ with |Viol(λ) ∩ C(a)| ≤ p ≤ 15. By (F2)–(F4) +and Lemma 1, only two kinds qualify: + +- **(i)** a is a root α, with λ = λ_α, and α ∈ P (a *self-line* reduction); +- **(ii)** a is a D7 normal ω, with its 14-line set ⊆ P. + +By (F3), case (ii) can occur for at most one direction ω, because p < 21. + +*If (ii) occurs:* By the normal form, ω is not a column normal of any term other than its own. +Transposing (D ↔ T) preserves exactness and costs, so assume ω = a_1. For l ≠ 1, ⟨a_1, b_l⟩ = 0, +so b_l ⊥ ω. A reduced column side l ≠ 1 is therefore a self-line β_l ∉ C(ω). Its line lies in +P minus the 14-line set, which has at most p − 14 ≤ 1 lines. The β_l are distinct, so at most one +of these seven column sides is reduced. That gives Σ s_k ≤ 16 − 6 = 10 < 14 ≤ p. + +*If (ii) does not occur:* Every reduced side is a self-line reduction. Lines from different +terms are distinct: the a's are distinct, the b's are distinct, and a_k ∦ b_l for k ≠ l. Term k +uses two distinct lines unless a_k ∥ b_k. In that case ρ_k = 8 by (3), so s_k = 1, the number of +lines it uses. So Σ s_k ≤ |P| = p in every case, and cst = 72 − Σ s_k ≥ 72 − p. + +*Proof of (c).* For p ≤ 15: + + 13(72 − p) − 7(120 − p) = 96 − 6p > 0. + +For 16 ≤ p ≤ 24, cst/v ≥ 56/(120 − p) ≥ 56/104. `verify.py` (section E) builds an exact +decoder attaining max(72 − p, 56) for every p = 0..24: + +- for p ≤ 8: the coordinate decoder with p frame lines punctured; +- for 8 < p ≤ 16: a frame-pair decoder (§5) with p − 8 partner lines punctured; +- for p > 16: the frame-pair decoder with p − 16 further lines punctured. Spans cannot fall below + 8 dimensions, by (a). ∎ + +## 5. Frame-pair decoders + +Let F0 be the coordinate frame and F1 another frame, i.e. 8 mutually orthogonal lines disjoint +from F0. A **frame-pair decoder** takes eight row normals: S ⊆ F0 and T ⊆ F1, with |S| + |T| = 8. +Each row normal is paired with a column partner from the other frame, chosen so that: + +- the partner is non-orthogonal to its own row normal; +- the partner is orthogonal to every other row normal. + +Lines from two distinct frames are 0 or ±1 apart, so every pair is odd. The 16 lines are exactly +F0 ∪ F1, so on P = F0 ∪ F1 every term has both self-lines punctured, and (3) gives ρ = 7. + +**(F7)** There are 1260 frames inside P112. Of these: + +- 896 admit frame-pair decoders, with exactly 8 each. All 7168 decoders satisfy AᵀB = 2I and have + eight cost-7 terms; one is also rechecked entry by entry. +- 364 admit none. These are the frames in which some pair of F1 lines shares four F0-neighbours. + They form two relative positions: 336 connected and 28 of type K4,4 ∪ K4,4. + +PR717 D3 drew its P104 clique at random. It is an admissible frame of this kind. Its recorded +decoder, along with both recorded P111 decoders, has exactly the root-pair structure. Each cost-7 +term is an odd pair of root normals whose two lines are both punctured, and no other term is. +The per-term costs computed from (1) equal those recorded by PR717's own label code. + +## 6. Scope + +The following are **not** covered: + +- decoders with n ≥ 9 terms; +- decoders that are exact only on PR717's E-graph and fix the odd entries with cost-0 terms. This + is the scope of D1(a), whose mixed-β open problem remains open; +- punctures of more than 24 lines; +- whether a word can realize the asymmetric (α ≠ β) centres. PR717 recorded, without shipping, a + negative buildability price for these decoders. + +Section G of `verify.py` gives a favorable budget only, not a construction. diff --git a/research/complex-frame-pair-decoders/README.md b/research/complex-frame-pair-decoders/README.md new file mode 100644 index 0000000000..be5bbbee8e --- /dev/null +++ b/research/complex-frame-pair-decoders/README.md @@ -0,0 +1,136 @@ +# Frame-pair decoders: the exact 8-term copy-cost floor for punctured complex units (no new κ) + +**Status: research note and scoped structural result. No κ claim, no new supplier.** The selected +κ = 0.001661960547713947 (PR942, T37) and every existing file are unchanged. + +## What this establishes + +The selected complex supplier is the binding side. Its copied-information cost is the decoder +constant, cst = 64 on 112 ports, inside the deficit 37·(8·112 − 9·64) = 11840 of T37. PR717 (DreamingOfClouds, +open) found two cheaper non-star decoders by random walks: cst 63 on single-line P111 punctures, and +cst 56 on one P104. This package explains that mechanism, bounds it, and prices it. It works in +PR717's own B14 model, for exact 8-term decoders (D = RA, T = R·2A^{-T}). + +1. **Mechanism.** Take a term whose row and column normals are roots α and β with ⟨α, β⟩ odd. + If both lines are punctured, it costs exactly 7 (for p ≤ 24). If either line is live, or if + α = β (the coordinate decoder), it costs 8. The reason is short: the labels of N(α) span the + hyperplane H_α = u_α^⊥ in F2^9, the line's own label lies outside it, and the pairing H_α × H_β + has rank 8 − [⟨α, β⟩ odd]. All three vendored PR717 hits have exactly this + structure. Every cost-7 term is an odd root pair with both lines punctured, and the per-term costs + agree with PR717's recorded values. +2. **Construction family.** Take a second frame F1. If there is a dual root basis on F0 ∪ F1 in which + every term pairs a line of F0 with a line of F1, the 16-line puncture P104 = P120 − F0 − F1 has + cst 56. A complete census of the 1260 frames inside P112 finds: + - **896** frames admit such decoders, with exactly 8 each; all 7168 are exact with eight cost-7 + terms; + - **364** admit none. In these, some pair of F1 lines shares four F0-neighbours. + + PR717's randomly drawn P104 clique is one of the 896. +3. **Floor (theorem, finite census plus written proof).** For every puncture of p ≤ 24 lines, every + exact 8-term decoder has + + cst ≥ 72 − p (p ≤ 15), cst ≥ 56 (p ≤ 24), + + and both bounds are attained at every p. Hence the copy ratio satisfies **cst/v ≥ 7/13** through 24 + punctures, with equality only at p = 16, cst = 56. The shipped P112 has 4/7. So PR717's P104 is + ratio-optimal in this class, and its P111 hits are cost-optimal among 9-line punctures. The + P112 = 64 floor is re-derived for exact 8-term decoders by a different argument. +4. **Favorable budget on the selected frontier.** These numbers transport PR717's P1 knob model to the + selected T37 profile and price it with the same pinned moment and outer engines as the selected + record: + - P111: b rises 0.67%, giving κ 0.001673104139787043. + - P104: b rises 5.51%, which takes it **above the bit supplier**. κ is then capped by PR589 at + **0.001730427469823602**, 4.12% above the selected value. That cap applies to *any* + complex-only change. + + So a realization of the asymmetric (α ≠ β) centres improves κ only if its extra costs lower b by + less than the 5.51% gain, measured against the selected b. It reaches the bit cap only if they lower + b by less than about 1.3%, since the P104 knob value of b is 1.33% above the bit c. PR717 recorded, + but did not ship, an estimate of −0.1% to −10% net b for building these decoders. + +Searches for cheaper exact 8-term complex decoders through deeper punctures (p ≤ 24) are closed by +item 3. The remaining open directions are in the Scope section below. + +## Reproduce + +From the repository root, Python 3.10+, standard library only, assertions enabled (about 30 s): + +```sh +python3 -I -B research/complex-frame-pair-decoders/verify.py +``` + +Expected: 48 `PASS` check lines, no `FAIL`, exit status 0, and the final line + +```text +PASS_COMPLEX_FRAME_PAIR_DECODERS: types 8; D7 orbit 1080; frames 1260 (admissible 896); chain p=0..24; P104 7/13; bit cap kappa 0.001730427469823602; controls 6 +``` + +Add `--out /new/file.json` to write the complete certificate: census, chain, hit replay, prices and +log. + +## What `verify.py` checks + +| section | content | +|---|---| +| A | 120 lines; the pairing (⟨r_i, r_j⟩ + 1) mod 2 has F2 rank 9 with distinct rows. This is PR717's S9 label pairing, computed without PR717's coordinates. | +| B | All 8 W(E8) hyperplane-flat types × all 511 hyperplanes and 130,305 codimension-2 pairs. Minimum violators to reach an 8-dim span: E7 (root) 1 (its own line), D7 14, all others ≥ 27; a root by any other hyperplane ≥ 24. A 7-dim span needs ≥ 25. The root fact is checked for all 120 roots directly. | +| C | The 1080-direction D7 orbit: unique 14-line sets, pairwise unions ≥ 21, none equal to a root functional. | +| D | All 1260 frames in P112 and all splits S ⊆ F0, T ⊆ F1: 896 × 8 decoders, each with AᵀB = 2I and eight cost-7 terms, plus one full 104 × 104 entrywise check; 364 frames have no solution. The three relative positions are reported. | +| E | An explicit exact decoder for every p = 0..24 with cst = max(72 − p, 56), and full-rank live sets. | +| F | Replay of PR717's P104 and two P111 decoders: exactness, root-pair structure of every cost-7 term, and agreement with PR717's recorded per-term costs. | +| G | Hash-pinned engines (the same hashes as the selected ASSEMBLY.json inputs). Gate: the selected record (T37, 37 replicas, inferred from the deficit identity) reproduces b and κ exactly. Then the P111 and P104 knob scenarios, two-engine moment checks, outer κ with the next-grid/η/β controls, and the PR589 cap. | +| H | Negative controls: a mutated decoder loses exactness; restoring one self-line gives 57 = 72 − 15; the even coordinate decoder on the same P104 stays at 64; the 364 inadmissible frames; swapped partners; a 25-line set does reach a 7-dim span, so the threshold is sharp. | + +The theorem's lower-bound argument is in [PROOF.md](PROOF.md). The finite facts it uses are +sections A–C. One step is cited rather than recomputed: the classical fact that every hyperplane +flat of a Weyl arrangement is conjugate to a standard one (8 types for E8). The D7 orbit, which is +the only non-root type below the thresholds, is enumerated directly. + +## Scope and inherited obligations + +- **Covered.** Decoders with exactly 8 terms that are exact on all live pairs. This is the D2/D3 + scope of PR717. The census does not depend on which lines are punctured, for any puncture of at + most 24 of the 120 lines. +- **Not covered: decoder classes.** + - n ≥ 9 terms, including PR717's open mixed-β problem on P112 (the PR845 family excluded one such + class); + - decoders exact only on the E-graph, with cost-0 terms for the odd entries; + - punctures of more than 24 lines; + - labels outside this model. +- **Not covered: construction.** No word is built. The knob pricing is a favorable budget, not a + supplier. Realizing asymmetric centres raises unresolved questions: centre reads, frame legality, + phase frames and restoration. PR717 recorded unpaired-centre parity costs (≥ 78) and 96 pair-split + conflicts, which are not re-derived here. The knob model removes a port as one modal source and + target climb per call plus nine idle rank-48 children per replica, exactly as in PR717 P1. +- **Inherited conditions.** All of the selected record's conditions are unchanged: all-size + compiler, common-label and mutable-source realization, whole-call hosting, precision/tape, + analytic transfer, and the bit supplier's H1–H5 interface. +- **Not a formal proof.** Finite replay is not a formal proof of the multiplication theorem. The + written lower-bound proof has not had independent human review. + +## Provenance, credit and overlap + +- **Base and assignment.** Base commit `bbc600db2fc15007b7c914f4f2b2ed55fa909c87`. The work started at + `47481c89` (PR890 T21 selected) and was rebased when T37 was published; the theorem is unaffected, + and on T21 the P111 knob value was κ 0.001673101338175894. Sprint track 40–49 (structural decoder + research), assignment seed **47** from OS randomness. See + [CLAIM.md](CLAIM.md). No pinned coordination issue existed, so the claim is local. +- **DreamingOfClouds, PR717** (open, head `4a97676`). The B14 model, the D1–D3 findings that this + package explains and bounds, and the P1 knob calculus. Three decoder files are vendored byte for + byte with git-blob and SHA-256 pins in [SOURCES.json](SOURCES.json) (Apache-2.0). +- **Joel Pulikkan / GamingPuzzled, PR620**, merged as `research/e8-decoder-floors-and-cold14-notes`. + The complex frame decoder of cost 64 and the star-floor census. +- **DreamingOfClouds, PR595** (merged, `research/format-limits*`). The (Dfc) identity, the format + ceiling and the copy-charge prices. +- **PR845.** The one-added-total exclusion on P112, a different class. +- **icekylinx, PR514/P112.** The 112-port puncture. +- **The selected T37/T21 chain.** Jonathan Capalbo (PR942), Chafik Boukhalfa (PR890), Jeremy Kothe + (PR869/870), Hao Yan (PR858), DreamingOfClouds (PR589) and eumemic (PR555). This package only reads their pinned pricing + inputs. +- **Overlap.** Bit-side puncture and pairing-rank results (#631, #761, #875, #939) and the + Gaussian/Eisenstein copy floors (#738, #770, #798, #868, #888) concern other units or the + non-binding bit side. Before submission, no open PR addressed exact 8-term complex decoders under + punctures. +- **AI assistance and license.** Prepared with substantial assistance from Claude Opus 5.5 + (Anthropic) via Claude Code: the research, proof, implementation and documentation. Submitted by + the account holder. Apache-2.0. diff --git a/research/complex-frame-pair-decoders/SOURCES.json b/research/complex-frame-pair-decoders/SOURCES.json new file mode 100644 index 0000000000..2adbb52d52 --- /dev/null +++ b/research/complex-frame-pair-decoders/SOURCES.json @@ -0,0 +1,49 @@ +{ + "base_commit": "bbc600db2fc15007b7c914f4f2b2ed55fa909c87", + "selected_record": { + "path": "certificates/selected-result.json", + "kappa": "1661960547713947/1000000000000000000", + "certificate": "research/community-frontier942-audit/ASSEMBLY.json", + "certificate_sha256": "4b2894956e594e408e111d806c842f2ed2c32aefcadff93fad69ff0b46f1991a" + }, + "pricing_inputs": { + "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c", + "research/complex-t21-owners/vendor/pr870/independent/price_profile_t16.py": "53f8e62dcf27bee032c1bee0245d126a9c8a12ebcf24f6aaff65ea3122fffe29", + "research/complex-t21-owners/vendor/pr870/inputs/PR589-EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "research/community-frontier942-audit/ASSEMBLY.json": "4b2894956e594e408e111d806c842f2ed2c32aefcadff93fad69ff0b46f1991a" + }, + "pricing_input_notes": "The three engine hashes and the PR589 record hash equal the input_sha256 entries of the selected frontier942 (T37) ASSEMBLY.json. price_profile_t16.py is the unchanged outer driver used by research/complex-t21-owners/price.py. The package was first priced at 47481c89 on the PR890 T21 profile; it was rebased when T37 was selected and now prices the current selection.", + "vendored": { + "inputs/pr717/P104_HIT_flip_3a.txt": { + "source": "research/format-limits-2/s5-6-decoders-spec/inputs/local-hits/P104/HIT_flip_3a.txt", + "pr": 717, + "head": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "git_blob": "458ddb13dcf73ed031ffb96d9df149c994c7e4ee", + "sha256": "8e0178db02c14e1b29058cdbdbd50aac22f2b55a1ba21dc82f417610c9932526" + }, + "inputs/pr717/P111_HIT_g0.txt": { + "source": "research/format-limits-2/s5-6-decoders-spec/inputs/local-hits/P111/HIT_g0.txt", + "pr": 717, + "head": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "git_blob": "05b86974fed125e52c1f7417467716d5e083316b", + "sha256": "c06d83ede44258b7250fe1df62a82011687f704c7f879ce4c91040ebbe2ef6b4" + }, + "inputs/pr717/P111_HIT_g111.txt": { + "source": "research/format-limits-2/s5-6-decoders-spec/inputs/local-hits/P111/HIT_g111.txt", + "pr": 717, + "head": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "git_blob": "21930b350685204aa36cd64bc224dc24eb877c2f", + "sha256": "8d5528362385dfc0c19cda625e5b2894d777d9405fc167c4c6723e99baa8db56" + } + }, + "vendored_license": "PR717 (DreamingOfClouds) is Apache-2.0; the three decoder files are copied byte for byte. Line indices in them use PR717's e8model P112 ordering; verify.py rebuilds that ordering as an adapter (same root enumeration and representative rule) and does not import e8model.", + "model_reference": { + "pr": 717, + "file": "research/format-limits-2/s5-6-decoders-spec/checks/e8model.py", + "head": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "used_for": "definition only (labels in F2^9 with form Gb mod 2 plus a unit ninth coordinate, so pairing = ( + 1) mod 2); not imported" + }, + "original_base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0" +} diff --git a/research/complex-frame-pair-decoders/inputs/pr717/P104_HIT_flip_3a.txt b/research/complex-frame-pair-decoders/inputs/pr717/P104_HIT_flip_3a.txt new file mode 100644 index 0000000000..458ddb13dc --- /dev/null +++ b/research/complex-frame-pair-decoders/inputs/pr717/P104_HIT_flip_3a.txt @@ -0,0 +1,26 @@ +cost 56 n 8 NP 104 +D(cols) +term 0 cost 7 + d: 1 1 1 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 + t: 0 2 0 2 2 0 2 0 2 0 2 -2 0 -2 0 -2 0 -2 0 -2 -2 0 -2 0 -2 0 -2 -2 0 0 -2 0 -2 0 -2 -2 0 2 0 0 2 2 0 2 0 0 0 -2 -2 -2 -2 2 0 0 0 0 0 0 -2 2 0 0 0 0 0 -2 2 2 2 0 2 0 0 0 2 0 0 0 0 0 0 -2 2 2 2 0 2 0 0 2 2 2 0 2 0 0 0 2 2 2 2 2 2 0 +term 1 cost 7 + d: 0 2 2 0 2 0 0 2 2 2 0 0 2 2 2 0 0 2 2 0 2 0 -2 -2 0 0 -2 0 -2 2 0 0 2 2 0 2 0 2 0 2 0 0 -2 -2 2 0 2 2 0 2 0 0 0 2 0 0 -2 0 0 2 2 2 2 0 2 2 2 0 2 2 0 0 2 0 0 0 2 0 0 -2 0 0 0 -2 0 0 -2 -2 -2 2 0 2 2 0 0 2 0 0 2 0 0 -2 0 0 + t: 0 0 0 0 1 -1 -1 1 0 0 0 0 0 0 1 -1 -1 1 0 0 0 0 -1 -1 1 0 0 0 0 1 -1 -1 1 0 0 0 0 1 1 1 1 -1 -1 -1 0 0 1 1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 1 1 -1 -1 0 0 0 1 1 -1 -1 0 0 +term 2 cost 7 + d: 0 0 2 -2 0 0 0 0 0 0 0 -2 -2 0 -2 -2 -2 -2 -2 -2 -2 -2 0 0 0 0 0 0 0 2 2 2 2 2 2 2 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -2 -2 -2 -2 -2 -2 -2 -2 0 0 0 0 0 0 0 -2 -2 -2 -2 -2 -2 -2 -2 2 2 2 2 2 2 2 2 0 0 0 0 0 0 0 2 2 2 2 2 2 2 2 0 0 0 0 0 0 0 + t: 1 -1 1 -1 0 0 0 0 0 0 0 1 -1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 +term 3 cost 7 + d: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + t: 2 0 2 0 0 2 2 0 2 0 2 2 0 2 0 2 2 0 2 0 0 2 2 2 0 2 0 0 2 0 2 2 0 2 0 0 2 0 -2 -2 0 2 0 2 2 2 2 0 2 2 2 2 0 0 0 2 2 2 0 2 0 0 2 2 2 0 0 0 0 -2 2 0 0 0 2 0 0 0 2 2 2 0 0 0 0 -2 2 0 0 0 0 0 -2 2 0 0 0 -2 -2 -2 0 0 0 -2 +term 4 cost 7 + d: 0 0 0 0 0 0 0 0 1 1 -1 0 0 0 0 0 0 0 1 -1 1 -1 0 0 0 1 -1 1 -1 0 0 0 0 1 -1 1 -1 1 -1 1 -1 1 -1 -1 1 -1 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 0 0 -1 1 -1 0 0 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 1 -1 0 0 0 0 -1 1 -1 0 0 0 0 1 -1 0 1 -1 1 -1 0 0 + t: 0 0 0 0 0 0 2 -2 0 2 -2 0 0 0 0 0 2 -2 0 0 2 -2 0 2 -2 0 0 2 -2 0 0 2 -2 0 0 2 -2 0 0 2 -2 2 2 0 2 0 -2 0 2 0 -2 0 2 0 -2 2 0 -2 0 0 2 -2 2 0 -2 0 2 0 -2 0 0 2 0 -2 0 2 0 -2 2 0 -2 0 2 0 -2 0 0 2 -2 2 0 -2 0 0 2 0 -2 2 0 -2 2 0 -2 0 +term 5 cost 7 + d: 2 2 2 2 2 2 2 2 0 2 2 0 0 0 0 0 0 0 -2 2 0 0 0 0 0 -2 2 0 0 0 0 0 0 -2 2 0 0 -2 2 0 0 -2 2 0 0 2 0 2 2 0 2 0 2 0 2 0 2 0 2 0 2 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 2 0 2 0 2 0 2 0 2 2 0 2 0 2 0 2 + t: 0 0 0 0 0 0 0 0 -1 1 -1 0 0 0 0 0 0 0 -1 1 1 -1 0 0 0 -1 1 1 -1 0 0 0 0 -1 1 1 -1 -1 1 1 -1 -1 1 -1 0 0 -1 1 1 0 0 -1 1 0 0 0 0 -1 1 -1 1 0 0 0 -1 1 0 0 -1 1 -1 1 0 0 -1 1 0 0 0 0 -1 1 0 0 -1 1 -1 1 0 0 0 -1 1 -1 1 0 0 1 0 0 0 0 -1 1 +term 6 cost 7 + d: 1 -1 -1 1 0 0 0 0 0 0 0 1 -1 -1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 + t: 2 -2 0 0 2 -2 0 0 0 0 0 2 -2 0 2 -2 0 0 0 0 0 0 0 2 2 2 2 2 2 2 -2 0 0 0 0 0 0 2 2 2 2 0 0 0 2 2 2 2 0 0 0 2 2 2 2 0 0 0 0 0 0 0 -2 -2 -2 -2 0 0 0 0 -2 -2 -2 -2 2 2 2 2 0 0 0 0 2 2 2 2 0 0 0 0 0 0 0 -2 -2 -2 -2 0 0 0 -2 -2 -2 -2 +term 7 cost 7 + d: 2 0 0 2 0 2 0 2 2 2 0 0 -2 -2 -2 0 -2 0 0 -2 0 -2 2 0 2 2 0 2 0 -2 0 -2 0 0 -2 0 -2 0 -2 0 -2 0 -2 -2 0 -2 0 0 0 2 0 0 0 2 0 2 0 2 2 -2 -2 -2 0 -2 0 0 0 -2 0 0 0 0 2 0 0 0 2 0 2 0 2 2 2 0 2 2 2 2 2 0 -2 0 0 0 0 2 0 0 2 0 2 0 2 2 + t: 0 0 0 0 -1 1 -1 1 0 0 0 0 0 0 -1 1 -1 1 0 0 0 0 1 -1 1 0 0 0 0 -1 1 -1 1 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 -1 -1 0 0 0 0 1 1 -1 0 0 0 0 1 1 diff --git a/research/complex-frame-pair-decoders/inputs/pr717/P111_HIT_g0.txt b/research/complex-frame-pair-decoders/inputs/pr717/P111_HIT_g0.txt new file mode 100644 index 0000000000..05b86974fe --- /dev/null +++ b/research/complex-frame-pair-decoders/inputs/pr717/P111_HIT_g0.txt @@ -0,0 +1,26 @@ +cost 63 n 8 NP 111 +D(cols) +term 0 cost 8 + d: 1 -1 1 0 0 0 0 0 0 0 0 -1 1 -1 1 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 + t: 2 0 2 2 0 2 0 1 1 1 1 0 2 0 2 2 0 2 0 1 1 1 1 0 -2 0 -2 -1 -1 -1 -1 0 -2 0 -2 -1 -1 -1 -1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 -1 -1 2 2 1 1 1 1 0 0 2 2 1 1 1 1 0 0 3 3 2 2 2 2 1 1 0 0 -1 -1 -1 -1 -2 -2 1 1 0 0 0 0 -1 -1 1 1 0 0 0 0 -1 -1 2 2 1 1 1 1 0 0 +term 1 cost 8 + d: 0 0 0 0 0 0 0 1 -1 -1 1 0 0 0 0 0 0 0 0 1 -1 -1 1 0 0 0 0 1 -1 -1 1 0 0 0 0 1 -1 -1 1 1 -1 -1 1 1 -1 -1 1 0 0 1 -1 1 -1 0 0 1 -1 0 0 0 0 1 -1 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 0 0 1 -1 1 -1 0 0 1 -1 0 0 0 0 1 -1 + t: 0 0 0 0 0 -2 2 1 -1 -1 1 0 0 0 0 0 0 -2 2 1 -1 -1 1 0 0 -2 2 1 -1 -1 1 0 0 -2 2 1 -1 -1 1 1 -1 -1 1 -1 -3 -3 -1 -1 -1 2 0 0 -2 1 1 0 -2 1 1 -1 -1 2 0 0 -2 1 1 -1 -1 2 0 -1 -1 2 0 0 -2 1 1 0 -2 1 1 -1 -1 2 0 -1 -1 2 0 0 -2 1 1 -1 -1 2 0 0 -2 1 1 0 -2 1 1 -1 -1 2 0 +term 2 cost 8 + d: 1 1 -1 0 0 0 0 0 0 0 0 -1 1 1 -1 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 + t: 2 2 0 1 1 1 1 1 1 1 1 0 2 2 0 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 2 2 2 2 2 2 2 2 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 +term 3 cost 7 + d: 0 2 2 2 2 2 2 2 2 2 2 2 -2 0 0 0 0 0 0 0 0 0 0 2 2 2 2 2 2 2 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 + t: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +term 4 cost 8 + d: 0 0 0 0 0 0 0 1 -1 1 -1 0 0 0 0 0 0 0 0 1 -1 1 -1 0 0 0 0 1 -1 1 -1 0 0 0 0 1 -1 1 -1 1 -1 1 -1 1 -1 1 -1 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 0 0 1 -1 1 -1 0 0 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 1 -1 0 0 0 0 1 -1 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 + t: 0 0 0 -1 1 -1 1 1 -1 1 -1 0 0 0 0 -1 1 -1 1 1 -1 1 -1 -1 1 -1 1 1 -1 1 -1 -1 1 -1 1 1 -1 1 -1 0 -2 0 -2 0 -2 0 -2 0 -2 0 0 0 0 2 0 -1 -1 1 -1 1 -1 1 1 -1 -1 1 -1 1 -1 1 1 0 -2 0 0 0 0 2 0 -1 -1 1 -1 1 -1 1 1 0 -2 0 0 0 0 2 0 0 -2 0 0 0 0 2 0 -1 -1 1 -1 1 -1 1 1 +term 5 cost 8 + d: 1 -1 1 -1 1 -1 1 -2 2 0 0 -1 1 -1 1 -1 1 -1 1 -2 2 0 0 -2 0 -2 0 -3 1 -1 -1 -2 0 -2 0 -3 1 -1 -1 -3 1 -1 -1 -3 1 -1 -1 -3 -1 -2 0 -2 0 -1 1 -2 0 -1 1 -1 1 0 2 -2 0 -1 1 -1 1 0 2 -1 1 0 2 0 2 1 3 -3 -1 -2 0 -2 0 -1 1 -2 0 -1 1 -1 1 0 2 -2 0 -1 1 -1 1 0 2 -1 1 0 2 0 2 1 3 + t: 0 0 0 -1 1 -1 1 0 0 0 0 0 0 0 0 -1 1 -1 1 0 0 0 0 -1 1 -1 1 0 0 0 0 -1 1 -1 1 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 +term 6 cost 8 + d: 1 1 1 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 + t: 0 0 0 1 -1 -1 1 0 0 0 0 -2 -2 -2 -2 -1 -3 -3 -1 -2 -2 -2 -2 1 -1 -1 1 0 0 0 0 1 -1 -1 1 0 0 0 0 1 1 1 1 -1 -1 -1 -1 -1 -1 0 0 -2 -2 -1 -1 -1 -1 0 0 -2 -2 -1 -1 -1 -1 0 0 -2 -2 -1 -1 -1 -1 0 0 -2 -2 -1 -1 1 1 2 2 0 0 1 1 1 1 2 2 0 0 1 1 1 1 2 2 0 0 1 1 1 1 2 2 0 0 1 1 +term 7 cost 8 + d: 1 1 1 0 2 2 0 2 0 0 2 -1 -1 -1 -1 -2 0 0 -2 0 -2 -2 0 -1 1 1 -1 1 -1 -1 1 -1 1 1 -1 1 -1 -1 1 0 -2 -2 0 2 0 0 2 0 0 0 -2 2 0 0 0 1 -1 -1 -1 1 1 1 -1 1 -1 -1 -1 1 1 1 -1 0 0 0 -2 2 0 0 0 2 0 0 0 2 2 2 0 1 1 1 -1 3 1 1 1 1 1 1 -1 3 1 1 1 2 0 0 0 2 2 2 0 + t: 0 0 0 -1 1 1 -1 0 0 0 0 0 0 0 0 -1 1 1 -1 0 0 0 0 -1 1 1 -1 0 0 0 0 -1 1 1 -1 0 0 0 0 -1 -1 -1 -1 1 1 1 1 0 0 -1 -1 1 1 0 0 0 0 -1 -1 1 1 0 0 0 0 -1 -1 1 1 0 0 0 0 -1 -1 1 1 0 0 0 0 -1 -1 1 1 0 0 0 0 -1 -1 1 1 0 0 0 0 -1 -1 1 1 0 0 0 0 -1 -1 1 1 0 0 diff --git a/research/complex-frame-pair-decoders/inputs/pr717/P111_HIT_g111.txt b/research/complex-frame-pair-decoders/inputs/pr717/P111_HIT_g111.txt new file mode 100644 index 0000000000..21930b3506 --- /dev/null +++ b/research/complex-frame-pair-decoders/inputs/pr717/P111_HIT_g111.txt @@ -0,0 +1,26 @@ +cost 63 n 8 NP 111 +D(cols) +term 0 cost 8 + d: 1 -1 1 -1 -2 2 0 0 -1 1 -1 1 1 -1 1 -1 -2 2 0 0 -1 1 -1 1 -1 3 1 1 0 2 0 2 -1 3 1 1 0 2 0 2 -3 -1 -3 -1 -1 1 -1 1 -1 1 0 0 2 2 1 3 -1 -1 -2 0 0 2 1 1 -1 -1 -2 0 0 2 1 1 -3 -1 -2 -2 0 0 -1 1 0 0 -1 1 1 3 2 2 -2 0 -1 -1 1 1 0 2 -2 0 -1 -1 1 1 0 2 -2 -2 -3 -1 -1 1 0 + t: 0 0 0 0 -1 1 -1 1 0 0 0 0 0 0 0 0 -1 1 -1 1 0 0 0 0 -1 1 -1 1 0 0 0 0 -1 1 -1 1 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 +term 1 cost 8 + d: 3 -1 1 1 1 1 1 1 0 2 0 2 1 -3 -1 -1 -1 -1 -1 -1 -2 0 -2 0 2 2 2 2 1 3 1 3 0 0 0 0 -1 1 -1 1 -1 1 -1 1 -1 1 -1 1 0 2 1 1 1 1 0 2 1 1 0 2 0 2 1 1 -1 -1 -2 0 -2 0 -1 -1 -2 0 -1 -1 -1 -1 -2 0 2 2 1 3 1 3 2 2 1 3 2 2 2 2 1 3 -1 1 0 0 0 0 -1 1 0 0 -1 1 -1 1 0 + t: 1 1 1 1 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 +term 2 cost 8 + d: 0 0 0 0 1 -1 -1 1 0 0 0 0 0 0 0 0 1 -1 -1 1 0 0 0 0 1 -1 -1 1 0 0 0 0 1 -1 -1 1 0 0 0 0 1 1 1 1 -1 -1 -1 -1 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 0 0 0 1 1 -1 -1 0 + t: -1 -1 -1 -1 -1 -1 -3 1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -3 1 -1 -1 -1 -1 0 0 -2 2 0 0 0 0 0 0 -2 2 0 0 0 0 0 0 0 0 -2 -2 -2 -2 -2 -2 0 0 -2 -2 0 0 -2 -2 0 0 -2 -2 0 0 -2 -2 0 0 -2 -2 0 0 -2 -2 0 0 -2 -2 0 0 -1 -1 1 1 -1 -1 1 1 -1 -1 1 1 -1 -1 1 1 -1 -1 1 1 -1 -1 1 1 -1 -1 1 1 -1 -1 1 +term 3 cost 8 + d: 0 0 0 0 0 0 0 0 1 -1 1 -1 0 0 0 0 0 0 0 0 1 -1 1 -1 0 0 0 0 1 -1 1 -1 0 0 0 0 1 -1 1 -1 1 -1 1 -1 1 -1 1 -1 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 0 0 1 -1 1 -1 0 0 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 0 1 -1 0 0 0 0 1 -1 1 -1 0 0 0 0 1 -1 0 0 1 -1 1 -1 0 + t: 1 1 1 1 0 2 0 2 1 1 3 -1 -1 -1 -1 -1 -2 0 -2 0 -1 -1 1 -3 -1 1 -1 1 0 0 2 -2 -1 1 -1 1 0 0 2 -2 -1 -1 1 -3 -1 -1 1 -3 0 -2 -1 1 -1 1 2 0 -2 0 1 -1 1 -1 0 2 -2 0 1 -1 1 -1 0 2 0 -2 -1 1 -1 1 2 0 -1 1 2 0 2 0 1 3 1 -1 0 2 0 2 3 1 1 -1 0 2 0 2 3 1 -1 1 2 0 2 0 1 +term 4 cost 8 + d: 0 2 2 0 2 0 0 2 1 1 1 1 0 2 2 0 2 0 0 2 1 1 1 1 0 -2 -2 0 -1 -1 -1 -1 2 0 0 2 1 1 1 1 1 1 1 1 -1 -1 -1 -1 1 1 2 2 0 0 1 1 0 0 1 1 -1 -1 0 0 2 2 3 3 1 1 2 2 1 1 2 2 0 0 1 1 0 0 1 1 -1 -1 0 0 -1 -1 0 0 -2 -2 -1 -1 1 1 2 2 0 0 1 1 0 0 1 1 -1 -1 0 + t: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 +term 5 cost 7 + d: 1 -1 1 -1 0 0 0 0 0 0 0 0 1 -1 1 -1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 -1 1 1 1 1 1 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 -1 -1 -1 -1 -1 -1 + t: 0 -2 0 -2 0 -2 0 -2 0 -2 -2 0 2 0 2 0 2 0 2 0 2 0 0 2 2 0 2 0 2 0 0 2 2 0 2 0 2 0 0 2 2 0 0 2 2 0 0 2 2 2 2 0 2 0 0 0 2 0 0 0 0 0 0 -2 2 0 0 0 0 0 0 -2 0 0 0 -2 0 -2 -2 -2 2 0 0 0 0 0 0 -2 0 0 0 -2 0 -2 -2 -2 0 0 0 -2 0 -2 -2 -2 0 -2 -2 -2 -2 -2 -2 +term 6 cost 8 + d: 1 -1 0 0 0 0 0 0 -1 1 0 0 1 -1 0 0 0 0 0 0 -1 1 0 0 1 1 1 1 0 2 1 1 0 0 0 0 -1 1 0 0 -1 1 0 0 -1 1 0 0 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 -1 0 -1 0 -1 0 -1 0 -1 0 -1 0 -1 0 -1 0 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 -1 0 -1 0 -1 0 -1 0 -1 0 -1 0 -1 0 -1 + t: 0 0 0 0 0 0 0 0 -2 2 2 -2 0 0 0 0 0 0 0 0 -2 2 2 -2 0 0 0 0 -2 2 2 -2 0 0 0 0 -2 2 2 -2 -2 2 2 -2 -2 2 2 -2 0 0 -2 2 -2 2 0 0 -2 2 0 0 0 0 -2 2 -2 2 0 0 0 0 -2 2 0 0 -2 2 -2 2 0 0 -2 2 0 0 0 0 -2 2 0 0 -2 2 -2 2 0 0 0 0 -2 2 -2 2 0 0 -2 2 0 0 0 0 -2 +term 7 cost 8 + d: 1 -1 -1 1 0 0 0 0 0 0 0 0 1 -1 -1 1 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 -1 -1 -1 -1 -1 -1 -1 -1 0 0 0 0 0 0 0 + t: 1 -1 -1 1 0 0 0 0 1 -1 -1 1 3 1 1 3 2 2 2 2 3 1 1 3 1 1 1 1 2 0 0 2 -1 -1 -1 -1 0 -2 -2 0 1 -1 -1 1 1 -1 -1 1 1 1 2 0 2 0 1 1 3 1 2 2 2 2 3 1 1 -1 0 0 0 0 1 -1 1 1 2 0 2 0 1 1 0 -2 -1 -1 -1 -1 0 -2 0 0 1 -1 1 -1 0 0 -2 -2 -1 -3 -1 -3 -2 -2 0 -2 -1 -1 -1 -1 0 diff --git a/research/complex-frame-pair-decoders/verify.py b/research/complex-frame-pair-decoders/verify.py new file mode 100644 index 0000000000..57dd8993e8 --- /dev/null +++ b/research/complex-frame-pair-decoders/verify.py @@ -0,0 +1,740 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Frame-pair decoders and the exact 8-term copy-cost floor on punctured complex E8 units. + +Standard library only. Exact integer, F2 and rational arithmetic throughout. + +Model (PR717 B14, D2/D3 scope): the 120 E8 root lines; a puncture P removes lines; an exact +8-term decoder is D = R A, T = R B with A B^T = 2 I, so that D T^T = 2G on the live lines +(G the integer inner products). Term k costs the F2 rank of the label pairing between its row +support (live lines not orthogonal to a_k) and column support (live lines not orthogonal to b_k). +The label pairing of two lines is ( + 1) mod 2, which this script uses directly; it +never constructs PR717's simple-root coordinates. + +Sections (each prints PASS/FAIL lines): + A model facts: 120 lines, nondegenerate rank-9 pairing, distinct pairing rows + B violator census for the eight W(E8) hyperplane-flat types (all 511 hyperplanes and all + 130,305 codimension-2 pairs of F2^9 functionals) + C the D7 orbit: 1080 directions, unique 14-line violator sets, pairwise unions >= 21, no + coincidence with a root functional + D frame-pair census: all 1260 frames disjoint from the coordinate frame, all (S, T) splits; + every solution is built and checked exactly + E attaining chain: explicit exact decoders for every puncture size p = 0..24 + F replay of the three vendored PR717 D3 hits and their root-pair structure + G favorable-budget pricing on the selected (U8/T37) profile with the pinned moment and outer + engines, and the PR589 bit-supplier cap + H negative controls +""" +import argparse +import hashlib +import importlib.util +import itertools +import json +import math +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +FAILS = [] +LOG = [] + + +def check(tag, cond, info=''): + line = ('PASS ' if cond else 'FAIL ') + tag + (' | ' + info if info else '') + print(line, flush=True) + LOG.append(line) + if not cond: + FAILS.append(tag) + + +# ---------------------------------------------------------------- A. E8 lines and pairing +def e8_roots(): + """240 roots in doubled coordinates; same enumeration order as PR717's e8model (adapter only).""" + roots = [] + for i, j in itertools.combinations(range(8), 2): + for si in (1, -1): + for sj in (1, -1): + v = [0] * 8 + v[i], v[j] = 2 * si, 2 * sj + roots.append(tuple(v)) + for s in itertools.product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: + roots.append(tuple(s)) + return roots + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +def ip(x, y): + """True inner product of doubled-coordinate vectors.""" + d = dot(x, y) + assert d % 4 == 0 + return d // 4 + + +def neg(v): + return tuple(-a for a in v) + + +ROOTS = e8_roots() +LINES = [] +_seen = set() +for r in ROOTS: + key = r if r > neg(r) else neg(r) + if key not in _seen: + _seen.add(key) + LINES.append(r) +NL = len(LINES) +IP = [[ip(LINES[i], LINES[j]) for j in range(NL)] for i in range(NL)] +# Label pairing as a 120-bit row mask: bit j of NROW[i] is ( + 1) mod 2. +NROW = [sum(((IP[i][j] + 1) & 1) << j for j in range(NL)) for i in range(NL)] +ALL = (1 << NL) - 1 +FRAME0 = [] +for a in range(4): + for s in (1, -1): + v = [0] * 8 + v[2 * a], v[2 * a + 1] = 2, 2 * s + FRAME0.append(LINES.index(tuple(v))) +P112 = [i for i in range(NL) if i not in FRAME0] + + +def popcount(x): + return bin(x).count('1') + + +def f2_rank(rows): + basis = {} + rank = 0 + for v in rows: + while v: + h = v.bit_length() - 1 + if h in basis: + v ^= basis[h] + else: + basis[h] = v + rank += 1 + break + return rank + + +def mask(idx): + m = 0 + for i in idx: + m |= 1 << i + return m + + +def pair_rank(rows, cols): + """F2 rank of the label pairing between the lines in `rows` and the lines in `cols`.""" + cm = mask(cols) + return f2_rank([NROW[i] & cm for i in rows]) + + +def span_dim(idx): + return f2_rank([NROW[i] for i in idx]) + + +def section_a(): + check('A.lines', NL == 120 and len(ROOTS) == 240, '120 lines from 240 roots') + check('A.pairing-values', all(IP[i][i] == 2 for i in range(NL)) and + {IP[i][j] for i in range(NL) for j in range(NL) if i != j} == {-1, 0, 1}, + 'line inner products are 2 on the diagonal and 0/+-1 off it') + check('A.pairing-rank-9', f2_rank(NROW) == 9, 'the 120x120 label pairing has F2 rank 9 (nondegenerate on the 9-dim label span)') + check('A.distinct-rows', len(set(NROW)) == 120, 'distinct lines have distinct pairing rows (distinct label functionals)') + check('A.frame0', len(FRAME0) == 8 and all(IP[a][b] == 0 for a in FRAME0 for b in FRAME0 if a != b), + 'coordinate frame e_{2a} +- e_{2a+1}: eight mutually orthogonal lines; P112 has %d lines' % len(P112)) + + +# Dual coordinates: phi_i = (pairing with nine basis lines). An F2-linear isomorphism of the label span, +# so the 511 nonzero functionals lambda . phi_i are exactly the 511 hyperplanes of the label space. +def dual_coordinates(): + basis = [] + for i in range(NL): + if f2_rank([NROW[b] for b in basis] + [NROW[i]]) == len(basis) + 1: + basis.append(i) + if len(basis) == 9: + break + phi = [sum(((NROW[i] >> b) & 1) << k for k, b in enumerate(basis)) for i in range(NL)] + return basis, phi + + +BASIS9, PHI = dual_coordinates() +LAMBDAS = list(range(1, 512)) +VMASK = {lam: mask(i for i in range(NL) if popcount(lam & PHI[i]) & 1) for lam in LAMBDAS} +ROOT_FUNCTIONAL = {} +for _i in range(NL): + # the functional of line i: lambda with lambda . phi_j = pairing(i, j) for all j + _cands = [lam for lam in LAMBDAS if VMASK[lam] == NROW[_i]] + assert len(_cands) == 1 + ROOT_FUNCTIONAL[_i] = _cands[0] + + +# ---------------------------------------------------------------- B. violator census +def solve_rational(M, rhs): + """Solve M x = rhs exactly (M square, invertible) with Fractions.""" + n = len(M) + A = [[Q(x) for x in row] + [Q(b)] for row, b in zip(M, rhs)] + for c in range(n): + p = next(r for r in range(c, n) if A[r][c] != 0) + A[c], A[p] = A[p], A[c] + for r in range(n): + if r != c and A[r][c] != 0: + f = A[r][c] / A[c][c] + A[r] = [x - f * y for x, y in zip(A[r], A[c])] + return [A[i][n] / A[i][i] for i in range(n)] + + +SIMPLE = [(1, -1, -1, -1, -1, -1, -1, 1), (2, 2, 0, 0, 0, 0, 0, 0), (-2, 2, 0, 0, 0, 0, 0, 0)] + \ + [tuple(-2 if t == k else 2 if t == k + 1 else 0 for t in range(8)) for k in range(1, 6)] + + +def fundamental_weights(): + """omega_i with = delta_ij, as integer doubled-coordinate directions.""" + out = [] + for i in range(8): + # unknown x (true coordinates): sum_t x_t * alpha_j[t]/2 = delta_ij + M = [[Q(a, 2) for a in alpha] for alpha in SIMPLE] + x = solve_rational(M, [1 if j == i else 0 for j in range(8)]) + den = 1 + for v in x: + den = den * v.denominator // math.gcd(den, v.denominator) + vec = tuple(int(v * den) for v in x) + out.append(vec) + return out + + +def support_mask(a): + return mask(i for i in range(NL) if dot(a, LINES[i]) != 0) + + +def census_type(a): + C = support_mask(a) + sizes = sorted(popcount(VMASK[lam] & C) for lam in LAMBDAS) + vm = [VMASK[lam] & C for lam in LAMBDAS] + pi7 = min(popcount(vm[x] | vm[y]) for x in range(511) for y in range(x + 1, 511)) + span = f2_rank([NROW[i] for i in range(NL) if C >> i & 1]) + return dict(support=popcount(C), flat_lines=NL - popcount(C), span=span, pi8=sizes[0], pi8_second=sizes[1], pi7=pi7) + + +EXPECTED_TYPES = { # flat lines -> (subsystem, |C|, pi8, second pi8, pi7) + 63: ('E7', 57, 1, 24, 25), 42: ('D7', 78, 14, 34, 42), 37: ('E6+A1', 83, 27, 28, 51), + 28: ('A7', 92, 28, 35, 56), 23: ('D5+A2', 97, 33, 41, 61), 22: ('A6+A1', 98, 35, 35, 62), + 16: ('A4+A3', 104, 40, 43, 68), 14: ('A4+A2+A1', 106, 43, 43, 70)} + + +def section_b(): + weights = fundamental_weights() + check('B.weights', all(sum(Q(dot(w, a), 4) == 0 for a in SIMPLE) == 7 for w in weights), + 'eight fundamental-weight directions, each orthogonal to seven simple roots') + rows = {} + for w in weights: + info = census_type(w) + rows[info['flat_lines']] = info + ok = set(rows) == set(EXPECTED_TYPES) and all( + (rows[f]['support'], rows[f]['pi8'], rows[f]['pi8_second'], rows[f]['pi7']) == EXPECTED_TYPES[f][1:] + and rows[f]['span'] == 9 for f in rows) + table = '; '.join('%s flat %d: |C|=%d pi8=%d (next %d) pi7=%d' % (EXPECTED_TYPES[f][0], f, rows[f]['support'], + rows[f]['pi8'], rows[f]['pi8_second'], rows[f]['pi7']) for f in sorted(rows, reverse=True)) + check('B.census', ok, table) + nonroot = min(rows[f]['pi8'] for f in rows if f != 63) + check('B.thresholds', nonroot == 14 and rows[63]['pi8_second'] == 24 and min(r['pi7'] for r in rows.values()) == 25, + 'only E7 (root) normals drop to an 8-dim span with one puncture (their own line); every other type needs >= 14; ' + 'a root normal by another hyperplane needs >= 24; any 7-dim span needs >= 25 punctures') + # the root type's unique one-line violator set is the line itself, through its own functional + alpha = next(i for i in range(NL) if LINES[i] == (2, 2, 0, 0, 0, 0, 0, 0)) + C = support_mask(LINES[alpha]) + check('B.root-self-line', VMASK[ROOT_FUNCTIONAL[alpha]] & C == 1 << alpha, + 'for a root normal alpha the 1-line violator set is {alpha}, via the functional of alpha itself') + allroots = True + for i in range(NL): + C = support_mask(LINES[i]) + sizes = sorted((popcount(VMASK[lam] & C), lam) for lam in LAMBDAS) + allroots &= sizes[0] == (1, ROOT_FUNCTIONAL[i]) and VMASK[ROOT_FUNCTIONAL[i]] & C == 1 << i and sizes[1][0] == 24 + check('B.root-all-120', allroots, 'checked directly for all 120 root normals: unique 1-line set {alpha}; every other hyperplane >= 24') + return rows, weights + + +# ---------------------------------------------------------------- C. D7 orbit +def canon(v): + g = 0 + for a in v: + g = math.gcd(g, abs(a)) + v = tuple(a // g for a in v) + first = next(a for a in v if a) + return v if first > 0 else neg(v) + + +def orbit(start): + seen = {canon(start)} + frontier = [canon(start)] + while frontier: + nxt = [] + for v in frontier: + for r in LINES: + d = dot(v, r) + u = tuple(4 * a - d * b for a, b in zip(v, r)) # 4 * reflection, integral + c = canon(u) + if c not in seen: + seen.add(c) + nxt.append(c) + frontier = nxt + return sorted(seen) + + +def section_c(weights): + d7 = next(w for w in weights if NL - popcount(support_mask(w)) == 42) + dirs = orbit(d7) + check('C.orbit', len(dirs) == 1080, 'W(E8) orbit of the D7 normal: %d directions' % len(dirs)) + v14 = {} + root_funcs = set(ROOT_FUNCTIONAL.values()) + coincide = 0 + inflat_all = True + rank_ok = True + for d in dirs: + C = support_mask(d) + sizes = sorted((popcount(VMASK[lam] & C), lam) for lam in LAMBDAS) + assert sizes[0][0] == 14 and sizes[1][0] >= 34 + lam = sizes[0][1] + v14[d] = VMASK[lam] & C + coincide += lam in root_funcs + flat = [i for i in range(NL) if not C >> i & 1] + inflat_all &= all(popcount(VMASK[lam] >> i & 1) for i in flat) + # removing any one flat line leaves a rank-7 set: a flat of rank <= 6 misses >= 2 of the 42 lines + # (not needed by the main argument; recorded as a cross-check of D7 rigidity) + if d == dirs[0]: + rank_ok = all(rank_q([LINES[j] for j in flat if j != i]) == 7 for i in flat) + sets = list(v14.values()) + check('C.unique-14', len(set(sets)) == 1080, 'each D7 direction has a unique 14-line violator set (next >= 34); 1080 distinct sets') + mn = min(popcount(a | b) for a, b in itertools.combinations(sets, 2)) + check('C.unions', mn == 21, 'any two distinct D7 violator sets have union >= %d > 15' % mn) + check('C.no-root-coincidence', coincide == 0, 'no D7 minimizing functional equals a root functional') + check('C.flat-lines-violate', inflat_all and rank_ok, 'all 42 flat lines violate the minimizing functional; flat minus any line has rank 7') + return len(dirs) + + +def rank_q(vectors): + rows = [[Q(x) for x in v] for v in vectors] + r = 0 + ncol = len(rows[0]) if rows else 0 + for c in range(ncol): + p = next((i for i in range(r, len(rows)) if rows[i][c] != 0), None) + if p is None: + continue + rows[r], rows[p] = rows[p], rows[r] + for i in range(len(rows)): + if i != r and rows[i][c] != 0: + f = rows[i][c] / rows[r][c] + rows[i] = [x - f * y for x, y in zip(rows[i], rows[r])] + r += 1 + return r + + +# ---------------------------------------------------------------- decoders +def decoder_cost(rowvecs, colvecs, live): + """Exactness of D T^T = 2G on `live` and the per-term costs.""" + live = list(live) + D = [[ip(LINES[i], a) for a in rowvecs] for i in live] + T = [[ip(LINES[i], b) for b in colvecs] for i in live] + exact = all(sum(x * y for x, y in zip(D[p], T[q])) == 2 * IP[live[p]][live[q]] + for p in range(len(live)) for q in range(len(live))) + costs = [] + for k in range(len(rowvecs)): + R = [live[p] for p in range(len(live)) if D[p][k]] + A = [live[p] for p in range(len(live)) if T[p][k]] + costs.append(pair_rank(R, A)) + return exact, costs + + +def frames_in(pool): + pool = list(pool) + orth = {i: mask(j for j in pool if j != i and IP[i][j] == 0) for i in pool} + out = [] + + def rec(clique, cand): + if len(clique) == 8: + out.append(tuple(clique)) + return + c = cand + while c: + j = c.bit_length() - 1 + c &= ~(1 << j) + rec(clique + [j], cand & orth[j] & ((1 << j) - 1)) + + for i in pool: + rec([i], orth[i] & ((1 << i) - 1)) + return sorted(tuple(sorted(f)) for f in out) + + +def frame_pair_solutions(F0, F1): + """All splits: row normals S (from F0) and T (from F1); every column partner is a cross-frame line with + odd inner product and orthogonal to all other row normals.""" + sols = [] + for smask in range(256): + S = [F0[j] for j in range(8) if smask >> j & 1] + need = 8 - len(S) + # g in F1 is usable as the partner of f in S iff N(g) cap S == {f} + part = {f: [g for g in F1 if [x for x in S if IP[g][x]] == [f]] for f in S} + if any(not part[f] for f in S): + continue + for choice in itertools.product(*[part[f] for f in S]): + if len(set(choice)) != len(S): + continue + Tset = [g for g in F1 if g not in choice] + if len(Tset) != need: + continue + rest = [f for f in F0 if f not in S] + part2 = {g: [f for f in rest if [x for x in Tset if IP[f][x]] == [g]] for g in Tset} + if any(not part2[g] for g in Tset): + continue + for choice2 in itertools.product(*[part2[g] for g in Tset]): + if len(set(choice2)) != len(Tset): + continue + pairs = list(zip(S, choice)) + list(zip(Tset, choice2)) + sols.append(pairs) + return sols + + +def pair_decoder(pairs, live): + """Root-pair decoder (a_k = alpha_k, b_k = 2 beta_k). Exactness on every live set is + equivalent to = 2 delta_kl, i.e. A^T B = 2I, hence A B^T = 2I and D T^T = R (A B^T) R^T = 2G.""" + dual = all((IP[a][b] in (1, -1)) if k == l else IP[a][b] == 0 + for k, (a, _) in enumerate(pairs) for l, (_, b) in enumerate(pairs)) + costs = [pair_rank([i for i in live if IP[a][i]], [i for i in live if IP[b][i]]) for a, b in pairs] + return dual, costs + + +def build_pairs(pairs): + rows, cols = [], [] + for a, b in pairs: + e = IP[a][b] + assert e in (1, -1) + rows.append(LINES[a]) + cols.append(tuple(2 * e * x for x in LINES[b])) + return rows, cols + + +def relative_type(F0, F1): + common = Counter(sum(1 for f in F0 if IP[g][f] and IP[h][f]) for g, h in itertools.combinations(F1, 2)) + return tuple(sorted(common.items())) + + +def section_d(): + F1s = frames_in(P112) + check('D.frames', len(F1s) == 1260, '%d frames inside P112 (disjoint from the coordinate frame)' % len(F1s)) + hist = Counter() + types = Counter() + built = 0 + allgood = True + example = None + for F1 in F1s: + sols = frame_pair_solutions(FRAME0, list(F1)) + hist[len(sols)] += 1 + types[(len(sols) > 0, relative_type(FRAME0, F1))] += 1 + live = [i for i in range(NL) if i not in FRAME0 and i not in F1] + for pairs in sols: + exact, costs = pair_decoder(pairs, live) + built += 1 + allgood &= exact and costs == [7] * 8 + if example is None: + example = dict(F1=list(F1), pairs=pairs) + check('D.census', hist == Counter({8: 896, 0: 364}), 'solutions per frame: %s' % dict(sorted(hist.items()))) + tdesc = {str(k): v for k, v in sorted(types.items(), key=lambda kv: -kv[1])} + check('D.types', len(types) == 3 and all(ok == (dict(t).get(4, 0) == 0) for ok, t in types), + 'relative position (common F0-neighbours of F1 pairs) -> admissible: %s' % tdesc) + check('D.exact-56', allgood and built == 7168, '%d frame-pair decoders built; every one satisfies A^T B = 2I and has eight cost-7 terms on its P104 (cst 56)' % built) + F1 = example['F1'] + live = [i for i in range(NL) if i not in FRAME0 and i not in F1] + rows, cols = build_pairs(example['pairs']) + exact, costs = decoder_cost(rows, cols, live) + check('D.full-exactness-crosscheck', exact and costs == [7] * 8, 'one decoder rechecked entrywise: D T^T = 2G on all 104 x 104 live pairs') + return F1s, example, hist, types + + +def section_e(F1s, example): + F1 = example['F1'] + pairs = example['pairs'] + # ordering of F1 lines: each F1 line is the self-line of exactly one term + f1order = [b if b in F1 else a for a, b in pairs] + chain = {} + extra = [i for i in range(NL) if i not in FRAME0 and i not in F1] + coord_rows = [LINES[f] for f in FRAME0] + for p in range(0, 25): + if p <= 8: + P = FRAME0[:p] + rows, cols = coord_rows, coord_rows + kind = 'coordinate frame, %d of its lines punctured' % p + else: + j = min(p - 8, 8) + P = FRAME0 + f1order[:j] + extra[:max(0, p - 16)] + rows, cols = build_pairs(pairs) + kind = 'frame pair, %d partner lines + %d extra lines punctured' % (j, max(0, p - 16)) + live = [i for i in range(NL) if i not in P] + exact, costs = decoder_cost(rows, cols, live) + bound = max(72 - p, 56) + chain[p] = dict(live=len(live), exact=exact, cost=sum(costs), lower_bound=bound, kind=kind, + ratio=str(Q(sum(costs), len(live))), punctured=sorted(P), live_rank=rank_q([LINES[i] for i in live])) + ok = all(c['exact'] and c['cost'] == c['lower_bound'] and c['live_rank'] == 8 and len(c['punctured']) == p + for p, c in chain.items()) + check('E.chain', ok, 'p=0..24: exact decoders with cst = max(72-p, 56) at every p (attaining the theorem)') + best = min(chain, key=lambda p: Q(chain[p]['cost'], chain[p]['live'])) + check('E.best-ratio', best == 16 and Q(chain[16]['cost'], chain[16]['live']) == Q(7, 13) and + Q(chain[8]['cost'], chain[8]['live']) == Q(4, 7), + 'minimum copy ratio along the chain is 56/104 = 7/13 at p = 16 (P112: 64/112 = 4/7)') + return chain + + +# ---------------------------------------------------------------- F. PR717 hit replay +def load_hit(path): + D, T = [], [] + for line in path.read_text().splitlines(): + s = line.strip() + if s.startswith('d:'): + D.append([int(x) for x in s[2:].split()]) + if s.startswith('t:'): + T.append([int(x) for x in s[2:].split()]) + return [list(c) for c in zip(*D)], [list(c) for c in zip(*T)] # live x n + + +def recover(live, col): + """Exact vector a with = col[p] for every live line; returns doubled coordinates or None.""" + idx = [] + for p, i in enumerate(live): + if rank_q([LINES[live[q]] for q in idx] + [LINES[i]]) == len(idx) + 1: + idx.append(p) + if len(idx) == 8: + break + M = [[Q(x, 4) for x in LINES[live[p]]] for p in idx] + a = solve_rational(M, [col[p] for p in idx]) + ok = all(sum(Q(x, 4) * y for x, y in zip(LINES[i], a)) == col[p] for p, i in enumerate(live)) + return a if ok else None + + +def as_line(a): + """Index of the root line parallel to a, or None.""" + for i, r in enumerate(LINES): + ratio = None + good = True + for x, y in zip(r, a): + if x == 0: + good &= y == 0 + else: + q = Q(y) / x + good &= ratio is None or q == ratio + ratio = q + if good and ratio: + return i + return None + + +def section_f(): + p112 = P112 + results = {} + vend = json.loads((HERE / 'SOURCES.json').read_text())['vendored'] + check('F.vendored-pins', all(sha(HERE / rel) == meta['sha256'] for rel, meta in vend.items()) and len(vend) == 3, + 'three PR717 decoder files match their SHA-256 pins (PR717 head %s)' % next(iter(vend.values()))['head'][:7]) + clique717 = [9, 15, 24, 46, 52, 66, 94, 104] # PR717 d3_punctures.py, P112 indexing + cases = [('P104_HIT_flip_3a.txt', [p112[q] for q in clique717]), ('P111_HIT_g0.txt', [p112[0]]), + ('P111_HIT_g111.txt', [p112[111]])] + for name, extra in cases: + punct = FRAME0 + extra + live = [i for i in range(NL) if i not in punct] + D, T = load_hit(HERE / 'inputs/pr717' / name) + recorded = [int(l.split()[3]) for l in (HERE / 'inputs/pr717' / name).read_text().splitlines() if l.startswith('term ')] + exact = all(sum(x * y for x, y in zip(D[p], T[q])) == 2 * IP[live[p]][live[q]] + for p in range(len(live)) for q in range(len(live))) + terms = [] + for k in range(len(D[0])): + a = recover(live, [row[k] for row in D]) + b = recover(live, [row[k] for row in T]) + R = [live[p] for p in range(len(live)) if D[p][k]] + A = [live[p] for p in range(len(live)) if T[p][k]] + la, lb = as_line(a), as_line(b) + terms.append(dict(cost=pair_rank(R, A), row_root=la, col_root=lb, + odd=(la is not None and lb is not None and IP[la][lb] % 2 != 0), + both_punctured=(la in punct and lb in punct))) + results[name] = dict(exact=exact, costs=[t['cost'] for t in terms], recorded_by_pr717=recorded, terms=terms) + check('F.%s.costs-match-pr717' % name, recorded == [t['cost'] for t in terms], + 'per-term pairing ranks from (+1) mod 2 equal the costs PR717 recorded with its own label model') + seven = [t for t in terms if t['cost'] == 7] + check('F.%s' % name, exact and all(t['row_root'] is not None and t['col_root'] is not None and t['odd'] and + t['both_punctured'] for t in seven) and + all(not (t['odd'] and t['both_punctured']) for t in terms if t['cost'] != 7), + 'exact; costs %s; every cost-7 term is an odd root pair with both lines punctured, and no other term is' + % sorted(Counter(t['cost'] for t in terms).items())) + # PR717's P104 clique is an admissible second frame + F1 = sorted(p112[q] for q in clique717) + sols = frame_pair_solutions(FRAME0, F1) + check('F.P104-clique-is-frame-pair', all(IP[a][b] == 0 for a in F1 for b in F1 if a != b) and len(sols) == 8, + "PR717's random clique is a frame of the admissible relative type with 8 frame-pair decoders") + return results + + +# ---------------------------------------------------------------- G. pricing +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load_module(path, name): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def section_g(repo): + pins = json.loads((HERE / 'SOURCES.json').read_text())['pricing_inputs'] + for rel, h in pins.items(): + check('G.pin.' + rel.split('/')[-1], sha(repo / rel) == h, rel) + eng = repo / 'research/complex-k492-owner-repair/vendor/multicold/engines' + M = load_module(eng / 'moment.py', 'pinned_moment') + B2 = load_module(eng / 'base_two_moment.py', 'pinned_base_two_moment') + A = load_module(eng / 'outer.py', 'pinned_outer') + P = load_module(repo / 'research/complex-t21-owners/vendor/pr870/independent/price_profile_t16.py', 'pinned_t16') + bit = json.loads((repo / 'research/complex-t21-owners/vendor/pr870/inputs/PR589-EXPECTED.json').read_text()) + c = Q(bit['nine']['bit_lower']) + src = json.loads((HERE / 'SOURCES.json').read_text())['selected_record'] + sel = json.loads((repo / 'certificates/selected-result.json').read_text()) + check('G.selected-record', sel['certificate'] == src['certificate'] and sel['certificate_sha256'] == src['certificate_sha256'] + and sha(repo / sel['certificate']) == src['certificate_sha256'] and sel['kappa'] == src['kappa'], + 'pricing uses the selected record %s (%s)' % (sel['certificate'], sel['decimal'])) + asm = json.loads((repo / sel['certificate']).read_text()) + H0 = Counter({int(r): n for r, n in asm['complex_profile'].items()}) + m, cell = 73, (9 - 1) * 112 - 9 * 64 + mass = sum(r * n for r, n in H0.items()) + T = next(t for t in range(1, 1000) if m * 896 * t - mass == cell * t) + W0, D0, calls = 896 * T, cell * T, 9 * T + check('G.identity', m * W0 - mass == D0 and max(H0) == 48, + 'selected profile: %d replicas, 73*%d - mass = %d = %d*((9-1)*112 - 9*64)' % (T, W0, D0, T)) + + def scenario(ports, units): + """PR717 P1 knobs transported to the selected U8 profile: a cst unit lowers one centre cut climb 8 -> 7 in every call; + a port removes one modal source (1,1,1,5) and target (1,1,4,1,1) climb per call and nine idle + rank-48 children per replica.""" + H = Counter(H0) + H[8] -= units * calls + H[7] += units * calls + for _ in range(ports): + for x in (1, 1, 1, 5, 1, 1, 4, 1, 1): + H[x] -= calls + H[48] -= 9 * T + H = Counter({r: n for r, n in H.items() if n}) + W = W0 - T * 8 * ports + D = T * ((9 - 1) * (112 - ports) - 9 * (64 - units)) + assert all(n > 0 for n in H.values()) and m * W - sum(r * n for r, n in H.items()) == D + return H, W, D + + out = {} + for name, (ports, units) in [('selected', (0, 0)), ('P111_knobs', (1, 1)), ('P104_knobs', (8, 8))]: + H, W, D = scenario(ports, units) + native = Q(M.certify(H, m, W, False)['lower']) + conservative = Q(M.certify(H, m, W, True)['lower']) + checks = P.moment_checks(M, B2, H, m, W, native, D, False) + o = P.outer47(c, native, A) + out[name] = dict(W=W, deficit=D, complex_b=str(native), complex_b_decimal=P.decimal(native), + conservative_b_decimal=P.decimal(conservative), + b_change_percent=P.decimal((native / Q(asm['complex_lower']) - 1) * 100), + kappa=o['kappa'], kappa_decimal=o['kappa_decimal'], binding=o['binding'], + outer_controls_rejected=o['controls_rejected'], two_engines=len(checks) == 2) + cap = P.outer47(c, 2 * c, A) + out['bit_cap'] = dict(kappa=cap['kappa'], kappa_decimal=cap['kappa_decimal'], binding=cap['binding'], + gain_over_selected_percent=P.decimal((Q(cap['kappa']) / Q(sel['kappa']) - 1) * 100)) + check('G.gate', out['selected']['complex_b'] == str(Q(asm['complex_lower'])) and + Q(out['selected']['kappa']) == Q(sel['kappa']), + 'pinned engines on the selected profile reproduce b and kappa = %s exactly' % sel['decimal']) + check('G.P111', out['P111_knobs']['binding'] == 'complex', + 'P111 knobs: b %+.4f%%, kappa %s (complex-bound)' % (float(Q(out['P111_knobs']['b_change_percent'])), + out['P111_knobs']['kappa_decimal'])) + check('G.P104', out['P104_knobs']['binding'] == 'bit' and out['P104_knobs']['kappa'] == out['bit_cap']['kappa'], + 'P104 knobs: b %+.4f%% > bit c, kappa capped at %s' % (float(Q(out['P104_knobs']['b_change_percent'])), + out['P104_knobs']['kappa_decimal'])) + check('G.bit-cap', out['bit_cap']['binding'] == 'bit', + 'any complex-only change is capped by PR589 at kappa %s (%+.4f%%)' % ( + out['bit_cap']['kappa_decimal'], float(Q(out['bit_cap']['gain_over_selected_percent'])))) + headroom = Q(out['P104_knobs']['complex_b']) / c - 1 + out['P104_headroom_above_bit_percent'] = P.decimal(headroom * 100) + return out + + +# ---------------------------------------------------------------- H. negative controls +def section_h(example, F1s, hist): + F1 = example['F1'] + pairs = example['pairs'] + live104 = [i for i in range(NL) if i not in FRAME0 and i not in F1] + rows, cols = build_pairs(pairs) + # H1: perturb one column vector -> exactness lost + bad = list(cols) + bad[0] = tuple(x + y for x, y in zip(bad[0], LINES[FRAME0[0]])) + exact, _ = decoder_cost(rows, bad, live104) + check('H.mutated-decoder', not exact, 'adding a frame root to one column vector breaks D T^T = 2G') + # H2: restore one partner line -> that term costs 8 (cst 57 = 72 - 15) + restored = next(b if b in F1 else a for a, b in pairs) + live = live104 + [restored] + exact, costs = decoder_cost(rows, cols, live) + check('H.self-line-live', exact and sum(costs) == 57 and sorted(costs) == [7] * 7 + [8], + 'restoring one self-line raises exactly one term to 8: cst 57 at p = 15') + # H3: even pairing on the same puncture: the coordinate decoder on P104 stays at 64 + exact, costs = decoder_cost([LINES[f] for f in FRAME0], [LINES[f] for f in FRAME0], live104) + check('H.even-pairs', exact and sum(costs) == 64, 'coordinate (even, alpha = beta) decoder on the same P104 costs 64') + # H4: an inadmissible frame admits no frame-pair decoder (and the census is not vacuous) + bad_frames = [F for F in F1s if not frame_pair_solutions(FRAME0, list(F))] + check('H.inadmissible', len(bad_frames) == 364 and hist[0] == 364, '364 frames of the two other relative types have no solution') + # H5: a swapped partner assignment is not dual + swapped = list(pairs) + (a0, b0), (a1, b1) = swapped[0], swapped[1] + swapped[0], swapped[1] = (a0, b1), (a1, b0) + try: + r2, c2 = build_pairs(swapped) + exact, _ = decoder_cost(r2, c2, live104) + except AssertionError: + exact = False + check('H.swapped-partners', not exact, 'swapping two column partners breaks duality or the odd pairing') + # H6: a 25-line puncture can push a support to a 7-dim span (the threshold is sharp) + alpha = FRAME0[0] + C = support_mask(LINES[alpha]) + best = min(((VMASK[x] | VMASK[y]) & C, x, y) for x in LAMBDAS for y in LAMBDAS if x < y + and popcount((VMASK[x] | VMASK[y]) & C) == 25) + killed = [i for i in range(NL) if best[0] >> i & 1] + rest = [i for i in range(NL) if C >> i & 1 and i not in killed] + check('H.pi7-sharp', len(killed) == 25 and span_dim(rest) == 7, + 'puncturing a 25-line codim-2 violator set leaves a root support with a 7-dim label span') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__.split('\n')[0]) + parser.add_argument('--repo', type=Path, default=HERE.parent.parent, help='repository root (for pricing inputs)') + parser.add_argument('--out', type=Path, help='optional JSON certificate output (must not exist)') + args = parser.parse_args() + if not __debug__: + sys.exit('assertions must be enabled') + if args.out and args.out.exists(): + sys.exit('output exists: %s' % args.out) + section_a() + rows, weights = section_b() + orbit_size = section_c(weights) + F1s, example, hist, types = section_d() + chain = section_e(F1s, example) + hits = section_f() + prices = section_g(args.repo.resolve()) + section_h(example, F1s, hist) + status = 'PASS_COMPLEX_FRAME_PAIR_DECODERS' if not FAILS else 'FAIL' + cert = dict(status=status, failures=FAILS, + census={'%s(%d)' % (EXPECTED_TYPES[f][0], f): v for f, v in sorted(rows.items(), reverse=True)}, + d7_orbit=orbit_size, frame_pairs=dict(frames=len(F1s), admissible=hist[8], inadmissible=hist[0], + solutions_per_admissible_frame=8), + chain={str(p): v for p, v in chain.items()}, pr717_hits=hits, pricing=prices, log=LOG, + scope='Exact 8-term decoders (D = R A, T = R A^-T) in the PR717 B14 label-pairing model, punctures of at ' + 'most 24 of the 120 E8 lines. No word is built; pricing uses PR717 P1 knobs on the selected U8 ' + 'profile and is a favorable budget, not a kappa claim.') + if args.out: + args.out.write_text(json.dumps(cert, indent=1, default=str) + '\n') + print('%s: types 8; D7 orbit %d; frames %d (admissible %d); chain p=0..24; P104 7/13; bit cap kappa %s; controls 6' + % (status, orbit_size, len(F1s), hist[8], prices['bit_cap']['kappa_decimal'])) + sys.exit(1 if FAILS else 0) + + +if __name__ == '__main__': + main()