diff --git a/research/p112-five-group-projector-lift/CANDIDATE.json b/research/p112-five-group-projector-lift/CANDIDATE.json new file mode 100644 index 0000000000..9c59a624c3 --- /dev/null +++ b/research/p112-five-group-projector-lift/CANDIDATE.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "name": "five-group case30", + "group_names": [ + "A", + "B", + "C", + "D", + "E" + ], + "ports": [ + [ + 10, + 18, + 93 + ], + [ + 6, + 36, + 74 + ], + [ + 13, + 23, + 102 + ], + [ + 41, + 73, + 88 + ], + [ + 30, + 50, + 87 + ] + ], + "payload_dimensions": [ + 3, + 3, + 3, + 3, + 3 + ], + "endpoint": "I15", + "excluded_profile": { + "nonzero_rank_one_terms": 16, + "whole_group_tariff_histogram": { + "1": 2, + "3": 14 + } + }, + "scope": "These five custom triads only. Any finite rational I15 decomposition whose nonzero terms each cost at most 3 has total cost at least 45. Terms costing at least 4 and the full P112 supplier remain outside the result.", + "theorem": { + "term_count": "any finite number", + "maximum_per_term_whole_group_tariff": 3, + "minimum_total_invoice": 45, + "attained_by_direct_copies": true + } +} diff --git a/research/p112-five-group-projector-lift/CERTIFICATE.json b/research/p112-five-group-projector-lift/CERTIFICATE.json new file mode 100644 index 0000000000..753b9e2517 --- /dev/null +++ b/research/p112-five-group-projector-lift/CERTIFICATE.json @@ -0,0 +1,360 @@ +{ + "schema_version": 1, + "auxiliary_dimension": 3, + "matrix_denominator": 3, + "scaled_bilinear_matrix": [ + [ + 3, + 0, + 0, + 0, + 3, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 3, + 3, + 3 + ], + [ + 0, + 3, + 0, + 3, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 3, + 0 + ], + [ + 0, + 0, + 3, + 0, + 0, + 3, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 3, + 0 + ], + [ + 0, + 3, + 0, + 3, + 0, + 0, + 0, + 3, + 0, + 0, + 0, + 3, + 3, + 3, + 3 + ], + [ + 3, + 0, + 0, + 0, + 3, + 0, + 0, + 0, + 3, + 0, + 3, + 0, + 3, + 3, + 3 + ], + [ + 0, + 0, + 3, + 0, + 0, + 3, + 3, + 0, + 0, + 3, + 0, + 0, + 3, + 3, + 3 + ], + [ + 1, + 1, + 1, + 0, + 0, + 3, + 3, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 3 + ], + [ + 1, + 1, + 1, + 3, + 0, + 0, + 0, + 3, + 0, + 1, + 1, + 1, + 3, + 3, + 3 + ], + [ + 1, + 1, + 1, + 0, + 3, + 0, + 0, + 0, + 3, + 1, + 1, + 1, + 0, + 0, + 3 + ], + [ + 1, + 1, + 1, + 0, + 0, + 3, + 1, + 1, + 1, + 3, + 0, + 0, + 3, + 0, + 0 + ], + [ + 1, + 1, + 1, + 0, + 3, + 0, + 1, + 1, + 1, + 0, + 3, + 0, + 0, + 0, + 3 + ], + [ + 1, + 1, + 1, + 3, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 3, + 0, + 3, + 0 + ], + [ + 3, + 0, + 0, + 3, + 3, + 3, + 0, + 3, + 0, + 3, + 0, + 0, + 3, + 0, + 0 + ], + [ + 3, + 3, + 3, + 3, + 3, + 3, + 0, + 3, + 0, + 0, + 0, + 3, + 0, + 3, + 0 + ], + [ + 3, + 0, + 0, + 3, + 3, + 3, + 3, + 3, + 3, + 0, + 3, + 0, + 0, + 0, + 3 + ] + ], + "expected_counts": { + "rectangles": 961, + "cost1_types": 14, + "cost3_types": 273, + "common_cost3_types": 165, + "cheap_pair_candidates": 91, + "branches": 21, + "direct_exclusions": 17, + "rank_tight_exclusions": 4, + "cost0_types": 0, + "cost2_types": 20, + "low_tariff_exceptional_types": 4 + }, + "exceptional_branches": [ + { + "cheap_pair": [ + [ + 1, + 12 + ], + [ + 8, + 5 + ] + ], + "exceptional_type": [ + 20, + 9 + ] + }, + { + "cheap_pair": [ + [ + 4, + 9 + ], + [ + 8, + 5 + ] + ], + "exceptional_type": [ + 17, + 12 + ] + }, + { + "cheap_pair": [ + [ + 5, + 8 + ], + [ + 9, + 4 + ] + ], + "exceptional_type": [ + 12, + 17 + ] + }, + { + "cheap_pair": [ + [ + 5, + 8 + ], + [ + 12, + 1 + ] + ], + "exceptional_type": [ + 9, + 20 + ] + } + ], + "low_tariff_exceptional_types": [ + [ + 9, + 20 + ], + [ + 12, + 17 + ], + [ + 17, + 12 + ], + [ + 20, + 9 + ] + ], + "sharp_invoice_floor": 45 +} diff --git a/research/p112-five-group-projector-lift/PROOF.md b/research/p112-five-group-projector-lift/PROOF.md new file mode 100644 index 0000000000..97829214b8 --- /dev/null +++ b/research/p112-five-group-projector-lift/PROOF.md @@ -0,0 +1,159 @@ +# A sharp low-tariff floor on five P112 triads + +**Theorem.** Every finite rational rank-one decomposition of `I15` on the +five triads below has total whole-group invoice at least 45 if each nonzero +term has tariff at most 3. The direct 15-copy decomposition attains 45. +There is no restriction on the number of terms, coefficient sizes or +rational denominators. A common nonzero scalar endpoint is equivalent by +rescaling one factor family, which preserves supports and tariffs. + +The ordered physical triads A, B, C, D, E have ports + +``` +A [10,18,93] B [6,36,74] C [13,23,102] +D [41,73,88] E [30,50,87]. +``` + +Every pair has nonzero physical pairing, so the strict endpoint on three +payload coordinates per group is exactly `I15`. Tariffs charge the complete +physical triad spaces touched by a factor, regardless of its active payload +coordinates. This theorem does not cover factors costing 4 or more, other +physical geometries, or a full P112 decoder. + +## 1. The rational auxiliary lift + +Form the 15-by-15 rational matrix `H` from the literal binary dot pairings +between the authenticated physical labels, interpreted as rational zeros +and ones. Replace each off-diagonal block between different groups in +`{A,C,D}` by `J3/3`. Those original blocks are all `J3`; leave all other +entries unchanged. In particular `H_gg=I3`. + +For nonempty group masks `s,t`, write `h(s,t)=rank_Q H[s,t]` and let +`rho(s,t)` be the actual binary whole-group tariff. The replay checks all +961 ordered rectangles. None has tariff zero. There are 14 tariff-1, +20 tariff-2 and 273 tariff-3 rectangles. For every rectangle of tariff at +most 3, `h<=rho`, except exactly these four: + +| Source mask | Reader mask | Lift rank | Tariff | +|---:|---:|---:|---:| +| 9 | 20 | 4 | 3 | +| 12 | 17 | 4 | 3 | +| 17 | 12 | 4 | 3 | +| 20 | 9 | 4 | 3 | + +Masks use A through E as bits 0 through 4. Each exceptional rectangle has +disjoint source and reader group sets. The matrix is not a universal +rank-domination certificate: higher tariffs have additional exceptions. + +Given a payload factor `u v^T`, form its 45-by-45 lift `A` with block + +``` +A_gh = (u_g v_h^T) tensor H_gh. +``` + +For exact nonzero group supports `(s,t)`, this equals +`D_u H[s,t] D_v^T`, where each group block of `D_u` is `u_g tensor I3` +and similarly for `D_v`. These blocks have full column rank 3. Consequently +`rank(A)=h(s,t)`. This uses exact nonzero group supports and holds for +arbitrary mixtures of payload coordinates. The lift of the endpoint is +`I45`, since all off-diagonal endpoint blocks vanish and `H_gg=I3`. + +## 2. A projector counts repeated exceptional rectangles + +**Surplus-rank lemma.** Suppose `I_n=sum_t A_t` and put +`R=sum_t rank(A_t)`. If `k` selected summands have the same disjoint +row/column support rectangle `(S,T)`, and each has rank `r`, then + +``` +R-n >= r k. +``` + +Choose minimal rank factorizations `A_t=X_t Y_t`, concatenate the X blocks +and stack the Y blocks. Then `XY=I_n`, so `P=I_R-YX` is an idempotent of +rank `R-n`. Each selected factorization can respect its supports: `X_t` +has zero rows outside S and `Y_t` has zero columns outside T. Because +`S intersect T` is empty, `Y_t X_s=0` for every pair of selected summands, +including equal indices. Their principal block in P is therefore `I_(rk)`, +which proves the bound. It does not require a rank-one projector or a +bound on the number of original payload factors. + +Let `b` be the total number of exceptional lifted terms and let +`k_1,...,k_4` be their multiplicities in the four types. If the invoice is C, +the complete low-tariff census gives `R<=C+b`. When `b=0`, the endpoint +rank immediately gives `45<=R<=C`. Otherwise the surplus-rank lemma gives + +``` +R-45 >= 4 max_i k_i >= sum_i k_i = b. +``` + +Combining this with `R<=C+b` proves `C>=45`. The direct copies each have +whole-group tariff 3, so the bound is sharp in the stated class. + +For example, this excludes 17 terms with four tariff-1 and thirteen +tariff-3 terms (invoice 43), as well as three tariff-1, one tariff-2 and +thirteen tariff-3 terms (invoice 44). Their original complementary +projector has rank 2; no rank-one assumption enters the theorem. + +## 3. Secondary sixteen-term branch certificate + +The package also retains the more detailed census that motivated the +all-term argument. Consider exactly 16 terms, two tariff 1 and fourteen +tariff 3. Write `UV^T=I15`. Then `P=I16-V^T U` has rank 1 and trace 1. +Every term with disjoint group supports has `P_tt=1`; every tariff-1 type +is disjoint. Two nonzero diagonal entries of a rank-one matrix require +both cross entries nonzero. Thus the two cheap types must cross in both +directions and must be distinct. + +Their diagonal entries total 2, so a common-footprint term must have a +nonzero projector diagonal to make the full trace 1. That term must cross +both cheap types. These necessary conditions reduce the 91 unordered +pairs of distinct cheap types to exactly 21 branches. Every disjoint +regular term must also cross both cheap types. + +In 17 branches all permitted regular types satisfy `h<=3`. The other four +branches each allow only one exceptional type: + +| Cheap pair | Exceptional `(source,reader)` masks | +|---|---:| +| `(1,12), (8,5)` | `(20,9)` | +| `(4,9), (8,5)` | `(17,12)` | +| `(5,8), (9,4)` | `(12,17)` | +| `(5,8), (12,1)` | `(9,20)` | + +Two copies of one disjoint type would give an `I2` principal block in the +rank-one projector, so at most one exceptional term occurs. With none, +the lifted rank sum is at most 44. With one, it is at most 45 and must +equal 45. Equality in an identity decomposition's rank sum forces every +summand to be idempotent: minimal rank factorizations concatenate to +square matrices `XY=I45`, hence `YX=I45`, and each diagonal block gives +`Y_t X_t=I`. But the exceptional rank-4 term is nonzero and square-zero +because its supports are disjoint. This is a contradiction. + +This secondary census is independently replayed, but is not a premise +of the stronger theorem in Section 2. No earlier solver receipt is used. + +## Replay, controls and attribution + +Both `verify.py` and `independent.py` use Python's standard library and +accept `--repo-root PATH`. They authenticate the local candidate and +certificate, archive container and exact archived label member, then +regenerate all prices and lift ranks. They print JSON without writes, +Git access, sibling imports or solver dependencies. + +The primary uses Fraction elimination and exact mixed rational fixtures. +The independent replay uses the integer matrix `3H`, primitive integer +elimination and reverse-order enumeration. Both verify the complete +low-tariff exception catalogue and the secondary branch certificate. + +Controls include direct-copy attainment and the literal lifted identity, +a rational redundant frame, all four rank-4 square-zero types, and exact +surplus-projector fixtures. The independent fixture tensors +`I2=E11+E22+E12-E12` with `I4`: its two same-type rank-4 summands force an +`I8` projector block. Mutations show that the division by 3 and the own +identity blocks are material. + +Separate AI agents developed and reviewed the proof and independently +implemented the two exact replays. This is AI-assisted research; human +mathematical admission remains open. A cheaper construction must include +a tariff-4-or-higher term or change geometry. No improved supplier or +full global cost-296 construction is claimed. diff --git a/research/p112-five-group-projector-lift/README.md b/research/p112-five-group-projector-lift/README.md new file mode 100644 index 0000000000..a52df15c54 --- /dev/null +++ b/research/p112-five-group-projector-lift/README.md @@ -0,0 +1,66 @@ +# A sharp five-group P112 floor for low-tariff factors + +On the five explicit triads in [CANDIDATE.json](CANDIDATE.json), every finite +rational `I15` decoder using only whole-group tariffs at most 3 costs at +least **45**. Direct copies attain 45. The result allows any number of +terms and arbitrary rational coefficients, denominators and payload mixing. + +The auxiliary lift has four exceptional support rectangles. A projector +rank argument bounds how often they can occur, proving the floor even +though the lift does not dominate them individually. A cheaper decoder +on these triads must use at least one term costing 4 or more. + +This is a scoped obstruction, not a cheaper construction. Frames containing +higher-tariff terms remain outside the theorem; the general local minimum +and global 296 target are unresolved. No improved native supplier or +multiplication bound is claimed. + +## Evidence and replay + +[PROOF.md](PROOF.md) proves the all-term theorem. [CERTIFICATE.json](CERTIFICATE.json) +stores the integer matrix `3H` and the complete four-defect catalogue. Two +standard-library replays independently check all 961 support rectangles, +including all 20 tariff-2 rectangles. The original 21-branch exclusion for +16 terms (two tariff 1, fourteen tariff 3) is retained as secondary evidence. + +From the repository root with Python 3.12: + +```sh +python3 -I -O -B research/p112-five-group-projector-lift/verify.py +python3 -I -O -B research/p112-five-group-projector-lift/independent.py +python3 scripts/research_package.py --package research/p112-five-group-projector-lift +``` + +Both mathematical replays are read-only and accept `--repo-root PATH`. +A Git-free export needs only this package and the exact archived input path +in [VERIFY.json](VERIFY.json). The container/member and local data are +hash-authenticated. No unpublished geometry list, predecessor partition, +solver or search output is required. Registered metadata checks additionally +resolve historical provenance through Git. + +The primary uses Fraction elimination; the independent checker uses +primitive integer elimination and reverse-order enumeration. Neither +imports the other. Controls include direct-copy attainment, a literal +45-dimensional lifted identity, rational factors, repeated-type surplus +projectors, and material rank/endpoint mutations. + +## Open next questions + +[TASK.json](TASK.json) asks whether higher-tariff terms or a changed geometry +can yield a fully priced saving. The auxiliary lift has additional excess +rectangles at tariffs 4 and higher, so the present counting argument must +not be extrapolated to those families. + +## Sources and credit + +The binary labels come from the immutable selected replay archive recorded +in [SOURCES.json](SOURCES.json), with its original attribution retained. +The five custom triads are explicit package data. The broader rational +decoder investigation follows flyingviper's [PR 2757](https://github.com/CrocSwap/integer-mult-bounds/pull/2757), +historical head `18da668a4f248f5c0cf3fc94355068ead4db3476`; that head is context, +not a replay dependency or scientific admission. This package starts from +canonical main `d8e0f83f00191df62174b641e9fff055c357f641`, priority revision 6. + +Author: flyingviper, with substantial OpenAI Codex assistance. Separate AI +agents developed and reviewed the proof and independent implementations. +Human mathematical review remains open. License: Apache-2.0. diff --git a/research/p112-five-group-projector-lift/SOURCES.json b/research/p112-five-group-projector-lift/SOURCES.json new file mode 100644 index 0000000000..521c5ccd49 --- /dev/null +++ b/research/p112-five-group-projector-lift/SOURCES.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + } + ], + "candidate": { + "path": "CANDIDATE.json", + "sha256": "dfb886d683dfef7b54ba582ebec5baf2cf84962915009fc28d8f9252fc8a7707", + "description": "New explicit custom five-triad ports, sharp all-term low-tariff theorem domain, and secondary sixteen-term profile." + }, + "certificate": { + "path": "CERTIFICATE.json", + "sha256": "127260a387bef913d544558299946e61106012423aaf057b268149de75d2efe9", + "description": "Integer 3H matrix, complete four-defect low-tariff catalogue, sharp invoice floor, and secondary finite branch expectations; both replays regenerate them." + }, + "archive_member": { + "path": "candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "predecessor_context": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2757", + "head": "18da668a4f248f5c0cf3fc94355068ead4db3476", + "author": "flyingviper", + "usage": "Historical whole-group rational decoder investigation only; neither its candidate partition nor its unpublished results are replay inputs." + }, + "implementation_provenance": { + "primary": "Independent Fraction elimination, low-pivot binary rank and full rational fixture lifts.", + "independent": "Separate primitive integer elimination on 3H and reverse-order rectangle enumeration; no primary imports.", + "credits": "Physical labels retained in the selected replay archive; predecessor attribution remains in that immutable archive. New candidate/lift and both implementations by flyingviper with substantial OpenAI Codex assistance.", + "license": "Apache-2.0" + } +} diff --git a/research/p112-five-group-projector-lift/TASK.json b/research/p112-five-group-projector-lift/TASK.json new file mode 100644 index 0000000000..e855d898a6 --- /dev/null +++ b/research/p112-five-group-projector-lift/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 6, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the sharp invoice floor 45 for every finite rational I15 factorization on five custom P112 triads when every nonzero term has whole-group tariff at most 3.", + "scope_change_reason": "Explicit user-directed rational decoder research. A rank-surplus projector counts repeated exceptional lift rectangles and closes every term count in the low-tariff family, beyond the motivating sixteen-term profile.", + "bottleneck_link": "Any local saving below the 45 direct-copy baseline must use a term costing at least 4. This scoped result supplies no global 296 decoder or supplier.", + "budget_minutes": 60, + "stop_rule": "Finish the all-term lift proof and two independent read-only replays. Further construction must include a higher-tariff term or change geometry.", + "outcome": "negative-result", + "evidence": "All 961 physical/rational support ranks, including 20 tariff-2 rectangles and exactly four disjoint rank-4 low-tariff defects; sharp surplus-projector controls; direct-copy attainment at 45. Secondary census covers all 91 cheap-type pairs and 21 sixteen-term branches.", + "author": "flyingviper", + "ai_assistance": "Substantial OpenAI Codex assistance. Separate AI agents developed and independently checked the algebra and two distinct exact implementations.", + "open_questions": [ + { + "question": "Can a factorization containing one or more tariff-4-or-higher terms give a verified saving on these triads?", + "why_it_matters": "All finite decompositions using only tariffs at most 3 are now excluded below 45; the general local minimum is not established.", + "first_step": "Name a higher-tariff profile and its complete invoice, then derive an applicable defect or coefficient test.", + "blocked_by": "The lift has additional excessive rectangles outside the low-tariff domain." + }, + { + "question": "Does another physical geometry admit a useful rational decoder with a complete global cost ledger?", + "why_it_matters": "This theorem applies only to the five literal triads and does not reach the global 296 target.", + "first_step": "State the changed geometry and attainable local saving before expanding synthesis.", + "blocked_by": "No cheaper rational construction or full supplier has been verified." + } + ], + "selected_kappa_unchanged": "0.001672660197076918", + "result": { + "excluded_profile": { + "nonzero_rank_one_terms": 16, + "whole_group_tariff_histogram": { + "1": 2, + "3": 14 + } + }, + "branches_excluded": 21, + "local_direct_copy_baseline": 45, + "new_cheaper_construction": false, + "global_target_296_met": false, + "maximum_per_term_tariff": 3, + "term_count": "any finite number", + "sharp_minimum_invoice": 45, + "direct_copy_attainment": true + }, + "scope": "Five literal custom triads; arbitrary finite term count and rational coefficients; exact I15 endpoint or a common nonzero scalar. Every nonzero factor must have whole-group tariff at most 3.", + "scientific_review_status": "Independent AI proof/code review and exact replay; no claim of human scientific admission.", + "remaining_obligations": [ + "Factorizations containing a tariff-4-or-higher term remain open in this package.", + "No improved full P112 decoder, native implementation, supplier or multiplication bound." + ] +} diff --git a/research/p112-five-group-projector-lift/VERIFY.json b/research/p112-five-group-projector-lift/VERIFY.json new file mode 100644 index 0000000000..f2abe23645 --- /dev/null +++ b/research/p112-five-group-projector-lift/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Authenticate candidate/certificate/archive/member; rebuild all 961 rank comparisons including tariffs 0 and 2 and the complete four-defect low-tariff catalogue; sharp surplus-projector control, literal I45/direct-copy attainment, rational and mutation controls; secondary 21-branch census; no writes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 60, + "checks": "Independently regenerate all 961 ranks using integer 3H, verify all-term four-defect premises and exact rank-8 repeated-type projector control, direct invoice 45 and secondary 91-pair/21-branch census; no writes." + } + ] +} diff --git a/research/p112-five-group-projector-lift/independent.py b/research/p112-five-group-projector-lift/independent.py new file mode 100644 index 0000000000..c9b663ce59 --- /dev/null +++ b/research/p112-five-group-projector-lift/independent.py @@ -0,0 +1,130 @@ +"""Independent integer-rank replay of the all-term low-tariff case30 floor. + +The producer, its output, and its rank helpers are not imported. This replay +uses 3H, primitive integer row elimination, and reverse-order mask enumeration. +""" +from pathlib import Path +from itertools import product +from math import gcd +from functools import reduce +from hashlib import sha256 +import argparse,io,json,tarfile + +HERE=Path(__file__).resolve().parent +CANDIDATE_HASH='dfb886d683dfef7b54ba582ebec5baf2cf84962915009fc28d8f9252fc8a7707' +CERTIFICATE_HASH='127260a387bef913d544558299946e61106012423aaf057b268149de75d2efe9' +PORTS=((10,18,93),(6,36,74),(13,23,102),(41,73,88),(30,50,87)) +ARCHIVE='f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6' +MEMBER='candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' +MEMBER_HASH='c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +def check(p,s): + if not p:raise ValueError(s) +def irank(rows): + pivots={} + for row in rows: + v=list(row) + for p,w in sorted(pivots.items()): + if v[p]: + a,b=v[p],w[p];v=[b*x-a*y for x,y in zip(v,w)] + d=reduce(gcd,v,0) + if d:v=[x//d for x in v] + p=next((j for j,x in enumerate(v) if x),None) + if p is not None: + d=reduce(gcd,v,0)*(1 if v[p]>0 else -1) + pivots[p]=[x//d for x in v] + return len(pivots) +def binary_rank(rows): + piv={} + for row in rows: + while row: + p=row.bit_length()-1 + if p not in piv:piv[p]=row;break + row^=piv[p] + return len(piv) +def run(repo): + raw_candidate=(HERE/'CANDIDATE.json').read_bytes();raw_certificate=(HERE/'CERTIFICATE.json').read_bytes() + check(sha256(raw_candidate).hexdigest()==CANDIDATE_HASH,'candidate pin') + check(sha256(raw_certificate).hexdigest()==CERTIFICATE_HASH,'certificate pin') + candidate=json.loads(raw_candidate);certificate=json.loads(raw_certificate) + check(candidate['ports']==list(map(list,PORTS)) and candidate['payload_dimensions']==[3]*5 and candidate['endpoint']=='I15','candidate ports and endpoint') + check(candidate['excluded_profile']=={'nonzero_rank_one_terms':16,'whole_group_tariff_histogram':{'1':2,'3':14}},'candidate profile') + check(candidate['theorem']=={'term_count':'any finite number','maximum_per_term_whole_group_tariff':3,'minimum_total_invoice':45,'attained_by_direct_copies':True},'all-term theorem scope') + raw=(repo/'research/community-frontier1094-audit/selected-replay.tar.gz').read_bytes() + check(sha256(raw).hexdigest()==ARCHIVE,'archive pin') + with tarfile.open(fileobj=io.BytesIO(raw)) as stream:physical=stream.extractfile(MEMBER).read() + check(sha256(physical).hexdigest()==MEMBER_HASH,'member pin') + recipes=json.loads(physical)['recipes'];labels={r['port']:r['q'] for r in recipes} + check(len(recipes)==len(labels)==112 and len(set(labels.values()))==112,'label uniqueness') + E=[[labels[p] for p in pp] for pp in PORTS];flat=sum(E,[]) + parity=lambda x,y:(x&y).bit_count()%2 + check(all(parity(x,y)==int(i==j) for e in E for i,x in enumerate(e) for j,y in enumerate(e)),'own physical identity') + H=[[3*parity(x,y) for y in flat] for x in flat] + for g in (0,2,3): + for h in (0,2,3): + if g!=h: + for i in range(3*g,3*g+3): + for j in range(3*h,3*h+3): + check(H[i][j]==3,'triangle rank1 block');H[i][j]=1 + check(certificate['schema_version']==1 and certificate['auxiliary_dimension']==3 and certificate['matrix_denominator']==3,'certificate format') + check(certificate['scaled_bilinear_matrix']==H,'independently regenerated scaled matrix') + ix={s:[i for i in range(15) if s>>(i//3)&1] for s in range(1,32)} + rho={};ranks={} + for s,t in product(range(31,0,-1),repeat=2): + rho[s,t]=binary_rank(sum(parity(flat[i],flat[j])<0 for g in range(5) for h in range(5)),'strict endpointI15') + cheap=sorted(st for st,c in rho.items() if c==1);regular=sorted(st for st,c in rho.items() if c==3) + common=[(s,t) for s,t in regular if s&t] + check(len(cheap)==14 and len(regular)==273 and len(common)==165,'full price domains') + check(all(ranks[p]==1 for p in cheap),'cheap lift rank') + check(all(ranks[p]<=3 for p in common),'common footprint domination') + check(min(rho.values())==1 and sum(c==2 for c in rho.values())==20,'complete tariff0/2 domains') + low_defects=sorted(st for st,c in rho.items() if c<=3 and ranks[st]>c) + check(low_defects==[(9,20),(12,17),(17,12),(20,9)],'all low-tariff defects') + check(all(rho[s,t]==3 and ranks[s,t]==4 and not(s&t) for s,t in low_defects),'four disjoint rank4 defects') + check(certificate['low_tariff_exceptional_types']==list(map(list,low_defects)) and certificate['sharp_invoice_floor']==45,'all-term finite certificate') + def crosses(p,q):return bool(p[0]&q[1]) and bool(q[0]&p[1]) + branches={};excluded_pairs=0 + for p in cheap: + for q in cheap: + if p>=q:continue + if not crosses(p,q) or not any(crosses(t,p) and crosses(t,q) for t in common): + excluded_pairs+=1;continue + allowed=[t for t in regular if t[0]&t[1] or (crosses(t,p) and crosses(t,q))] + exceptional=[t for t in allowed if ranks[t]>3] + check(len(exceptional)<=1,'only one exceptional type per branch') + if exceptional: + s,t=exceptional[0] + check(not(s&t) and ranks[s,t]==4,'rank4 squarezero type') + # Two equal disjoint types force an I2 complement minor. + check(irank([[1,0],[0,1]])==2,'rank1 projector disallows duplicate') + branches[p,q]=exceptional + check(len(branches)==21 and excluded_pairs==70,'complete91 cheap type pairs') + exceptional=sorted((p,q,tuple(ex)) for (p,q),ex in branches.items() if ex) + check(len(exceptional)==4,'exactly four rank-tight branches') + check(sorted(ex[0] for ex in branches.values() if ex)==[(9,20),(12,17),(17,12),(20,9)],'exceptional types') + check(certificate['expected_counts']=={'rectangles':961,'cost1_types':14,'cost3_types':273,'common_cost3_types':165,'cheap_pair_candidates':91,'branches':21,'direct_exclusions':17,'rank_tight_exclusions':4,'cost0_types':0,'cost2_types':20,'low_tariff_exceptional_types':4},'certificate counts') + saved={(tuple(x['cheap_pair'][0]),tuple(x['cheap_pair'][1])):tuple(x['exceptional_type']) for x in certificate['exceptional_branches']} + actual={(p,q):ex[0] for (p,q),ex in branches.items() if ex} + check(saved==actual,'independently regenerated exceptional branches') + # Diagonal I15 terms lift to 3I45, total rank45. Division by3 matters. + check(all(H[3*g+i][3*g+j]==3*int(i==j) for g in range(5) for i in range(3) for j in range(3)),'lifted3I45') + untuned=[[3*parity(x,y) for y in flat] for x in flat] + check(irank([[untuned[i][j] for j in ix[5]] for i in ix[12]])==4 and ranks[12,5]==3,'mutation changes material rank') + # Different integer control: tensor I2=E11+E22+E12-E12 with I4. + X0=((1,0,1,-1),(0,1,0,0));Y0=((1,0),(0,1),(0,1),(0,1)) + X=[[X0[i//4][j//4]*int(i%4==j%4) for j in range(16)] for i in range(8)] + Y=[[Y0[i//4][j//4]*int(i%4==j%4) for j in range(8)] for i in range(16)] + mul=lambda A,B:[[sum(x*y for x,y in zip(a,b)) for b in zip(*B)] for a in A] + check(mul(X,Y)==[[int(i==j) for j in range(8)] for i in range(8)],'tensor surplus endpoint') + YX=mul(Y,X);P=[[int(i==j)-YX[i][j] for j in range(16)] for i in range(16)] + check(irank(P)==8 and mul(P,P)==P,'integer surplus projector rank8') + check([[P[i][j] for j in range(8,16)] for i in range(8,16)]==[[int(i==j) for j in range(8)] for i in range(8)],'two same-type rank4 blocks force I8') + return {'status':'PASS','ports':PORTS,'physical_labels':E,'archive_sha256':ARCHIVE,'member_sha256':MEMBER_HASH, + 'rectangles':len(ranks),'cost0_types':0,'cost2_types':20,'low_tariff_exceptional_types':low_defects,'all_term_low_tariff_invoice_floor':45,'attaining_direct_invoice':45,'surplus_projector_control_rank':8,'cheap_pair_domain':91,'cheap_pairs_ruled_out_by_projector':excluded_pairs, + 'branches':21,'direct_rank_contradictions':17,'rank_tight_nilpotent_contradictions':4, + 'exceptional_branches':exceptional,'scope':'Any finite rational I15 frame on these five triads whose individual whole-group tariffs are at most 3 costs at least 45. Frames containing tariff4-or-higher terms and the global target remain outside this result.', + 'source_sha256':sha256(Path(__file__).read_bytes()).hexdigest()} +if __name__=='__main__': + parser=argparse.ArgumentParser();parser.add_argument('--repo-root',type=Path,default=HERE.parents[1]) + args=parser.parse_args();print(json.dumps(run(args.repo_root),indent=2)) diff --git a/research/p112-five-group-projector-lift/verify.py b/research/p112-five-group-projector-lift/verify.py new file mode 100644 index 0000000000..fa76de407c --- /dev/null +++ b/research/p112-five-group-projector-lift/verify.py @@ -0,0 +1,205 @@ +"""Solver-free sharp cost-45 floor for arbitrary low-tariff case30 frames. + +No producer imports or writes. Physical labels are authenticated from the retained +archive. All finite term counts are covered when each whole-group tariff is at most 3. +""" +from pathlib import Path +from fractions import Fraction as F +from itertools import combinations +from hashlib import sha256 +import argparse, io, json, tarfile, time + +HERE=Path(__file__).resolve().parent +PORTS=[[10,18,93],[6,36,74],[13,23,102],[41,73,88],[30,50,87]] +PINS={'candidate':'dfb886d683dfef7b54ba582ebec5baf2cf84962915009fc28d8f9252fc8a7707', + 'certificate':'127260a387bef913d544558299946e61106012423aaf057b268149de75d2efe9', + 'archive':'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6', + 'member':'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa'} +MEMBER='candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' + +def need(p,m): + if not p:raise ValueError(m) + +def auth(raw,pin): + need(sha256(raw).hexdigest()==pin,'authenticated input SHA256') + return raw + +def qrank(matrix): + rows=[[F(x) for x in row] for row in matrix] + if not rows:return 0 + k=0 + for j in range(len(rows[0])): + p=next((i for i in range(k,len(rows)) if rows[i][j]),None) + if p is None:continue + rows[k],rows[p]=rows[p],rows[k];scale=rows[k][j] + rows[k]=[v/scale for v in rows[k]] + for i in range(k+1,len(rows)): + scale=rows[i][j] + if scale:rows[i]=[a-scale*b for a,b in zip(rows[i],rows[k])] + k+=1 + if k==len(rows):break + return k + +def brank(rows): + piv={} + for x in rows: + while x: + j=(x&-x).bit_length()-1 + if j in piv:x^=piv[j] + else:piv[j]=x;break + return len(piv) + +def dot(x,y):return sum(a*b for a,b in zip(x,y)) +def product(A,B):return [[dot(a,b) for b in zip(*B)] for a in A] +def transpose(A):return list(map(list,zip(*A))) +def indices(mask):return [j for j in range(15) if mask>>(j//3)&1] +def rectangle(H,s,t):return [[H[i][j] for j in indices(t)] for i in indices(s)] + +def read_geometry(repo): + candidate=json.loads(auth((HERE/'CANDIDATE.json').read_bytes(),PINS['candidate'])) + need(candidate['ports']==PORTS and candidate['payload_dimensions']==[3]*5 and candidate['endpoint']=='I15','literal package candidate') + need(candidate['excluded_profile']=={'nonzero_rank_one_terms':16,'whole_group_tariff_histogram':{'1':2,'3':14}},'literal excluded profile') + need(candidate['theorem']=={'term_count':'any finite number','maximum_per_term_whole_group_tariff':3,'minimum_total_invoice':45,'attained_by_direct_copies':True},'all-term low-tariff theorem scope') + raw=auth((repo/'research/community-frontier1094-audit/selected-replay.tar.gz').read_bytes(),PINS['archive']) + with tarfile.open(fileobj=io.BytesIO(raw)) as stream: + member=stream.extractfile(MEMBER);need(member is not None,'exact archive member') + physical=auth(member.read(),PINS['member']) + recipes=json.loads(physical)['recipes'];q={r['port']:r['q'] for r in recipes} + need(set(q)==set(range(112)) and len(set(q.values()))==112,'112 distinct labels') + E=[[q[p] for p in group] for group in PORTS] + need(len(set(sum(PORTS,[])))==15,'disjoint selected ports') + need(all(((x&y).bit_count()&1)==int(i==j) for group in E for i,x in enumerate(group) for j,y in enumerate(group)),'orthonormal physical triads') + union=[[x for g in range(5) if s>>g&1 for x in E[g]] for s in range(32)] + price=[[brank(sum((((x&y).bit_count()&1)<0 for g,h in combinations(range(5),2)),'all cross endpoints constrained') + return E,price + +def lift(u,v,H): + # Index physical group, payload coordinate, auxiliary coordinate. + out=[[F(0)]*45 for _ in range(45)] + for g in range(5): + for h in range(5): + for a in range(3): + for b in range(3): + c=u[3*g+a]*v[3*h+b] + if c: + for x in range(3): + for y in range(3):out[9*g+3*a+x][9*h+3*b+y]=c*H[3*g+x][3*h+y] + return out + +def support(v):return sum(1<>(i//3)&1 else F(0) for i in range(15)] + v=[F((2,-1,4)[i%3],3) if t>>(i//3)&1 else F(0) for i in range(15)] + A=lift(u,v,H) + need(support(u)==s and support(v)==t and qrank(A)==4,'mixed rational exceptional exact rank4') + need(not any(any(row) for row in product(A,A)),'exceptional square zero') + need(A!=product(A,A),'exceptional not idempotent') + nilpotents.append([s,t]) + # A genuine rational redundant frame with arbitrary cross-group mixing. + a=[F(0)]*15;a[0]=F(1);a[6]=F(2) + t=[F(0)]*15;t[0]=F(1,2);t[9]=F(-1,3) + U=[unit(j) for j in range(15)]+[a] + V=[[F(i==j)-a[j]*t[i] for i in range(15)] for j in range(15)]+[t] + endpoint=[[sum(u[i]*v[j] for u,v in zip(U,V)) for j in range(15)] for i in range(15)] + need(endpoint==[[F(i==j) for j in range(15)] for i in range(15)],'rational frame exact I15') + P=[[F(i==j)-dot(V[i],U[j]) for j in range(16)] for i in range(16)] + need(qrank(P)==1 and product(P,P)==P,'rank1 complementary projector fixture') + total=[[F(0)]*45 for _ in range(45)] + charges=[] + for u,v in zip(U,V): + s,t=support(u),support(v);A=lift(u,v,H) + need(qrank(A)==qrank(rectangle(H,s,t)),'injective mixed factor lift') + total=[[x+y for x,y in zip(a,b)] for a,b in zip(total,A)];charges.append(price[s][t]) + need(total==eye and sum(charges)>=45,'rational positive fixture not claimed cost44') + # Equality of rank-sum can hold for nonorthogonal idempotents. + X=[[F(1),F(1,2),F(0)],[F(0),F(1),F(1,3)],[F(0),F(0),F(1)]] + Y=[[F(1),F(-1,2),F(1,6)],[F(0),F(1),F(-1,3)],[F(0),F(0),F(1)]] + need(product(X,Y)==[[F(i==j) for j in range(3)] for i in range(3)],'invertible tight fixture') + for j in range(3): + A=[[X[i][j]*Y[j][k] for k in range(3)] for i in range(3)] + need(product(A,A)==A and qrank(A)==1,'tight summand is idempotent') + need(qrank([[1,0],[0,1]])==2,'duplicate disjoint type projector obstruction') + original=[row[:] for row in H] + for g,h in ((0,2),(0,3),(2,0),(2,3),(3,0),(3,2)): + for i in range(3*g,3*g+3): + for j in range(3*h,3*h+3):original[i][j]=1 + need(qrank(rectangle(original,12,5))==4 and qrank(rectangle(H,12,5))==3,'division by3 is material') + corrupt=[row[:] for row in H];corrupt[0][0]=2 + need(corrupt[:3]!=H[:3] and lift(unit(0),unit(0),corrupt)!=lift(unit(0),unit(0),H),'own-block mutation changes lifted identity') + # Sharp repeated-type surplus projector: I2 = E11+E22+E12-E12. + X=[[F(1),F(0),F(1),F(-1)],[F(0),F(1),F(0),F(0)]] + Y=[[F(1),F(0)],[F(0),F(1)],[F(0),F(1)],[F(0),F(1)]] + need(product(X,Y)==[[1,0],[0,1]],'surplus control endpoint') + YX=product(Y,X);P=[[F(i==j)-YX[i][j] for j in range(4)] for i in range(4)] + need(qrank(P)==2 and product(P,P)==P,'surplus control projector rank') + need([[P[i][j] for j in (2,3)] for i in (2,3)]==[[1,0],[0,1]],'same disjoint type I2 block') + return {'baseline_invoice':45,'rational_positive_invoice':sum(charges),'nilpotent_rank4_controls':nilpotents, + 'controls':['same-type surplus projector','literal I45','mixed rational redundant frame','exact factor-lift ranks','rank1 projector','tight idempotents','duplicate projector rank2','critical division by3','own-block mutation']} + +def run(repo): + start=time.monotonic();E,price=read_geometry(repo);labels=sum(E,[]) + H=[[F((x&y).bit_count()&1) for y in labels] for x in labels] + for g,h in combinations((0,2,3),2): + need(all(H[i][j]==1 for i in range(3*g,3*g+3) for j in range(3*h,3*h+3)),'triangle all-ones crossblock') + for i in range(3*g,3*g+3): + for j in range(3*h,3*h+3):H[i][j]=H[j][i]=F(1,3) + cert=json.loads(auth((HERE/'CERTIFICATE.json').read_bytes(),PINS['certificate'])) + need(cert['schema_version']==1 and cert['auxiliary_dimension']==3 and cert['matrix_denominator']==3,'certificate format') + need(cert['scaled_bilinear_matrix']==[[int(3*x) for x in row] for row in H],'literal scaled lift matrix') + need(all(H[3*g+i][3*g+j]==int(i==j) for g in range(5) for i in range(3) for j in range(3)),'own I3 blocks') + lifted={(s,t):qrank(rectangle(H,s,t)) for s in range(1,32) for t in range(1,32)} + cheap=[(s,t) for s,t in lifted if price[s][t]==1] + regular=[(s,t) for s,t in lifted if price[s][t]==3] + common=[(s,t) for s,t in regular if s&t] + need((len(cheap),len(regular),len(common))==(14,273,165),'complete type counts') + need(all(not(s&t) for s,t in cheap),'every cheap type has disjoint supports') + need(all(lifted[x]<=1 for x in cheap),'all cost1 dominated') + need(all(lifted[x]<=3 for x in common),'all common-footprint cost3 dominated') + cost2=[x for x in lifted if price[x[0]][x[1]]==2] + need(len(cost2)==20 and all(price[s][t]>=1 for s,t in lifted),'all nonzero tariff domains including zero/2') + low_bad=sorted((s,t) for s,t in lifted if price[s][t]<=3 and lifted[s,t]>price[s][t]) + need(low_bad==[(9,20),(12,17),(17,12),(20,9)],'complete all-term low-tariff exceptional catalogue') + need(all(not(s&t) and price[s][t]==3 and lifted[s,t]==4 for s,t in low_bad),'four disjoint rank4 excess1 rectangles') + need(cert['low_tariff_exceptional_types']==list(map(list,low_bad)) and cert['sharp_invoice_floor']==45,'all-term certificate data') + branches=[] + for p,q in combinations(cheap,2): + if not(p[0]&q[1] and q[0]&p[1]):continue + comp=[(s,t) for s,t in common if s&p[1] and s&q[1] and t&p[0] and t&q[0]] + if not comp:continue + zero=[(s,t) for s,t in regular if not s&t and s&p[1] and s&q[1] and t&p[0] and t&q[0]] + bad=[(s,t) for s,t in zero if lifted[s,t]>3] + need(len(bad)<=1 and all(lifted[x]==4 for x in bad),'at most one exceptional type, excess1') + branches.append({'cheap_pair':[list(p),list(q)],'compatible_zero_footprint':list(map(list,zero)), + 'exceptional_types':list(map(list,bad)), + 'exclusion':'rank-tight nonzero square-zero summand' if bad else 'rank sum at most44'}) + need(len(branches)==21,'complete cheap-pair branch count') + exceptional=sorted({tuple(x) for b in branches for x in b['exceptional_types']}) + need(exceptional==[(9,20),(12,17),(17,12),(20,9)],'exact exceptional four types') + need(all(not(s&t) for s,t in exceptional),'every exceptional type is square-zero by support') + need(sum(bool(b['exceptional_types']) for b in branches)==4,'17 direct and4 tight exclusions') + need(cert['exceptional_branches']==[{'cheap_pair':b['cheap_pair'],'exceptional_type':b['exceptional_types'][0]} for b in branches if b['exceptional_types']],'literal exceptional branch certificate') + need(cert['expected_counts']=={'rectangles':961,'cost1_types':14,'cost3_types':273,'common_cost3_types':165,'cheap_pair_candidates':91,'branches':21,'direct_exclusions':17,'rank_tight_exclusions':4,'cost0_types':0,'cost2_types':20,'low_tariff_exceptional_types':4},'certificate coverage counts') + ctl=controls(H,price,exceptional) + return {'status':'PASS','ports':PORTS,'physical_labels':E,'pins':PINS, + 'lift_matrix':[[str(x) for x in row] for row in H],'lift_full_rank':qrank(H), + 'rectangles_checked':961,'cost0_types':0,'cost2_types':20,'low_tariff_exceptional_types':low_bad,'all_term_low_tariff_invoice_floor':45,'cost1_types':14,'cost3_types':273,'common_cost3_types':165, + 'branches':branches,'all_21_branches_excluded':True,'controls':ctl,'seconds':time.monotonic()-start, + 'scope':'Any finite rational I15 decomposition on these five triads with every nonzero term tariff at most 3 has total invoice at least 45, attained by direct copies. Higher individual tariffs and the global P112 target remain outside this result.'} + +if __name__=='__main__': + ap=argparse.ArgumentParser();ap.add_argument('--repo-root',type=Path,default=HERE.parents[1]) + args=ap.parse_args();out=run(args.repo_root) + print(json.dumps({k:v for k,v in out.items() if k not in ('lift_matrix','branches')},indent=2))