diff --git a/research/p112-generalized-nonfano-invoice/PROOF.md b/research/p112-generalized-nonfano-invoice/PROOF.md new file mode 100644 index 0000000000..9272a474b6 --- /dev/null +++ b/research/p112-generalized-nonfano-invoice/PROOF.md @@ -0,0 +1,215 @@ +# One generalized non-Fano five-target mechanism: exact identity, wrong invoice + +This note tests ONE explicit algebraic construction supplied by the literature +agent from Das--Rai, arXiv:1609.05815, Section IV after equation(44), q=4. +No coefficient, embedding, or reader-choice sweep is performed. The network +coding identity is credited to that source; its present full-triad invoice +audit is local research and supplies no improved decoder or bound. + +## The exact identity + +Let a,b1,b2,b3,b4 be five distinct canonical target columns. Put B=sum_i bi, + + y0=a+B, yi=a+B-bi (i=1,...,4), yB=B. + +Then each bi=y0-yi. There are two displayed readers for a: + + a=y0-yB, + a=(y1+y2+y3+y4-3yB)/4. + +The query relation is + + 4y0-y1-y2-y3-y4-yB=0. + +Use the first reader at one scalar copy of a and the second at the other. +Use y0-yi at every scalar copy of bi. For a with a residual third copy, +either displayed a reader may be used there. Each reader column reconstructs +its corresponding target, so the six rank-one terms give exactly + + aa^T + sum_i bi bi^T. + +`verify.py` checks all100 entries on ten abstract scalar copies +over exact fractions, and finds source rank5 and reader rank6. The division +by4 is essential to this displayed algebra over Q; the argument is not an +entrywise reduction modulo2. + +## Exact complete-group masks + +Write Ua for the complete binary support of a, and Ui for that of bi. +Let L and R be the physical triads at the two a copies, and V=sum_i Ui. +The source and reader support spaces are exactly: + +| Term | Source space | Reader space | +|---|---|---| +| y0 | Ua+V | L+V | +| yi | Ua+sum_(j!=i) Uj | R+Ui | +| yB | V | Ua | + +The exact invoice is the sum of the six rectangular pairing ranks of these +spaces. Addition denotes a binary space sum, not direct sum. Repeated-role +axes cause physical groups to coincide; one must take the corresponding +unions, not count duplicate groups as additional dimensions. Since different +canonical targets have disjoint scalar supports, their nonzero query +coefficients do not cancel at a scalar port. + +In abstract group order aL,aR,b1L,b1R,...,b4L,b4R and term order +y0,y1,y2,y3,y4,yB, the checked masks are + + source: [1023,1011,975,831,255,1020], + reader: [1021,14,50,194,770,3]. + +These masks are a transparent exact invoice formula; they are not six scalar +rank charges. The physical cost remains rank_F2 of COMPLETE group pairings. + +## Structural rejection for every five ordinary target choice + +Let H_i=E_(2i+1)+E_(2i+2), i=0,...,17, be the ordinary pair spaces. Each has +dimension6 and Gram identity. The independent checker authenticates the +physical labels and cover, constructs their annihilators directly, and gives + +* each H_i^perp has seven nonzero vectors; +* among511 nonzero ambient vectors, the numbers lying in0,1,2,3 pair + annihilators are respectively395,107,8,1; none lies in4; +* among153 pairs of distinct roles,142 have zero common nonzero annihilators + and11 have exactly one. + +Consequently ANY TWO distinct pair roles span dimension at least8, and ANY +FOUR span the complete nine-dimensional ambient space. This is a fixed +incidence verification, not an embedding-cost optimization. + +Every ordinary paired role contains only three canonical scalar target axes. +Any four distinct ordinary targets therefore touch at least two pair roles. +Each of the SIX source queries above contains at least four distinct targets. +Their complete source spans S_t all have codimension at most1 in F2^9. + +For any binary source and reader spaces, + + rho(S,T)=dim(T)-dim(T intersect S^perp) + >=dim(T)-codim(S). + +The y0 reader contains the four b targets, so its reader span has dimension +at least8. Each yi reader contains Ui of dimension6, and the yB reader +contains Ua of dimension6. Therefore, without any detailed pricing, + + total invoice >= (8-1) + 4(6-1) + (6-1) = 32. (1) + +The five untouched ordinary targets cost30. Thus this specified mechanism +cannot improve their bill, even when several targets are different axes of +the same paired role. For FIVE DISTINCT roles the four-role saturation +premise makes all sources full9, giving the stronger simple floor + + total invoice >= 9 + 4*6 + 6 = 39. + +The bound32 also holds if one selected target is the residual-bearing axis. +Delete the residual scalar port from both factors first. The resulting +ordinary ten-port identity is unchanged, and each tariff can only decrease. +The original five-target baseline is then31, still below32. This argument +does not depend on which displayed a reader was assigned to the residual +copy. It also works when both remaining a copies use the same reader, +because y0 always reads all b copies, yi always reads bi, and yB always +reads a with a nonzero coefficient. + +## Why the hoped-for four-unit saving fails geometrically + +For the exact source and reader spaces define the annihilator benefit + + Z=sum_t dim(R_t intersect S_t^perp). + +The invoice is exactly sum_t dim(R_t)-Z. A four-unit improvement on an +ordinary baseline30 would require Z>=sum dim(R_t)-26>=12. But these actual +sources give Z<=6. This isolates the missing geometry: the query sums are +already so large that the readers have at most one invisible direction each. +The characteristic-dependent cancellation does not provide enough physical +annihilator benefit to offset that cost. Four successful units per block +would help the global38-unit gap only if enough compatible blocks existed; +this direct construction supplies none. + +## J cases and the complete scope of this specific reader assignment + +If the hub a is one of the final unpaired J axes, it has only one canonical +scalar copy, so the specified two-copy reader switch is unavailable. Choosing +either displayed reader for that one port, with the stated fixed b readers, +leaves every reader constant on each canonical target's support. Both factor +families then lie in the canonical span. The existing arbitrary-term +canonical-span theorem applies: after adjoining the untouched targets, a +58-term decomposition costs at least334+2, so its local invoice is at least +its old baseline plus2. This is a scope application of +`p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md`, not a new theorem. + +If a is ordinary and k of the bi are J axes, where1<=k<=3, write B0=30-3k +for the original bill before adding a possible residual line. The following +analytic extension was derived by the parent and independently audited here. +It uses two further fixed physical premises, checked from annihilator +intersections rather than embedding prices: + +* J plus any ordinary pair has dimension at least7: the dimensions9,8,7 occur + respectively7,9,2 times among the18 roles. +* An ordinary triad from a DIFFERENT role plus an ordinary paired space has + dimension at least7. All612 ordered choices were checked; their dimension + histogram is {7:46,8:318,9:248}. + +If every ordinary target is in the same pair H, every query source contains +H. The y0 reader contains H because there is at least one ordinary bi +(k<=3). Every ordinary yi reader contains H, as does the yB reader. These +terms cost at least6 each. For a J target bi, its yi source and reader both +contain the a-right triad R, so that term costs at least3. Thus + + C >= 6 + (4-k)*6 + k*3 + 6 = B0+6. (2) + +If the ordinary targets occupy at least two roles, the y0 source has +dimension at least8, while its reader contains an ordinary bi pair plus J +and has dimension at least7. Its tariff is at least6. The yB source contains +an ordinary bi pair plus J and has dimension at least7; its reader contains +the six-dimensional a pair, so its tariff is at least4. The k J-middle +terms still cost at least3 from their common a-right triad. + +Every ordinary middle term costs at least5. If its source retains at least +two ordinary roles, source dimension>=8 and reader dimension>=6 prove this. +Otherwise every remaining ordinary target lies in a's role H. The removed +bi belongs to a different role, since the entire target set occupied at +least two roles. The source contains H+J, of dimension>=7, and the reader +contains Ui plus the foreign a-right triad, also of dimension>=7. Rank-nullity +again gives tariff>=7-(9-7)=5. Consequently + + C >= 6 + 5(4-k) + 3k + 4 = 30-2k = B0+k. (3) + +There is at most one residual-bearing selected target. Deleting its residual +port reduces neither of the paired-triad premises used in(2)-(3), and the +original baseline is at most B0+1. Since k>=1, these cases cannot improve it; +the weakest k=1 residual bound allows a tie, not a saving. + +For this last assertion the reader assignment is exactly the one defined +above: the two ORDINARY partner-triad copies of a receive the two different +readers; an optional third residual copy may receive either. This guarantees +the a-right incidence in every middle reader after residual deletion. Putting +the sole five-term a reader on the residual line instead is a different +assignment and is not silently covered by(2)-(3). + +Together with(1) and the hub-J canonical-span application, this closes this +specified six-query/five-target mechanism on every choice of the fixed +canonical targets. No embedding or reader-choice sweep is used. + +## Relation to earlier hub work + +The earlier external-star theorem has queries of the form +a_j+alpha_j*c and a compensating common reader. It proves a floor for that +specific rank-one perturbation architecture. The present construction has +different query rays and a port-dependent choice between two a readers; +I have not proved it is an instance of that theorem. The earlier two-hub +K3,2 investigation retains seven independent reader-support premises per +mark and has a different rank/port architecture. Its failure to embed is +not used here. The present rejection rests entirely on the explicit identity +and literal span premises above. No broad old-hub closure is asserted. + +## Reproduction and status + + python -I -O -Werror -B research/p112-generalized-nonfano-invoice/verify.py + +The checker is standalone standard-library code, reads only the two pinned +physical inputs, and writes no files. It checks the exact coefficient identity, +source and reader masks, factor ranks, and the pair/J/foreign-triad annihilator +premises. The displayed analytic inequalities are the written proof; the +checker also checks their small integer accounting table. +It ran successfully in approximately0.3 seconds. The literary source was +identified by another agent; the algebra and physical premises were derived +and checked independently here. Human mathematical review is unclaimed. diff --git a/research/p112-generalized-nonfano-invoice/README.md b/research/p112-generalized-nonfano-invoice/README.md new file mode 100644 index 0000000000..6e54937312 --- /dev/null +++ b/research/p112-generalized-nonfano-invoice/README.md @@ -0,0 +1,28 @@ +# A generalized non-Fano decoder has the wrong full-group invoice + +The q=4 generalized non-Fano identity gives six rational queries for five canonical P112 targets, with different readers at the two physical copies of its hub. It reconstructs the endpoint exactly, but cannot save on the complete physical-group invoice for the reader assignment stated in [PROOF.md](PROOF.md). This is a structural rejection of one mechanism, not a coefficient or embedding search. + +For five ordinary targets the invoice is at least32 versus baseline30, including repeated axes in a paired role. A residual-bearing target raises that baseline to31 and still cannot help. The proof also closes every permitted placement of the exceptional J targets. The two ordinary hub copies use the two different displayed readers; an optional residual copy may use either. Other reader assignments are not silently included. + +The result does not improve334, meet the296 target, or change the selected multiplication bound. It does not exclude different sparse network codes, changed covers, or higher-rank fitting matrices. + +## Evidence and reproduction + +[PROOF.md](PROOF.md) derives the exact identity and the physical rank inequalities. [verify.py](verify.py) checks all100 endpoint entries, rejects altered nonzero coefficients, and authenticates the two physical inputs. It derives the fixed annihilator incidences: any two ordinary pair roles span at least8 dimensions, J plus a pair spans at least7, and every foreign triad plus a pair spans at least7. These are complete fixed-premise checks; the analytic case argument is in the proof. + +```sh +python3.12 -I -O -Werror -B research/p112-generalized-nonfano-invoice/verify.py +python3.12 -B scripts/research_package.py --package research/p112-generalized-nonfano-invoice +``` + +Standard-library Python3.12. The direct verifier also runs from an exported package containing its declared inputs, without Git or network access. [RESULT.json](RESULT.json) records the replay output. The hub-J case uses the pinned canonical-span theorem, whose proof is an explicitly declared input; it is not reproved here. + +## Sources and credit + +The network coding construction is from N. Das and B. K. Rai, [Generalized Fano and non-Fano networks](https://arxiv.org/pdf/1609.05815), Section IV, Lemma5 and the scalar code following equation(44). This package's contribution is the explicit split-reader adaptation and its complete-group invoice obstruction on the fixed P112 geometry. No novelty claim is made for the underlying coding identity. Repository geometry, canonical-span proof and their predecessor attribution are retained through [SOURCES.json](SOURCES.json). + +Prepared by flyingviper with substantial OpenAI Codex assistance, including a literature agent and separate mathematical audit. No independent human or proof-kernel review is claimed. New work is Apache-2.0; no third-party paper text is vendored. + +## Open next questions + +A useful next construction must avoid the dense-source obstruction. Give a sparse characteristic-dependent query identity and derive its exact whole-group masks and annihilator benefit before optimizing its placement. No such cheaper construction is supplied. [TASK.json](TASK.json) records this question, its first test and the remaining blockers. diff --git a/research/p112-generalized-nonfano-invoice/RESULT.json b/research/p112-generalized-nonfano-invoice/RESULT.json new file mode 100644 index 0000000000..f1ff7cfc0c --- /dev/null +++ b/research/p112-generalized-nonfano-invoice/RESULT.json @@ -0,0 +1,84 @@ +{ + "status": "PASS", + "input_sha256": { + "research/p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md": "9b2646258e5a7956380a601bb83c9721fe9c006be768762cf3095ae0b336ca08", + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/p112-rational-decoder-gate/CANDIDATE.json": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b" + }, + "endpoint_entries": 100, + "endpoint_mutations_rejected": 73, + "source_rank": 5, + "reader_rank": 6, + "source_masks_abstract_groups": [ + 1023, + 1011, + 975, + 831, + 255, + 1020 + ], + "reader_masks_abstract_groups": [ + 1021, + 14, + 50, + 194, + 770, + 3 + ], + "query_dependence": [ + 4, + -1, + -1, + -1, + -1, + -1 + ], + "annihilator_occupancy": { + "0": 395, + "1": 107, + "2": 8, + "3": 1 + }, + "nonzero_common_annihilator_profiles": { + "2": { + "0": 142, + "1": 11 + }, + "3": { + "0": 815, + "1": 1 + } + }, + "J_pair_nonzero_common_annihilator_profile": { + "0": 7, + "1": 9, + "3": 2 + }, + "foreign_triad_plus_pair_dimension_profile": { + "7": 46, + "8": 318, + "9": 248 + }, + "J_case_analytic_bounds": [ + { + "J_b_targets": 1, + "baseline_without_residual": 27, + "one_ordinary_role_floor": 33, + "multiple_ordinary_roles_floor": 28 + }, + { + "J_b_targets": 2, + "baseline_without_residual": 24, + "one_ordinary_role_floor": 30, + "multiple_ordinary_roles_floor": 26 + }, + { + "J_b_targets": 3, + "baseline_without_residual": 21, + "one_ordinary_role_floor": 27, + "multiple_ordinary_roles_floor": 24 + } + ], + "every_four_distinct_roles_span_dimension": 9, + "scope": "One exact six-query mechanism; fixed physical span checks, no pricing sweep." +} diff --git a/research/p112-generalized-nonfano-invoice/SOURCES.json b/research/p112-generalized-nonfano-invoice/SOURCES.json new file mode 100644 index 0000000000..461bb22398 --- /dev/null +++ b/research/p112-generalized-nonfano-invoice/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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/adaptive-kernel-demotion/inputs/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/p112-rational-decoder-gate/CANDIDATE.json", + "usage": "input", + "git_blob": "e645ae164f5b4132889bd2aab162ecc2e8ebf4c4", + "sha256": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b" + }, + { + "path": "research/p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md", + "usage": "input", + "git_blob": "6143e856b59319862d87915baefe6f9e10a494f4", + "sha256": "9b2646258e5a7956380a601bb83c9721fe9c006be768762cf3095ae0b336ca08" + } + ] +} diff --git a/research/p112-generalized-nonfano-invoice/TASK.json b/research/p112-generalized-nonfano-invoice/TASK.json new file mode 100644 index 0000000000..ee111cef55 --- /dev/null +++ b/research/p112-generalized-nonfano-invoice/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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": "Audit the exact q=4 generalized non-Fano split-reader construction on all choices of five fixed P112 canonical targets. Prove no full-group invoice saving for the specified reader assignment, including repeated roles, J targets and the residual line.", + "scope_change_reason": "The donor assigned the rational-decoder cost296 goal and requested a continuous literature agent. This is a concrete literature mechanism audit within that assigned goal, rather than a new task draw.", + "bottleneck_link": "Characteristic-dependent scalar cancellation is useful only if complete physical source and reader group costs fall. Dense query spans prevent this mechanism from saving.", + "budget_minutes": null, + "stop_rule": "Stop after the exact six-query identity and all target-choice cases are proved using fixed span premises. No coefficient or embedding sweep.", + "outcome": "negative-result", + "evidence": "PROOF.md, verify.py and RESULT.json; exact source pins and declared replay.", + "author": "flyingviper", + "ai_assistance": "Substantial OpenAI Codex assistance with a separate literature agent and separate mathematical audit. No independent human or formal-kernel review claimed.", + "open_questions": [ + { + "question": "Can a different sparse characteristic-dependent network keep its source spaces small enough to earn a physical annihilator benefit?", + "why_it_matters": "The displayed six-query gadget is exact but its dense sources erase the prospective saving. Reaching296 from334 needs38 compatible saved charges.", + "first_step": "Give a concrete sparse query identity and reader assignment, derive every complete-group support, and bound its annihilator benefit before any geometry optimization.", + "blocked_by": "No cheaper identity, whole-group cost certificate or native supplier is supplied. Changes to the reader assignment, cover or fitting matrix are outside this result." + } + ], + "budget_override": "Donor requests continuation until 30 percent usage remains; this bounded completed mechanism audit is part of that research." +} diff --git a/research/p112-generalized-nonfano-invoice/VERIFY.json b/research/p112-generalized-nonfano-invoice/VERIFY.json new file mode 100644 index 0000000000..81e23a2725 --- /dev/null +++ b/research/p112-generalized-nonfano-invoice/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json", + "research/p112-rational-decoder-gate/CANDIDATE.json", + "research/p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact rational endpoint and coefficient mutations; full source/reader masks; authenticated pair/J/foreign-triad span premises and analytic accounting." + } + ] +} diff --git a/research/p112-generalized-nonfano-invoice/verify.py b/research/p112-generalized-nonfano-invoice/verify.py new file mode 100644 index 0000000000..da048ded71 --- /dev/null +++ b/research/p112-generalized-nonfano-invoice/verify.py @@ -0,0 +1,158 @@ +"""Exact identity and fixed geometric premises for one five-target mechanism. + +No candidate, coefficient, reader, or embedding optimization is performed. +""" +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PINS = { + 'research/p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md': + '9b2646258e5a7956380a601bb83c9721fe9c006be768762cf3095ae0b336ca08', + 'research/adaptive-kernel-demotion/inputs/DATA-PHASES.json': + 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa', + 'research/p112-rational-decoder-gate/CANDIDATE.json': + 'dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b', +} + + +def need(ok, text): + if not ok: + raise ValueError(text) + + +def read(path): + raw = (ROOT / path).read_bytes() + need(sha256(raw).hexdigest() == PINS[path], 'input pin') + return json.loads(raw) + + +def rational_rank(matrix): + rows = [[F(x) for x in row] for row in matrix] + r = 0 + for c in range(len(rows[0])): + found = next((i for i in range(r, len(rows)) if rows[i][c]), None) + if found is None: + continue + rows[r], rows[found] = rows[found], rows[r] + pivot = rows[r][c] + rows[r] = [x/pivot for x in rows[r]] + for i in range(r+1, len(rows)): + v = rows[i][c] + if v: + rows[i] = [x-v*y for x, y in zip(rows[i], rows[r])] + r += 1 + return r + + +def check_endpoint(source, reader): + need(all(sum(source[p][t]*reader[q][t] for t in range(6)) == int(p//2 == q//2) + for p in range(10) for q in range(10)), '100 exact endpoint entries') + + +def main(): + for path, pin in PINS.items(): + need(sha256((ROOT/path).read_bytes()).hexdigest() == pin, 'source pin: '+path) + # Query order y0,y1,y2,y3,y4,yB. Target-coordinate order a,b1,..,b4. + queries = [[1]*5] + for i in range(1, 5): + queries.append([int(j != i) for j in range(5)]) + queries.append([0,1,1,1,1]) + source = [[queries[t][p//2] for t in range(6)] for p in range(10)] + reader = [[F(1),F(0),F(0),F(0),F(0),F(-1)], + [F(0),F(1,4),F(1,4),F(1,4),F(1,4),F(-3,4)]] + for i in range(1, 5): + row = [F(0)]*6 + row[0], row[i] = F(1), F(-1) + reader.extend([row[:], row[:]]) + check_endpoint(source, reader) + rejected=0 + for original, which in ((source, 'source'), (reader, 'reader')): + for row in range(10): + for col in range(6): + if not original[row][col]: + continue + changed=[list(r) for r in original] + changed[row][col] += 1 + try: + check_endpoint(changed if which=='source' else source, + changed if which=='reader' else reader) + except ValueError: + rejected+=1 + else: + raise ValueError('endpoint mutation survived') + need(rejected == 73, 'complete nonzero-coefficient mutation domain') + need(rational_rank(source) == 5 and rational_rank(reader) == 6, 'factor ranks5,6') + relation = [4,-1,-1,-1,-1,-1] + need(all(sum(relation[t]*queries[t][j] for t in range(6)) == 0 for j in range(5)), + 'query circuit relation') + source_masks = [sum(1 << p for p in range(10) if source[p][t]) for t in range(6)] + reader_masks = [sum(1 << p for p in range(10) if reader[p][t]) for t in range(6)] + need(source_masks == [1023,1011,975,831,255,1020], 'abstract source masks') + need(reader_masks == [1021,14,50,194,770,3], 'abstract reader masks') + + data = read('research/adaptive-kernel-demotion/inputs/DATA-PHASES.json') + cover = read('research/p112-rational-decoder-gate/CANDIDATE.json') + labels = [r['q'] for r in sorted(data['recipes'], key=lambda r: r['port'])] + groups = cover['groups'] + need(len(labels) == 112 and len(groups) == 38, 'literal geometry size') + pair_vectors = [[labels[p] for g in (2*i+1, 2*i+2) for p in groups[g]] for i in range(18)] + need(all(all((x&y).bit_count()%2 == int(i == j) for i,x in enumerate(pair) + for j,y in enumerate(pair)) for pair in pair_vectors), 'own six-dimensional Gram') + annihilators = [{z for z in range(1, 512) if all((z&x).bit_count()%2 == 0 for x in pair)} + for pair in pair_vectors] + need(all(len(s) == 7 for s in annihilators), 'three-dimensional annihilators') + occupancy = Counter(sum(z in s for s in annihilators) for z in range(1, 512)) + need(dict(occupancy) == {0:395, 1:107, 2:8, 3:1}, 'literal annihilator incidence') + intersection_profile = {} + for count in (2, 3): + hist = Counter(len(set.intersection(*(annihilators[i] for i in roles))) + for roles in combinations(range(18), count)) + intersection_profile[count] = dict(sorted(hist.items())) + need(intersection_profile == {2:{0:142,1:11},3:{0:815,1:1}}, 'pair/triple span premises') + j_vectors = [labels[p] for p in groups[37]] + need(all((x&y).bit_count()%2 == int(i == j) for i,x in enumerate(j_vectors) + for j,y in enumerate(j_vectors)), 'J own Gram identity') + j_annihilator = {z for z in range(1, 512) if all((z&x).bit_count()%2 == 0 for x in j_vectors)} + j_pair_profile = Counter(len(j_annihilator & ann) for ann in annihilators) + need(dict(j_pair_profile) == {0:7,1:9,3:2}, 'J-plus-pair boundary') + triad_annihilators = [{z for z in range(1,512) + if all((z&labels[p]).bit_count()%2 == 0 for p in groups[g])} + for g in range(1,37)] + foreign_dimensions = Counter() + for role, ann in enumerate(annihilators): + for group_index, triad_ann in enumerate(triad_annihilators): + if group_index//2 == role: + continue + annihilator_order = len(ann & triad_ann)+1 + need(annihilator_order & (annihilator_order-1) == 0, 'annihilator subspace order') + dimension = 9-(annihilator_order.bit_length()-1) + foreign_dimensions[dimension] += 1 + need(dict(foreign_dimensions) == {7:46,8:318,9:248}, 'foreign triad plus pair premise') + need(sum(foreign_dimensions.values()) == 612, 'complete foreign triad domain') + j_bounds = [{'J_b_targets':k, 'baseline_without_residual':30-3*k, + 'one_ordinary_role_floor':36-3*k, 'multiple_ordinary_roles_floor':30-2*k} + for k in (1,2,3)] + need(all(r['multiple_ordinary_roles_floor'] >= r['baseline_without_residual']+1 + for r in j_bounds), 'residual cannot rescue J cases') + print(json.dumps({'status':'PASS', 'input_sha256':PINS, + 'endpoint_entries':100, 'endpoint_mutations_rejected':rejected, 'source_rank':5, 'reader_rank':6, + 'source_masks_abstract_groups':source_masks, + 'reader_masks_abstract_groups':reader_masks, + 'query_dependence':relation, + 'annihilator_occupancy':dict(sorted(occupancy.items())), + 'nonzero_common_annihilator_profiles':intersection_profile, + 'J_pair_nonzero_common_annihilator_profile':dict(sorted(j_pair_profile.items())), + 'foreign_triad_plus_pair_dimension_profile':dict(sorted(foreign_dimensions.items())), + 'J_case_analytic_bounds':j_bounds, + 'every_four_distinct_roles_span_dimension':9, + 'scope':'One exact six-query mechanism; fixed physical span checks, no pricing sweep.'}, + separators=(',', ':'))) + + +if __name__ == '__main__': + main()