From 4d80ba76770faa76317c7c397cfe992fbb4c551a Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 2 Nov 2026 21:07:26 -0600 Subject: [PATCH] Quantify sharp flag defect for unequal decoder payloads --- .../flag-defect-decoder-budget/.gitattributes | 1 + .../flag-defect-decoder-budget/ORIGIN.json | 7 + research/flag-defect-decoder-budget/PROOF.md | 156 +++++++ research/flag-defect-decoder-budget/README.md | 66 +++ .../flag-defect-decoder-budget/RESULT.json | 391 ++++++++++++++++++ .../flag-defect-decoder-budget/SOURCES.json | 27 ++ research/flag-defect-decoder-budget/TASK.json | 102 +++++ .../flag-defect-decoder-budget/VERIFY.json | 32 ++ .../inputs/flag_source.md | 159 +++++++ research/flag-defect-decoder-budget/model.py | 91 ++++ research/flag-defect-decoder-budget/verify.py | 216 ++++++++++ 11 files changed, 1248 insertions(+) create mode 100644 research/flag-defect-decoder-budget/.gitattributes create mode 100644 research/flag-defect-decoder-budget/ORIGIN.json create mode 100644 research/flag-defect-decoder-budget/PROOF.md create mode 100644 research/flag-defect-decoder-budget/README.md create mode 100644 research/flag-defect-decoder-budget/RESULT.json create mode 100644 research/flag-defect-decoder-budget/SOURCES.json create mode 100644 research/flag-defect-decoder-budget/TASK.json create mode 100644 research/flag-defect-decoder-budget/VERIFY.json create mode 100644 research/flag-defect-decoder-budget/inputs/flag_source.md create mode 100644 research/flag-defect-decoder-budget/model.py create mode 100644 research/flag-defect-decoder-budget/verify.py diff --git a/research/flag-defect-decoder-budget/.gitattributes b/research/flag-defect-decoder-budget/.gitattributes new file mode 100644 index 0000000000..8abeb4295b --- /dev/null +++ b/research/flag-defect-decoder-budget/.gitattributes @@ -0,0 +1 @@ +inputs/** -text diff --git a/research/flag-defect-decoder-budget/ORIGIN.json b/research/flag-defect-decoder-budget/ORIGIN.json new file mode 100644 index 0000000000..a9710c535d --- /dev/null +++ b/research/flag-defect-decoder-budget/ORIGIN.json @@ -0,0 +1,7 @@ +{ + "local": "inputs/flag_source.md", + "commit": "e95d4665ecc67808d6cf4344b6f2fe6f1300768c", + "path": "research/compatible-flag-fitting-rank/PROOF.md", + "git_blob": "6cf82cf95911a4546434a1b5b9c63c6eced1ba2d", + "sha256": "077cf34f35123e65799a6f7f9b95a2f83daa35b39844375f54e1c7554265920a" +} diff --git a/research/flag-defect-decoder-budget/PROOF.md b/research/flag-defect-decoder-budget/PROOF.md new file mode 100644 index 0000000000..abd9772826 --- /dev/null +++ b/research/flag-defect-decoder-budget/PROOF.md @@ -0,0 +1,156 @@ +# The rank budget for a defect in port flags + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +Nick Petalas's PR6471 proves the equal-width compatible-flag floor. +This contribution permits unequal widths and gaps in flag levels. It +quantifies the rank of a violation, proves a sharp family, and gives the +complete field-operation word for that family. The odd-cycle edge code +and elementary rank inequalities are classical; neither is claimed new. + +## Declared interface + +Let K be a field. Port i has dimension d_i>0 and a fixed ordered basis. +Give its basis vectors distinct increasing integer levels l_(i,a). +F_i^t is the span of vectors whose levels are at most t. Thus each port +can gain zero or one dimension at each level. The levels may have gaps. +Ordinary unequal complete flags have l_(i,a)=a for 1<=a<=d_i. + +Let Z be a directed zero mask on distinct ports. A fitting matrix M has +rectangular blocks M_ij:K^d_j -> K^d_i, identity diagonal blocks and zero +blocks on Z. For a port set I, mu_K(Z[I]) is the minimum scalar fitting +rank on that induced mask, with diagonal one. Put mu(empty)=0. Let + + I_t={i: port i has a basis vector at level t}, + B=sum_t mu_K(Z[I_t]). + +Define E by retaining precisely the entries of M whose target level is +strictly greater than their source level. All other entries of E are zero. +The defect rank e is rank E. This definition uses the declared adapted +bases, including their complements, not just the abstract flag subspaces. +No entry of a forbidden block or a diagonal identity is changed. + +## Theorem + +The exact minimum among compatible matrices, those with E=0, is B. +For every fitting M, compatible or not, + + rank M >= B-rank E. (1) + +Consequently a query factorization M=DQ through q field coordinates obeys +q+rank E>=B. A claimed saving of s query coordinates below B needs at +least s defect rank in every choice of adapted port bases and flags. +The defect is a diagnostic quantity, not a separately free physical channel. + +To prove the compatible minimum, order coordinates by level. The matrix +is block upper triangular. At each occupied level t its diagonal block +fits Z[I_t], so it has rank at least mu_K(Z[I_t]). The nonzero-minor +argument in PR6471 gives rank M>=B. Conversely choose a scalar minimum +independently at each level and set every cross-level entry to zero. +This has identity diagonal blocks and all required zeros. Its rank is B. +Conjugate by the prescribed port bases to realize the same construction +for arbitrary given flags. This includes gaps and unequal dimensions. + +For an arbitrary M, A=M-E is compatible. The standard inequality +rank A<=rank M+rank E proves (1). Thus the coefficient of the defect +rank is exactly one. The next family proves that it cannot be reduced. + +These formulas use scalar minima over K. Flags or bases available only +over an extension L give minima over L. No base-field substitution is +implicit. The result gives no efficient general minrank or flag algorithm. + +## A sharp defect of every positive rank + +Fix n=2k+1>=5 and s>=1. The zero mask is the cycle C_n: only diagonal +and neighbor blocks are allowed. At each port put two coordinates for +each of s copies, one for each incident edge. Let Q sum the two source +coordinates on each edge in each copy. Let D copy each edge value to +its two incident output coordinates. Then M=DQ has diagonal I_(2s), +zero nonneighbor blocks, and rank ns over every field. Indeed each +edge contributes one nonzero all-one two-by-two block on a disjoint +pair of coordinates. This is the classical edge representation. + +For clarity, the scalar cycle minimum is k+1 over every field. A cover +by k disjoint edges and one vertex gives rank k+1. For the lower bound, +the odd-indexed ports 1,3,...,2k-1 form an independent set of size k. +If a fitting factorization had rank k, their encoder vectors and decoder +rows would be dual bases. Port 0's encoder and decoder then use only +the first basis direction, and both coefficients are nonzero because +its diagonal is one. The nonneighbor entry from row 0 to column 2 forces +the first coefficient of encoder 2 to vanish. Encoder 2 can use only +the first two basis directions, so its second coefficient is nonzero; +its diagonal forces decoder 2's second coefficient to be nonzero. +Repeat using the nonneighbor entry from row 2 to column 4. Induction +forces encoder 2k-2 to use only the last basis direction. Decoder 2k +also uses only that last dual direction, with nonzero coefficient. +Their nonneighbor entry is then nonzero, a contradiction. This proof +uses directed zeros and works in every characteristic. + +The compatible floor is therefore 2s(k+1)=ns+s. Inequality (1) proves +that rank E>=s for this M under EVERY local complete flag and adapted +basis. To attain s, order copies consecutively and alternate the two +incident edge coordinates at successive ports. Every cycle edge except +the closing edge then connects equal levels in each direction. The +closing edge has one entry below the level order in each copy. These +s entries have distinct rows and columns, so rank E=s. Thus + + min_(all local flags and adapted bases) rank E = s, + rank M = B-s. + +This exact result holds for all odd n>=5, all s>=1 and every field. +It proves the quantitative bound is sharp at arbitrary defect rank. +It does not assert a new unrestricted vector minrank theorem for C_n. +The edge-code rank and scalar cycle minimum are established context. + +## Literal word and its complete field-operation bill + +Sources x are read-only. Outputs y can have arbitrary initial values. +For each edge/copy with source fields a,b and output fields u,v, use one +reusable scratch field q. With q initially zero, execute + + q += a; q += b; u += q; v += q; q -= b; q -= a. + +After each group, q is zero, the sources are unchanged, and the two +outputs have received a+b. The complete word has 6ns field additions, +12ns operand reads and 6ns destination writes. There are ns encodings, +2ns output uses and ns complete uncomputations. Scratch is one field, +not ns retained fields. The initial clean field is an explicit premise. + +If q must instead start with arbitrary dirty value z, first execute +u-=q and v-=q before the same six operations. This costs 8ns additions, +16ns reads and 8ns writes, and restores q=z after every group. Both +output increments are still exactly a+b and independent of z. No CLEAR +of a nonzero field, hidden transcript or unpaid initialization is used. +All 2ns output coordinates are updated once per complete code application. + +For exact integer data with initial absolute values at most H, all clean +word values are bounded by 3H. The dirty word has q=z+a+b, intermediate +outputs y-z, and final outputs y+a+b, so the same 3H bound holds at every +event. It is sharp. A signed width w with 2^(w-1)>3H is sufficient. +No division or fractional rounding is needed. These are indexed field +operations. Physical movement, control, record precision and native +recursive costs have NOT been priced. A direct four-ADD-per-edge program +also applies the same matrix without exposing Q. Thus fewer abstract +queries do not imply fewer scalar operations or a physical speedup. + +## Evidence and limits + +The finite verifier independently enumerates small binary fitting matrices +with unequal widths and checks both compatible minima and (1). It tests +gapped levels, directed masks, fields 2,3,5, explicit sharp words and all +binary local two-dimensional bases for C5. Literal ADD traces verify +source preservation, arbitrary dirty output/scratch behavior, every range +bound, the full operation invoice and omitted-operation failures. + +The written proof supplies the unbounded result. The finite corpus is +corroboration, not independent human or proof-kernel acceptance. No +native supplier, profitable actual caller, complete physical invoice, +new kappa or selected-frontier change is claimed. All five selected +assumptions remain. The useful next task is a source-bound decoder that +pays for the required defect and still wins after its full caller costs. + +Credit Nick Petalas / PR6471, ywz65 / PR2541, Aaron Wang / navinor / +PR825, Cinna Davis and the retained geometry/native/compiler lineage. +Bukh, Cox and Blasiak retain the fractional Haemers framework credit. +See Bukh and Cox, [On a fractional version of Haemers' bound](https://arxiv.org/html/1802.00476v2). +No global literature-priority claim is made. diff --git a/research/flag-defect-decoder-budget/README.md b/research/flag-defect-decoder-budget/README.md new file mode 100644 index 0000000000..919992a796 --- /dev/null +++ b/research/flag-defect-decoder-budget/README.md @@ -0,0 +1,66 @@ +# Exact flag-defect decoder budget + +A fitting matrix with unequal payloads and prescribed one-dimensional flag +levels has the exact compatible minimum B=sum_t mu(Z[I_t]). Gaps in each +port's levels are allowed. For an arbitrary fitting matrix M, let E retain +only entries that move to a higher flag level. Then **rank M+rank E>=B**. +A query saving of s therefore needs at least s defect rank. + +The [proof](PROOF.md) shows that this bound is sharp for every positive s, +over every field. For s copies of the classical width-two odd-cycle edge +code, the minimum defect rank over ALL local complete flags and adapted +bases is exactly s. The code and its rank advantage are credited prior +work; the new result is their exact defect budget, together with the +unequal/gapped interface and the complete linear operation word. + +The literal implementation preserves sources, updates arbitrary dirty +outputs, and restores one reused scratch field. It pays six ADDs per +edge-copy with initially clean scratch, or eight with arbitrary dirty +scratch. The integer prefix range is at most 3H, and this is sharp. A +four-ADD direct-source implementation exists too. This package therefore +claims no scalar-operation or physical speedup from the query-rank gain. + +## Evidence and replay + +```sh +python3.12 -B scripts/research_package.py --package research/flag-defect-decoder-budget +``` + +Standalone: `python3.12 -I -Werror -B verify.py` in this directory, and +again with `-O`. The [receipt](RESULT.json) is recomputed. The verifier +uses only the standard library and retained files. No Git or network is +needed. It covers all 180,625 binary fitting matrices for the unequal +(1,2,2) payload, independent image ranks, gapped profiles over F2/F3/F5, +all 7,776 local GL2 basis tuples for C5, larger sharp cases and complete +clean/dirty literal words. Failure controls include an actual retained +source corruption and omitted ADDs. Exact counts are in the receipt. + +Canonical base: main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, +priority 8, selected 6030. The selected binding example passed. The +02:55Z overlap cache covered 476 open PRs and 6,464 Discussion records. +Live handoffs and PRs were also checked. No competing quantitative defect +scope was found. Sparse history, nested diffs and unpublished work remain +coverage limits. The theorem is written; finite checks corroborate it. + +## Open next questions + +Bind the inequality to an actual decoder with a full native and physical +invoice. The first test must include its input access, flags, payload +volume, monomial maps, dirty restoration and complete caller costs. +A separate useful question is efficient defect minimization in a specific +source family; the exact odd-cycle family is a calibration input. + +No native supplier, actual profitable caller, kappa gain or selected-frontier +change is claimed. Precision, stock, tape, compiler, outer admission and +all five selected assumptions remain. Independent human and proof-kernel +review are unclaimed. Lean, Docker and the selected cold replay were not run. + +## Credit + +Ali Romman with substantial OpenAI Codex assistance; no subagents. +Nick Petalas / PR6471 supplies the equal-width flag theorem. Credit +also ywz65 / PR2541, Aaron Wang / navinor / PR825, Cinna Davis, Bukh, +Cox, Blasiak and the retained geometry/native/compiler lineage. The +source proof is retained byte for byte. The odd-cycle representation, +scalar minrank facts and elementary rank inequalities are classical. +No global literature-priority claim is made. New work is Apache-2.0. diff --git a/research/flag-defect-decoder-budget/RESULT.json b/research/flag-defect-decoder-budget/RESULT.json new file mode 100644 index 0000000000..23621de36c --- /dev/null +++ b/research/flag-defect-decoder-budget/RESULT.json @@ -0,0 +1,391 @@ +{ + "C5_defect_histogram": { + "1": 640, + "3": 5120, + "4": 32, + "5": 1984 + }, + "counts": { + "C5_local_basis_tuples": 7776, + "all_unequal_matrices": 180625, + "compatible_unequal_matrices": 18225, + "complete_word_inputs": 678, + "gapped_field_cases": 288, + "invalid_inputs": 10, + "omitted_operations": 192, + "sharp_family_cases": 36, + "source_corruptions": 1 + }, + "scope": "All-field written theorem and finite checks; no native invoice or kappa.", + "sharp_family": [ + [ + 2, + 5, + 1, + 5, + 1 + ], + [ + 2, + 5, + 2, + 10, + 2 + ], + [ + 2, + 5, + 3, + 15, + 3 + ], + [ + 2, + 7, + 1, + 7, + 1 + ], + [ + 2, + 7, + 2, + 14, + 2 + ], + [ + 2, + 7, + 3, + 21, + 3 + ], + [ + 2, + 9, + 1, + 9, + 1 + ], + [ + 2, + 9, + 2, + 18, + 2 + ], + [ + 2, + 9, + 3, + 27, + 3 + ], + [ + 2, + 11, + 1, + 11, + 1 + ], + [ + 2, + 11, + 2, + 22, + 2 + ], + [ + 2, + 11, + 3, + 33, + 3 + ], + [ + 3, + 5, + 1, + 5, + 1 + ], + [ + 3, + 5, + 2, + 10, + 2 + ], + [ + 3, + 5, + 3, + 15, + 3 + ], + [ + 3, + 7, + 1, + 7, + 1 + ], + [ + 3, + 7, + 2, + 14, + 2 + ], + [ + 3, + 7, + 3, + 21, + 3 + ], + [ + 3, + 9, + 1, + 9, + 1 + ], + [ + 3, + 9, + 2, + 18, + 2 + ], + [ + 3, + 9, + 3, + 27, + 3 + ], + [ + 3, + 11, + 1, + 11, + 1 + ], + [ + 3, + 11, + 2, + 22, + 2 + ], + [ + 3, + 11, + 3, + 33, + 3 + ], + [ + 5, + 5, + 1, + 5, + 1 + ], + [ + 5, + 5, + 2, + 10, + 2 + ], + [ + 5, + 5, + 3, + 15, + 3 + ], + [ + 5, + 7, + 1, + 7, + 1 + ], + [ + 5, + 7, + 2, + 14, + 2 + ], + [ + 5, + 7, + 3, + 21, + 3 + ], + [ + 5, + 9, + 1, + 9, + 1 + ], + [ + 5, + 9, + 2, + 18, + 2 + ], + [ + 5, + 9, + 3, + 27, + 3 + ], + [ + 5, + 11, + 1, + 11, + 1 + ], + [ + 5, + 11, + 2, + 22, + 2 + ], + [ + 5, + 11, + 3, + 33, + 3 + ] + ], + "source_hashes": { + "ORIGIN.json": "ad31dd6f4b891a944629e2e38069a0dea219d1adb9c9e3a6b97005670d755c9e", + "PROOF.md": "9a440e8bb28ead8737dc5d4f2ec9c90bae73385368183559acdff67a1174e93f", + "model.py": "07bf0cdab0eede873ad2561bf7152c89f275afd71b2b742196bb6d0de9708428", + "verify.py": "78b7dca1f90cbccccfc431e95f2c1d065315356308af9e9806fb9b1b60375e89" + }, + "status": "PASS_FLAG_DEFECT_DECODER_BUDGET", + "word_invoices": [ + { + "adds": 30, + "copies": 1, + "dirty": false, + "n": 5, + "reads": 60, + "scratch_fields": 1, + "writes": 30 + }, + { + "adds": 40, + "copies": 1, + "dirty": true, + "n": 5, + "reads": 80, + "scratch_fields": 1, + "writes": 40 + }, + { + "adds": 60, + "copies": 2, + "dirty": false, + "n": 5, + "reads": 120, + "scratch_fields": 1, + "writes": 60 + }, + { + "adds": 80, + "copies": 2, + "dirty": true, + "n": 5, + "reads": 160, + "scratch_fields": 1, + "writes": 80 + }, + { + "adds": 42, + "copies": 1, + "dirty": false, + "n": 7, + "reads": 84, + "scratch_fields": 1, + "writes": 42 + }, + { + "adds": 56, + "copies": 1, + "dirty": true, + "n": 7, + "reads": 112, + "scratch_fields": 1, + "writes": 56 + }, + { + "adds": 84, + "copies": 2, + "dirty": false, + "n": 7, + "reads": 168, + "scratch_fields": 1, + "writes": 84 + }, + { + "adds": 112, + "copies": 2, + "dirty": true, + "n": 7, + "reads": 224, + "scratch_fields": 1, + "writes": 112 + }, + { + "adds": 66, + "copies": 1, + "dirty": false, + "n": 11, + "reads": 132, + "scratch_fields": 1, + "writes": 66 + }, + { + "adds": 88, + "copies": 1, + "dirty": true, + "n": 11, + "reads": 176, + "scratch_fields": 1, + "writes": 88 + }, + { + "adds": 132, + "copies": 2, + "dirty": false, + "n": 11, + "reads": 264, + "scratch_fields": 1, + "writes": 132 + }, + { + "adds": 176, + "copies": 2, + "dirty": true, + "n": 11, + "reads": 352, + "scratch_fields": 1, + "writes": 176 + } + ] +} diff --git a/research/flag-defect-decoder-budget/SOURCES.json b/research/flag-defect-decoder-budget/SOURCES.json new file mode 100644 index 0000000000..dea196138e --- /dev/null +++ b/research/flag-defect-decoder-budget/SOURCES.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ], + "retained_predecessors": [ + { + "local": "inputs/flag_source.md", + "commit": "e95d4665ecc67808d6cf4344b6f2fe6f1300768c", + "path": "research/compatible-flag-fitting-rank/PROOF.md", + "git_blob": "6cf82cf95911a4546434a1b5b9c63c6eced1ba2d", + "sha256": "077cf34f35123e65799a6f7f9b95a2f83daa35b39844375f54e1c7554265920a" + } + ] +} diff --git a/research/flag-defect-decoder-budget/TASK.json b/research/flag-defect-decoder-budget/TASK.json new file mode 100644 index 0000000000..eab0a860ec --- /dev/null +++ b/research/flag-defect-decoder-budget/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact unequal/gapped flag floor, defect-rank budget, sharp all-field odd-cycle family and complete clean/dirty field-operation words.", + "scope_change_reason": "Extend the released PR6471 interface to quantify required cross-level coupling and variable payloads; no Lean or selected-caller theorem.", + "bottleneck_link": "A decoder that beats scalar fitting must pay enough cross-level coupling. The sharp defect budget gives a quantitative necessary target, while the complete field word exposes restoration costs.", + "budget_minutes": 90, + "stop_rule": "Stop at the all-field theorem, sharp family and literal full invoice. Do not infer a native or physical gain.", + "outcome": "completed", + "evidence": "PROOF.md, model.py, verify.py and RESULT.json; exhaustive unequal-width binary matrices and all C5 local GL2 bases.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, code, testing and prose; no subagents.", + "open_questions": [ + { + "question": "Can a source-bound decoder pay for its flag defect and still improve the full caller?", + "why_it_matters": "A query-rank saving does not pay physical costs by itself.", + "first_step": "Choose an actual caller mask and payload, compute its defect and price its full word.", + "blocked_by": "No actual paid native caller is supplied." + }, + { + "question": "Can defect-rank minimization over local flags be solved efficiently for a useful source family?", + "why_it_matters": "The theorem gives a certificate but no general optimizer.", + "first_step": "Use the exact odd-cycle family as a positive control for a restricted source-bound solver.", + "blocked_by": "Unrestricted minrank and flag search are not solved." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19365165" +} diff --git a/research/flag-defect-decoder-budget/VERIFY.json b/research/flag-defect-decoder-budget/VERIFY.json new file mode 100644 index 0000000000..11888cae15 --- /dev/null +++ b/research/flag-defect-decoder-budget/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "All unequal binary matrices, independent image ranks, gapped profiles, all C5 bases, sharp families, full clean/dirty ADD words and controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "All unequal binary matrices, independent image ranks, gapped profiles, all C5 bases, sharp families, full clean/dirty ADD words and controls." + } + ] +} diff --git a/research/flag-defect-decoder-budget/inputs/flag_source.md b/research/flag-defect-decoder-budget/inputs/flag_source.md new file mode 100644 index 0000000000..6cf82cf959 --- /dev/null +++ b/research/flag-defect-decoder-budget/inputs/flag_source.md @@ -0,0 +1,159 @@ +# Exact fitting rank with compatible port flags + +This scoped written proof was produced by Nick Petalas. Apache-2.0. + +## Contract + +Let K be any field, n,d positive integers, and Z a set of ordered pairs +(i,j) with i different from j. A scalar matrix A fits Z if A_ii=1 and +A_ij=0 for (i,j) in Z. Other ordered entries are free, independently of +their transposes. Write mu_K(Z) for the smallest rank of a fitting matrix. +This minimum exists: the identity fits, and ranks are integers in 1..n. + +At each port i choose a complete K-flag + + 0 = F_i^0 < F_i^1 < ... < F_i^d = K^d, + dim F_i^a = a. + +A block fitting matrix M has d-by-d blocks, M_ii=I_d and M_ij=0 for +(i,j) in Z. Call it compatible if + + M_ij(F_j^a) is contained in F_i^a + +for every i,j,a. The source flag is at j and the target flag is at i. +Flags at distinct ports may differ. Entries and free blocks need not be +symmetric, invertible, commuting, normal, diagonalizable or positive. +There is one flag per port used by every block incident to it, not a +fresh flag for each block. The diagonal identity identifies that port's +input and output payload spaces. No coordinate is assumed clean or fixed. + +## Theorem + +For every K,n,d,Z and every prescribed family of complete flags, + + min rank_K M = d mu_K(Z), + +where the minimum is over compatible block fitting matrices. +In particular, even optimizing the flags cannot lower this value. + +### Lower bound + +Choose a basis P_i adapted to each flag. With the block diagonal matrix +P=diag(P_1,...,P_n), set T=P^-1 M P. Its block T_ij is upper triangular: +its column a lies in the first a coordinates precisely because the map +sends F_j^a into F_i^a. Also T_ii=I and T_ij=0 on Z. Conjugation preserves +rank over K. + +Order the full coordinates by flag level first, then by port. This is one +simultaneous row and column permutation. The resulting matrix is block +upper triangular with d diagonal blocks of size n: + + A_a = ((T_ij)_aa)_(i,j), a=1,...,d. + +Each A_a fits the original directed mask Z. Thus rank A_a>=mu_K(Z). + +For completeness, an upper block triangular matrix with possibly singular +diagonal blocks A_a has rank at least sum_a rank A_a. For each a select a +nonsingular square minor of A_a of order rank A_a. Select those rows and +columns in the full matrix. The combined submatrix is square and block +upper triangular, with exactly those nonsingular minors on its diagonal. +Its determinant is their nonzero product. This argument includes empty +minors for any zero-rank diagonal block and works in every characteristic. +Therefore + + rank M = rank T >= sum_a rank A_a >= d mu_K(Z). + +### Attainment for any prescribed flags + +Take a scalar fitting matrix A of rank mu_K(Z), and set + + M_ij = A_ij P_i P_j^-1. + +Its diagonal blocks are I and its forbidden blocks are zero. It sends +F_j^a into F_i^a. The full M equals P(A tensor I_d)P^-1, so its rank is +d rank A. One can see this rank directly by permuting A tensor I_d into +d copies of A. This attains the lower bound with the prescribed flags. +No method for efficiently finding a scalar optimum is asserted. QED. + +## Consequences and the field boundary + +If a linear query layer factors M=D E through r field coordinates, then +r>=rank M>=d mu_K(Z). This counts total linear query coordinates. It is +not a native COPY tariff or a count of recursive child ranks. Volume, +source access, frames, ownership and restoration still need separate costs. + +Over an algebraically closed field, any finite commuting family of square +matrices has a common complete flag. To recall the classical argument, +restrict to a nonzero eigenspace of one member. All other commuting members +preserve it. Repeated restriction gives a common eigenvector. Its span is +invariant; applying induction to the quotient gives the full flag. +This does not assume diagonalizability and includes Jordan blocks. +Apply the theorem with the same flag at every port. Consequently commuting +complex block fitting matrices cannot beat d mu_C(Z). Noncommuting blocks +which preserve compatible flags are excluded as well. Mere noncommutation +is not sufficient to obtain a block-rank advantage. + +If a K-matrix has compatible flags only over an extension L, extension +preserves its rank and the proof gives rank_K M>=d mu_L(Z). It does not +give d mu_K(Z) unless flags over K or equality of the scalar minima is +separately justified. The theorem with prescribed K-flags remains valid +over all fields, including finite fields. The complex commuting corollary +must not be silently read as a base-field rational minrank statement. + +For Cinna Davis's field-line scalar-query repair, the cited complex scalar +fitting-rank inequality is mu_C(G)>|V(G)|/4 for its C4-free graph. +The present theorem transfers that inequality to compatible-flag block +fits as rank M>d|V(G)|/4. This is a conditional use of the retained scalar +lemma, not a fresh proof or replay of its scaling argument or invoice. +It closes only the flag-compatible part of that open operator-valued +boundary. Arbitrary flag-breaking block fits remain outside this result. + +## Why the hypothesis matters + +The finite checker includes two sharp complete-mask examples. One has +noncommuting upper triangular 3-by-3 blocks and rank three. Another has +three distinct two-dimensional local charts and rank two, although its +raw block family preserves no common binary line. The second example +shows why a single raw-coordinate flag is stronger than portwise +compatibility. + +As a boundary control, take the classical width-two C5 representation +with one scalar coordinate per edge. Port i carries the two edges incident +to i, and a block identifies coordinates bearing the same edge. The +diagonal is I_2, nonneighbors have zero blocks, and the complete matrix +has rank five. The scalar C5 minimum is three, so the theorem would force +rank at least six if compatible flags existed. The verifier independently +rejects all 3^5 local flag tuples over F2. This classical block advantage +is inherited context, not a new C5 optimum. It prevents dropping the +compatibility hypothesis or inferring it from identity diagonal blocks. + +## Provenance and scope + +The block-fitting and query-factorization framework is classical. See +Boris Bukh and Christopher Cox, [On a fractional version of Haemers' bound, +section 2 and Proposition 9](https://arxiv.org/html/1802.00476v2), which +credits Anna Blasiak's earlier fractional bound. The elementary rank-minor +and simultaneous-triangularization facts are also classical. No global +literature priority is claimed. The contribution is the exact arbitrary +directed-mask, prescribed port-flag interface and its stated obstruction +for this repository's vector-decoder search. + +Credit ywz65's [PR2541](https://github.com/CrocSwap/integer-mult-bounds/pull/2541) +for the strict block-fitting contract, its 49d result on a particular mask +and the unrestricted C5 comparison. Credit Aaron Wang / navinor's +[PR825](https://github.com/CrocSwap/integer-mult-bounds/pull/825) for a +different common-flag obstruction in the all-role framed XOR circuit +model. The present argument concerns a completed fitting matrix, not that +circuit model, and neither theorem subsumes the other's physical contract. +Credit Cinna Davis's retained field-line repair for its scalar inequality +and open operator-valued question, and the native/geometry predecessors +credited in those sources. SOURCES.json pins these texts as historical +provenance. No predecessor executable, certificate or scientific replay +is used by the new verifier. + +The proof supplies no native word, arbitrary flag-breaking lower bound, +efficient flag-finding procedure, unequal-dimension theorem, paid physical +invoice, new kappa, supplier admission or complete multiplication theorem. +The five selected framework assumptions remain. Independent human and +formal proof-kernel review are unclaimed. Finite checks corroborate the +written proof rather than establish its unbounded quantifiers. diff --git a/research/flag-defect-decoder-budget/model.py b/research/flag-defect-decoder-budget/model.py new file mode 100644 index 0000000000..445b29427a --- /dev/null +++ b/research/flag-defect-decoder-budget/model.py @@ -0,0 +1,91 @@ +"""Finite-field flags and the literal edge-query word. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +def require(ok, message): + if not ok: + raise ValueError(message) + + +def rank(matrix, p): + a = [row[:] for row in matrix] + if not a: + return 0 + m, n, r = len(a), len(a[0]), 0 + for j in range(n): + pivot = next((i for i in range(r, m) if a[i][j] % p), None) + if pivot is None: + continue + a[r], a[pivot] = a[pivot], a[r] + scale = pow(a[r][j] % p, -1, p) + a[r] = [v*scale % p for v in a[r]] + for i in range(r+1, m): + z = a[i][j] % p + a[i] = [(x-z*y) % p for x, y in zip(a[i], a[r])] + r += 1 + if r == m: + break + return r + + +def audit(matrix, levels, allowed, p): + require(p in (2, 3, 5), 'unsupported replay field') + require(type(levels) is tuple and levels and all(type(v) is tuple and v for v in levels), 'levels shape') + require(all(all(type(x) is int for x in v) and list(v) == sorted(set(v)) for v in levels), 'levels not strictly increasing') + coordinates = [(i, t) for i, layer in enumerate(levels) for t in layer] + size = len(coordinates) + require(size <= 120, 'replay size limit') + require(type(allowed) is frozenset and all(type(e) is tuple and len(e) == 2 and + all(type(i) is int and 0 <= i < len(levels) for i in e) and e[0] != e[1] + for e in allowed), 'invalid directed mask') + require(len(matrix) == size and all(len(row) == size for row in matrix), 'matrix shape') + require(all(type(x) is int and 0 <= x < p for row in matrix for x in row), 'noncanonical field entry') + defect = [[0]*size for _ in range(size)] + for a, (i, t) in enumerate(coordinates): + for b, (j, u) in enumerate(coordinates): + if i == j: + require(matrix[a][b] == int(a == b), 'diagonal block is not identity') + elif (i, j) not in allowed: + require(matrix[a][b] == 0, 'forbidden block') + if t > u: + defect[a][b] = matrix[a][b] + return rank(matrix, p), rank(defect, p), defect + + +def cycle(n, copies): + require(type(n) is int and n >= 5 and n % 2 == 1, 'cycle must be odd and at least five') + require(type(copies) is int and copies > 0 and 2*n*copies <= 120, 'copy limit') + labels = [(c, (i-1) % n if a == 0 else i) for i in range(n) + for c in range(copies) for a in range(2)] + matrix = [[int(x == y) for y in labels] for x in labels] + allowed = frozenset((i, j) for i in range(n) for j in range(n) if (i-j) % n in (1, n-1)) + return matrix, allowed + + +def word(n, copies, dirty): + require(type(dirty) is bool, 'dirty mode must be boolean') + require(type(n) is int and n >= 5 and n % 2 == 1, 'cycle must be odd and at least five') + require(type(copies) is int and copies > 0 and 2*n*copies <= 120, 'copy limit') + size = 2*n*copies + q = 2*size + result = [] + for i in range(n): + for c in range(copies): + a = 2*copies*i+2*c+1 + b = 2*copies*((i+1) % n)+2*c + u, v = size+a, size+b + if dirty: + result += [(u, q, -1), (v, q, -1)] + result += [(q, a, 1), (q, b, 1), (u, q, 1), (v, q, 1), + (q, b, -1), (q, a, -1)] + return tuple(result) + + +def execute(values, operations): + values = list(values) + maximum = max(map(abs, values), default=0) + for dst, src, sign in operations: + require(dst != src and sign in (-1, 1), 'invalid ADD') + values[dst] += sign*values[src] + maximum = max(maximum, abs(values[dst])) + return values, maximum diff --git a/research/flag-defect-decoder-budget/verify.py b/research/flag-defect-decoder-budget/verify.py new file mode 100644 index 0000000000..a97b35b5d1 --- /dev/null +++ b/research/flag-defect-decoder-budget/verify.py @@ -0,0 +1,216 @@ +"""Independent finite tests for the defect budget and the complete ADD word. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from pathlib import Path +from itertools import product +from collections import Counter +import hashlib +import json +import random +import runpy +import shutil +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent +M = runpy.run_path(str(ROOT/'model.py')) +check, rank, audit = M['require'], M['rank'], M['audit'] + + +def image_rank(matrix): + rows = [sum(x << j for j, x in enumerate(row)) for row in matrix] + space = {0} + for row in rows: + space |= {x ^ row for x in space} + size = len(space) + check(size & (size-1) == 0, 'image is not a binary subspace') + return size.bit_length()-1 + + +def scalar(ports, allowed, p): + edges = [(i, j) for i in range(len(ports)) for j in range(len(ports)) + if i != j and (ports[i], ports[j]) in allowed] + best, witness = len(ports)+1, None + for values in product(range(p), repeat=len(edges)): + a = [[int(i == j) for j in ports] for i in ports] + for (i, j), x in zip(edges, values): + a[i][j] = x + r = rank(a, p) + if r < best: + best, witness = r, a + return best, witness + + +def bound_and_attainer(levels, allowed, p): + coordinates = [(i, t) for i, layer in enumerate(levels) for t in layer] + attainer = [[0]*len(coordinates) for _ in coordinates] + bound = 0 + for t in sorted({t for _, t in coordinates}): + indices = [j for j, x in enumerate(coordinates) if x[1] == t] + ports = [coordinates[j][0] for j in indices] + minimum, a = scalar(ports, allowed, p) + bound += minimum + for i, row in enumerate(indices): + for j, col in enumerate(indices): + attainer[row][col] = a[i][j] + r, e, _ = audit(attainer, levels, allowed, p) + check((r, e) == (bound, 0), 'layer attainer fails') + return bound + + +def fitting(levels, allowed, values): + coords = [(i, t) for i, layer in enumerate(levels) for t in layer] + a = [[int(i == j) for j in range(len(coords))] for i in range(len(coords))] + values = iter(values) + for i, (port, _) in enumerate(coords): + for j, (source, _) in enumerate(coords): + if (port, source) in allowed: + a[i][j] = next(values) + return a + + +def binary_census(counts): + levels = ((0,), (0, 1), (0, 1)) + edges = [(i, j) for i in range(3) for j in range(3) if i != j] + for mask in range(64): + allowed = frozenset(e for i, e in enumerate(edges) if mask >> i & 1) + bound = bound_and_attainer(levels, allowed, 2) + free = sum(len(levels[i])*len(levels[j]) for i, j in allowed) + compatible_min = 6 + for values in product(range(2), repeat=free): + a = fitting(levels, allowed, values) + r, e, defect = audit(a, levels, allowed, 2) + check(r == image_rank(a) and e == image_rank(defect), 'independent image rank') + check(r+e >= bound, 'defect inequality fails') + if e == 0: + compatible_min = min(compatible_min, r) + counts['compatible_unequal_matrices'] += 1 + counts['all_unequal_matrices'] += 1 + check(compatible_min == bound, 'unequal minimum fails') + check(counts['all_unequal_matrices'] == 180625, 'incomplete unequal census') + + +def chart_c5(matrix, charts): + invs = [] + for a in charts: + # Every nonzero determinant over F2 is one. + invs.append([[a[1][1], a[0][1]], [a[1][0], a[0][0]]]) + out = [[0]*10 for _ in range(10)] + for i, j, r, c in product(range(5), range(5), range(2), range(2)): + out[2*i+r][2*j+c] = sum(invs[i][r][u]*matrix[2*i+u][2*j+v]*charts[j][v][c] + for u in range(2) for v in range(2)) % 2 + return out + + +def run(): + counts = Counter() + origin = json.loads((ROOT/'ORIGIN.json').read_text()) + data = (ROOT/origin['local']).read_bytes() + check(hashlib.sha256(data).hexdigest() == origin['sha256'], 'source pin') + check(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() == origin['git_blob'], 'source Git blob') + with tempfile.TemporaryDirectory() as tmp: + dest = Path(tmp) + (dest/'inputs').mkdir() + for name in ('model.py', 'verify.py', 'ORIGIN.json'): + shutil.copyfile(ROOT/name, dest/name) + (dest/origin['local']).write_bytes(data+b'\n') + mutated = runpy.run_path(str(dest/'verify.py')) + try: + mutated['run']() + except ValueError as error: + check(str(error) == 'source pin', 'wrong source rejection') + counts['source_corruptions'] += 1 + else: + raise ValueError('changed retained source accepted') + binary_census(counts) + rng = random.Random(20261103) + gap_profiles = [((0, 3), (1,), (0, 2)), ((-2,), (0, 1), (3, 4)), ((0,), (0, 2, 4), (1, 2))] + edges = [(i, j) for i in range(3) for j in range(3) if i != j] + for p, levels, mask in product((2, 3, 5), gap_profiles, (0, 13, 37, 63)): + allowed = frozenset(e for i, e in enumerate(edges) if mask >> i & 1) + bound = bound_and_attainer(levels, allowed, p) + for _ in range(8): + free = sum(len(levels[i])*len(levels[j]) for i, j in allowed) + a = fitting(levels, allowed, (rng.randrange(p) for _ in range(free))) + r, e, _ = audit(a, levels, allowed, p) + check(r+e >= bound, 'gapped/field defect inequality') + counts['gapped_field_cases'] += 1 + sharp = [] + for p, n, copies in product((2, 3, 5), (5, 7, 9, 11), (1, 2, 3)): + a, allowed = M['cycle'](n, copies) + # Change each odd port's basis by swapping the two edge coordinates. + order = [2*copies*i+2*c+(1-b if i % 2 else b) + for i in range(n) for c in range(copies) for b in range(2)] + changed = [[a[i][j] for j in order] for i in order] + levels = (tuple(range(2*copies)),)*n + r, e, defect = audit(changed, levels, allowed, p) + check((r, e) == (n*copies, copies), 'sharp all-field defect') + check(sum(x != 0 for row in defect for x in row) == copies, 'defect is not the claimed matching') + counts['sharp_family_cases'] += 1 + sharp.append([p, n, copies, r, e]) + a, allowed = M['cycle'](5, 1) + bases = [] + for values in product(range(2), repeat=4): + b = [list(values[:2]), list(values[2:])] + if rank(b, 2) == 2: + bases.append(b) + hist = Counter() + for charts in product(bases, repeat=5): + r, e, defect = audit(chart_c5(a, charts), ((0, 1),)*5, allowed, 2) + check(r == 5 and e >= 1 and e == image_rank(defect), 'C5 all-basis lower bound') + hist[e] += 1 + check(sum(hist.values()) == 6**5 and min(hist) == 1, 'incomplete GL2 census') + counts['C5_local_basis_tuples'] = sum(hist.values()) + word_invoices = [] + for n, copies, dirty in product((5, 7, 11), (1, 2), (False, True)): + a, _ = M['cycle'](n, copies) + size = len(a) + operations = M['word'](n, copies, dirty) + expected_ops = (8 if dirty else 6)*n*copies + check(len(operations) == expected_ops, 'wrong full ADD bill') + vectors = [[int(i == j) for i in range(2*size+1)] for j in range(2*size+int(dirty))] + vectors += [[sign*7]*(2*size)+([sign*7] if dirty else [0]) for sign in (-1, 1)] + vectors += [[rng.randrange(-7, 8) for _ in range(2*size)]+([rng.randrange(-7, 8)] if dirty else [0]) for _ in range(8)] + for values in vectors: + actual, maximum = M['execute'](values, operations) + expected = values[:size] + [values[size+i]+sum(a[i][j]*values[j] for j in range(size)) + for i in range(size)] + values[-1:] + check(actual == expected, 'literal word endpoint/source/scratch') + check(maximum <= 3*max(map(abs, values)), 'prefix range exceeds 3H') + counts['complete_word_inputs'] += 1 + positive = [7]*(2*size)+([7] if dirty else [0]) + check(M['execute'](positive, operations)[1] == 21, 'range bound not attained') + for j in range(min(len(operations), 16)): + bad = operations[:j]+operations[j+1:] + check(any(M['execute'](v, bad)[0] != M['execute'](v, operations)[0] for v in vectors), 'omitted operation survived') + counts['omitted_operations'] += 1 + word_invoices.append(dict(n=n,copies=copies,dirty=dirty,adds=expected_ops,reads=2*expected_ops,writes=expected_ops,scratch_fields=1)) + invalid = [lambda: M['cycle'](4,1), lambda: M['cycle'](3,1), lambda: M['cycle'](5,0), + lambda: M['word'](5,1,1), lambda: audit([[1]],((0,0),),frozenset(),2), + lambda: audit([[0]],((0,),),frozenset(),2), lambda: audit([[1]],((0,),),frozenset(),4), + lambda: audit([[1,1],[0,1]],((0,),(0,)),frozenset(),2), + lambda: audit([[1]],((0,),),frozenset({(0,0)}),2), + lambda: audit([[2]],((0,),),frozenset(),2)] + for f in invalid: + try: + f() + except ValueError: + counts['invalid_inputs'] += 1 + else: + raise ValueError('invalid input accepted') + hashes = {name: hashlib.sha256((ROOT/name).read_bytes()).hexdigest() + for name in ('PROOF.md','model.py','verify.py','ORIGIN.json')} + return dict(status='PASS_FLAG_DEFECT_DECODER_BUDGET',counts=dict(counts),sharp_family=sharp, + C5_defect_histogram={str(k):v for k,v in sorted(hist.items())},word_invoices=word_invoices, + source_hashes=hashes,scope='All-field written theorem and finite checks; no native invoice or kappa.') + + +if __name__ == '__main__': + result = run() + if sys.argv[1:] == ['--write']: + (ROOT/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: + check(not sys.argv[1:],'unknown command option') + check(result == json.loads((ROOT/'RESULT.json').read_text()),'receipt differs') + print(json.dumps(result,sort_keys=True))