From f41c74eb9c628c4998b8f7ed9813a7585d4bb301 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 23:12:57 +0000 Subject: [PATCH] feat(research): classify third binary character extremizers --- .../binary-character-extremizers/PROOF.md | 154 +++++++++++++ .../binary-character-extremizers/README.md | 136 +++++++++++ .../binary-character-extremizers/SOURCES.json | 36 +++ .../binary-character-extremizers/TASK.json | 113 +++++++++ .../binary-character-extremizers/VERIFY.json | 34 +++ .../binary-character-extremizers/verify.py | 216 ++++++++++++++++++ 6 files changed, 689 insertions(+) create mode 100644 research/binary-character-extremizers/PROOF.md create mode 100644 research/binary-character-extremizers/README.md create mode 100644 research/binary-character-extremizers/SOURCES.json create mode 100644 research/binary-character-extremizers/TASK.json create mode 100644 research/binary-character-extremizers/VERIFY.json create mode 100644 research/binary-character-extremizers/verify.py diff --git a/research/binary-character-extremizers/PROOF.md b/research/binary-character-extremizers/PROOF.md new file mode 100644 index 0000000000..fe3f755a75 --- /dev/null +++ b/research/binary-character-extremizers/PROOF.md @@ -0,0 +1,154 @@ +# Exact equality in the third binary character mode + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and result + +Let k >= 3 and let c be a zero-diagonal k-by-k matrix over F2, with at +least two nonzero entries. Interpret c_ij=1 as an arrow i -> j. Define + +```text +Z(c) = sum over s in {0,1,2}^k of + (-1)^(sum over i,j of c_ij [s_i=1][s_j=2]). +``` + +Nick Petalas's [PR5146](https://github.com/CrocSwap/integer-mult-bounds/pull/5146) +proves 0 < Z(c) <= 19*3^(k-3). Its second open question asks which graphs +attain the upper bound. The following is the new classification. + +**Theorem.** Equality holds if and only if c has exactly two arrows, and +they have a common tail or a common head. Every other vertex is isolated. +There are exactly k(k-1)(k-2) labelled equality matrices. Each has even +entry weight, hence positive sign in the signed character expansion. + +The proof uses an exhaustive new local equality lemma. It does not infer +the universal statement by testing a finite list of dimensions. + +## The local equality lemma + +For a zero-diagonal three-by-three binary matrix a with at least two +arrows and a binary field f=(u_0,v_0,u_1,v_1,u_2,v_2), put + +```text +L(a,f) = sum over s in {0,1,2}^3 of + (-1)^(sum a_ij [s_i=1][s_j=2] + + sum_i (u_i[s_i=1]+v_i[s_i=2])). +``` + +**Finite lemma.** |L(a,f)| <= 19. Equality in absolute value holds exactly +when a consists of two arrows with a common head or tail and f=0. +In those six cases L(a,0)=+19. There are no cases with L(a,f)=-19. + +`verify.py:local_equality` proves this finite lemma by enumerating every +one of the (64-1-6)*64=3648 graph/field configurations and all 27 states +for each. The graph bits, in order, are + +```text +(0,1), (0,2), (1,0), (1,2), (2,0), (2,1). +``` + +The complete equality rows are below. The field mask is zero in each row. + +| Graph mask | Arrows | L | +|---:|---|---:| +| 3 | 0->1, 0->2 | 19 | +| 10 | 0->2, 1->2 | 19 | +| 12 | 1->0, 1->2 | 19 | +| 20 | 1->0, 2->0 | 19 | +| 33 | 0->1, 2->1 | 19 | +| 48 | 2->0, 2->1 | 19 | + +The checker derives its expected equality condition from endpoint +incidence, rather than using this table to compute the sums. It retains +the complete table in the generated receipt. Every test uses explicit +exceptions and also runs under optimized Python. + +## Reducing global equality to three vertices + +We use PR5146's reciprocal-pair and directed-matching bounds as cited +premises. A reciprocal pair gives Z(c) <= 5*3^(k-2), strictly below the +target. If the arrows form a directed matching with r >= 2 arrows, then + +```text +Z(c)/3^k = (7/9)^r <= 49/81 < 19/27. +``` + +Otherwise some two arrows share a vertex. Their endpoints form a set H +of three vertices with at least two induced arrows. For each fixed +outside assignment t, separate the character exponent into the induced +quadratic part on H, its induced unary field f(t), and its outside +constant q(t). Thus + +```text +Z(c) = sum over t in {0,1,2}^(k-3) of (-1)^q(t) L(c_H,f(t)). +``` + +The finite lemma bounds each real summand above by 19. If the sum equals +19*3^(k-3), every summand must equal +19. At t=0, the field and constant +are both zero. The equality lemma forces c_H to be a two-arrow star. +For every other t it then forces f(t)=0 and q(t)=0, since its only +absolute equality value is L(c_H,0)=+19. + +These requirements remove every possible outside arrow. For an outside +vertex v, set all other outside states to zero. The choice t_v=1 gives + +```text +coefficient of [s_i=2] in f(t) = c_vi for each i in H. +``` + +The choice t_v=2 gives the coefficients c_iv of [s_i=1]. Thus f(t)=0 +for these two assignments implies that no arrow joins v to H, in either +direction. This holds for each outside vertex. + +If an arrow v->w existed entirely outside H, assign t_v=1, t_w=2 and +all other outside states zero. The only possible active outside term is +c_vw=1, even if the reverse arrow exists. Hence q(t)=1, contradicting +q(t)=0. Therefore the outside graph is empty. This proves necessity, +including k=3 where the outside set is empty. + +## Attainment, count and signed multiplicity + +For a common-tail star, condition on its center. States 0 and 2 each +contribute 9; state 1 contributes (1+1-1)^2=1. The sum is 19. Swapping +states 1 and 2 at every vertex transposes the graph and gives the same +value for a common-head star. Every isolated vertex contributes a factor +3, proving sufficiency. + +Choose the center, an unordered pair of other vertices, and one of the +two orientations. The center and orientation are unique in every such +graph, so the exact labelled count is + +```text +2*k*binomial(k-1,2) = k(k-1)(k-2). +``` + +Each matrix has exactly two entries. In PR4275's signed character law +its sign (-1)^|c| is therefore +1. Write its unnormalized power sum as + +```text +S_n = sum over zero-diagonal c of (-1)^|c| Z(c)^n. +``` + +The coefficient of (19*3^(k-3))^n in S_n is exactly k(k-1)(k-2). +The walk count has the additional Fourier factor 2^(-k(k-1)); header +probabilities have their further finite-GL denominator. None of these +normalizations is included in the stated spectral multiplicity. This +is a direct corollary of the classification, not a calculation of the +rest of the spectrum or a new all-dimension probability inequality. + +## Dependencies and limits + +PR5146 supplies the character interpretation, sharp bound and explicit +equality question. The cited reciprocal and matching bounds are used as +published results, without auditing their predecessors. PR4275 supplies +the signed character law for the multiplicity corollary. Ryanson Jonathan +and PR4607 supply the five-event spectral context. The retained request +and normalizer lineage is credited in README.md. + +Zero diagonal, F2 and the exact uniform three-state sum are essential. +The proof supplies no odd-field or weighted analogue, fourth-mode bound, +complete negative-association theorem, header producer, sampling/emission +procedure, native implementation, dirty restoration, complete physical +invoice, new kappa or complete multiplication theorem. The five selected +framework assumptions remain. Independent human and formal proof-kernel +review are unclaimed. diff --git a/research/binary-character-extremizers/README.md b/research/binary-character-extremizers/README.md new file mode 100644 index 0000000000..8d9b9a0210 --- /dev/null +++ b/research/binary-character-extremizers/README.md @@ -0,0 +1,136 @@ +# Exact extremizers of the third binary character mode + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped mathematical proof with an exhaustive finite equality +lemma. For every k >= 3, the zero-diagonal binary character matrices with +at least two entries attaining Z(c)=19*3^(k-3) are exactly two arrows +with a common head or tail, plus isolated vertices. Their exact labelled +count is k(k-1)(k-2). Every one has positive sign in the unnormalized +signed full-guard character sum, so this is its exact third-mode +coefficient. The Fourier and finite-GL normalization factors are separate. + +This answers Open next question 2 of +[PR5146](https://github.com/CrocSwap/integer-mult-bounds/pull/5146). +That predecessor proves the sharp bound and supplies one attaining +family. The new result is the complete equality classification and exact +multiplicity. Its published bound is a cited premise. No predecessor +program, census or spectrum table is imported or audited. + +[PROOF.md](PROOF.md) gives the universal argument. A three-vertex equality +lemma forces every outside-induced unary field and constant to vanish. +One-vertex and two-vertex outside assignments then rule out every extra +arrow. Labelled stars give the matching construction and count. No new +kappa or selected-frontier change is claimed. + +## Reproduce + +From the repository root, using the Python 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/binary-character-extremizers/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/binary-character-extremizers/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/binary-character-extremizers +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/binary-character-extremizers --check-source-history +``` + +Any CPython 3.12 interpreter can replace the displayed local path. The +direct commands write nothing and emit `PASS_BINARY_CHARACTER_EXTREMIZERS` +inside a newly generated JSON receipt binding all six package files by +SHA256. Neither a receipt nor mathematical output is hand-written. +Each registered command has a 120-second timeout. The standalone checker +requires neither Git nor predecessor files. + +## Evidence + +The checker enumerates every three-vertex graph with at least two arrows +and every unary field. Its literal ternary-state sum establishes the new +local equality lemma. A separate positive-subset sum checks global +classification at small dimensions and every extension of a fixed +attaining core by two outside vertices. It also constructs all labelled +stars for k=3 through 8 and checks their distinctness, values and count. +The generated receipt records exact executed counts and the six complete +local equality rows. Invalid domains and false equality rules reject, +including a directed path, reciprocal arrows, a three-arrow star, +nonzero unary fields and an outside edge with a changing constant sign. + +Executed coverage is 3648 local graph/field cases, 4140 character matrices +at k=3,4, all 16384 two-outside-vertex extensions of one fixed core, and +756 distinct labelled attaining examples at k=3..8. The local sums and +the positive-subset oracle agree on all 57 eligible k=3 characters. +There are eight invalid-domain rejections, six semantic checks and 63 +nonzero-field rejections. The local equality table has exactly six rows. +Three actual code mutations, omitting fields, changing star incidence and +ignoring outside edges, reject in both normal and optimized local runs. + +The finite checks establish the local finite lemma and corroborate the +universal argument. They are not a census at every dimension. Normal and +optimized modes run the same explicit checks. Source pins are historical +provenance only, with no external executable inputs. The current baseline +orientation reports `PASS_RESEARCH_BASELINE_BINDINGS_ONLY` for selected +PR6030; that is metadata orientation rather than a scientific replay. + +## Scope and limits + +The independent-moment card is explicitly changed to this original +spectral side question. Binary arithmetic, zero diagonal and the uniform +three-state weights are essential. The result does not give a fourth +spectral mode, a complete all-k probability inequality, negative +association, an odd-field or weighted analogue, a request producer, +sampling/emission procedure, native realization, dirty restoration or +complete physical invoice. All five selected framework assumptions remain. +No complete multiplication theorem is claimed. Selected cold replay, +Lean, Docker and native builds were not run. Independent human and formal +proof-kernel review are unclaimed. + +All verifier loops have explicit finite input bounds, with no recursion, +subprocesses or dynamic execution. Matrices have at most twelve rows; +literal sums allow at most six, and executed local sums use three. +The extension loop has exactly 16384 cases and handles one matrix at a +time. Each function fits within sixty physical lines. Explicit exceptions +retain contracts under optimization; registered commands treat warnings +as errors. Python and standard-library runtime dispatch and allocation +are managed-runtime deviations from fixed allocation and static calls. +The declared dimension/file bounds and one-at-a-time enumeration bound +live work. No real-time or fixed-memory runtime guarantee is claimed. +A larger census must revise and verify the capacities first. Syntax and +function-length inspection pass. External Python analyzers were unavailable; +warning-strict execution is the recurring registered diagnostic. + +## Open next questions + +1. What is the sharp fourth character value and its complete equality + family? Begin with the next local conditioned extrema and outside-field + rigidity. This proof supplies neither that value nor a fourth-mode gap. + The answer could sharpen full-guard moment remainders. +2. Can an actual request producer exploit a shared header at a favorable + complete price? Start with one source-bound producer/consumer and + account for sampling, selection, emission, native alignment and dirty + restoration. Those physical costs are unknown here. + +[TASK.json](TASK.json) records structured relevance, first steps and blockers. +Research stops at this first verified improvement; no follow-on is reserved. + +## Credit and coordination + +Nick Petalas / PR5146 supplies the sharp remainder bound and explicit +equality question, and PR4275 supplies the signed character law. Ryanson +Jonathan / pinterbanget PR4607 supplies the five-event predecessor and +structural-spectrum motivation. Nick Petalas / PR4599 supplies the +four-event antecedent. Cinna Davis, source527, commdata2338 and Jose Manuel +retain the request and normalizer lineage credited by those sources. +Conditioning, finite character sums and the triangle inequality are +classical. The scoped classification and its checker are the new work. +Frozen sources and predecessor attribution are unchanged. + +Base: canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority +revision 8, selected PR6030. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362336) +records the target. Live claims, local reservations, current main README +searches, merged/open PR searches and recent account work were checked. +The cached overlap snapshot has 387 open PRs and 6319 Discussion records +with complete remote pagination, but searches only 114 of 8917 local +notes. Separate Git searches cover main README terms. Unpublished work, +sparse notes and arbitrary historical diffs remain coverage limits. +PR5860's five-indicator probability comparisons and PR6415's literal +header-census optimization are separate quantities and are not extended. diff --git a/research/binary-character-extremizers/SOURCES.json b/research/binary-character-extremizers/SOURCES.json new file mode 100644 index 0000000000..78f2602970 --- /dev/null +++ b/research/binary-character-extremizers/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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" + }, + { + "path": "research/binary-character-remainder-gap/README.md", + "usage": "provenance", + "git_blob": "26dfd91cd1076ceae1732a8340daa70c746969a5", + "sha256": "d333054883ff2d9a5f8414d188b0e51c418d14de21f1f3ba927f5546c2d6661d" + }, + { + "path": "research/five-event-guard-correlation/README.md", + "usage": "provenance", + "git_blob": "ffcdb61c6e3619f440453e18499ecf6a7a2b3f6f", + "sha256": "1fb2d6ae867323dc1330bb5581def650b1d1c81e365043b104db73d803ebcb19" + }, + { + "path": "research/corankone-triple-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8", + "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f" + } + ] +} diff --git a/research/binary-character-extremizers/TASK.json b/research/binary-character-extremizers/TASK.json new file mode 100644 index 0000000000..b27745b3af --- /dev/null +++ b/research/binary-character-extremizers/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify every zero-diagonal binary character matrix attaining the sharp third-mode bound, and count its labelled signed multiplicity for every k>=3.", + "scope_change_reason": "The user requests original research rather than an audit. This answers PR5146 Open next question 2, a spectral side question; no constructor invoice is audited.", + "bottleneck_link": "Scoped shared-header spectral side result. Exact extremizers determine the positive third-mode coefficient but supply no physical supplier or paid caller.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified equality classification; defer fourth modes and probability inequalities.", + "outcome": "completed", + "evidence": "PROOF.md and the new standalone exact equality verifier. Normal and optimized registered commands enumerate the local equality domain and bounded global/extension controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the sharp largest character value after excluding zero, single arrows and the two-arrow stars?", + "why_it_matters": "A fourth-mode gap would sharpen the remainder in full-guard moment comparisons.", + "first_step": "Classify the next local conditioned extrema, then prove how equality constrains outside fields.", + "blocked_by": "This equality theorem supplies neither the next value nor its global extremizers." + }, + { + "question": "Can an actual producer exploit this shared-header spectrum within a fully paid caller?", + "why_it_matters": "A counting theorem alone does not fund request preparation, selection, emission or restoration.", + "first_step": "Specify one source-bound request family and its complete physical producer/consumer bill.", + "blocked_by": "Native realization, sampling and complete physical costs are unknown." + } + ], + "claim_type": "scoped mathematical proof with an exhaustive finite equality lemma", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362336", + "source_question": { + "pr": 5146, + "opened": "2026-10-23T11:00:42Z", + "question": 2, + "author": "petalas" + } +} diff --git a/research/binary-character-extremizers/VERIFY.json b/research/binary-character-extremizers/VERIFY.json new file mode 100644 index 0000000000..e5e6ee66c9 --- /dev/null +++ b/research/binary-character-extremizers/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete finite equality lemma; all small characters; every two-outside-vertex extension; labelled families and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact equality checks with assertions disabled; all checks use explicit exceptions." + } + ] +} diff --git a/research/binary-character-extremizers/verify.py b/research/binary-character-extremizers/verify.py new file mode 100644 index 0000000000..5d3897e250 --- /dev/null +++ b/research/binary-character-extremizers/verify.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Exact new equality checks; no predecessor imports or spectrum tables.""" + +import hashlib +import itertools +import json +import platform +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def validate(rows): + require(type(rows) is tuple and 2 <= len(rows) <= 12, "matrix size") + k = len(rows) + require(all(type(row) is int and 0 <= row < 1 << k for row in rows), + "binary row masks") + require(all(not (rows[i] >> i & 1) for i in range(k)), "zero diagonal") + return k + + +def from_mask(k, mask): + require(type(k) is int and 2 <= k <= 6, "mask dimension") + require(type(mask) is int and 0 <= mask < 1 << (k * (k - 1)), + "edge mask") + rows = [0] * k + bit = 0 + for i in range(k): + for j in range(k): + if i != j: + rows[i] |= (mask >> bit & 1) << j + bit += 1 + return tuple(rows) + + +def literal(rows, field=0): + k = validate(rows) + require(k <= 6, "literal capacity") + require(type(field) is int and 0 <= field < 1 << (2 * k), "field") + total = 0 + for state in itertools.product(range(3), repeat=k): + ones = sum(1 << i for i in range(k) if state[i] == 1) + twos = sum(1 << i for i in range(k) if state[i] == 2) + parity = 0 + for i in range(k): + if ones >> i & 1: + parity ^= (rows[i] & twos).bit_count() & 1 + if state[i]: + parity ^= field >> (2 * i + state[i] - 1) & 1 + total += 1 - 2 * parity + return total + + +def subset_sum(rows): + k = validate(rows) + total = 0 + for sources in range(1 << k): + parity_row = 0 + for i in range(k): + if sources >> i & 1: + parity_row ^= rows[i] + if parity_row & ((1 << k) - 1 - sources) == 0: + total += 1 << (k - sources.bit_count()) + return total + + +def is_star(rows): + k = validate(rows) + edges = [(i, j) for i in range(k) for j in range(k) if rows[i] >> j & 1] + return len(edges) == 2 and (edges[0][0] == edges[1][0] + or edges[0][1] == edges[1][1]) + + +def local_equality(): + cases = 0 + equality = [] + edge_counts = {} + for mask in range(64): + if mask.bit_count() < 2: + continue + rows = from_mask(3, mask) + for field in range(64): + value = literal(rows, field) + expected = is_star(rows) and field == 0 + require(abs(value) <= 19, "local bound") + require((abs(value) == 19) == expected, "local equality") + if expected: + require(value == 19, "local positive sign") + equality.append([mask, field, value]) + cases += 1 + count = mask.bit_count() + edge_counts[count] = max(edge_counts.get(count, 0), abs(value)) + require(cases == 3648 and len(equality) == 6, "local coverage") + return {"cases": cases, "equality_rows": equality, + "max_absolute_by_edge_count": edge_counts} + + +def full_small(): + counts = {} + compared = 0 + classified = 0 + for k in (3, 4): + attained = 0 + bound = 19 * 3 ** (k - 3) + for mask in range(1 << (k * (k - 1))): + if mask.bit_count() < 2: + continue + rows = from_mask(k, mask) + value = subset_sum(rows) + require((value == bound) == is_star(rows), "full equality") + require(value <= bound, "full upper bound") + attained += value == bound + classified += 1 + if k == 3: + require(value == literal(rows), "independent local character") + compared += 1 + require(attained == k * (k - 1) * (k - 2), "labelled multiplicity") + counts[k] = attained + return {"classified": classified, "literal_comparisons": compared, + "attainers": counts} + + +def outside_extensions(): + # Fix the attaining core 0->1,0->2. Enumerate every remaining edge. + k = 5 + extra = [(i, j) for i in range(k) for j in range(k) + if i != j and (i >= 3 or j >= 3)] + require(len(extra) == 14, "outside edge coverage") + attained = 0 + for mask in range(1 << len(extra)): + rows = [6, 0, 0, 0, 0] + for bit, (i, j) in enumerate(extra): + rows[i] |= (mask >> bit & 1) << j + value = subset_sum(tuple(rows)) + require((value == 171) == (mask == 0), "outside rigidity") + attained += value == 171 + return {"extensions": 1 << len(extra), "attainers": attained} + + +def labelled_families(): + counts = {} + probes = 0 + for k in range(3, 9): + family = set() + for center in range(k): + others = [i for i in range(k) if i != center] + for a, b in itertools.combinations(others, 2): + for orientation in range(2): + rows = [0] * k + if orientation == 0: + rows[center] = (1 << a) | (1 << b) + else: + rows[a] = rows[b] = 1 << center + rows = tuple(rows) + require(rows not in family, "distinct labelled stars") + require(subset_sum(rows) == 19 * 3 ** (k - 3), + "attaining extension") + require(is_star(rows), "structural recognizer") + family.add(rows) + probes += 1 + require(len(family) == k * (k - 1) * (k - 2), "family cardinality") + counts[k] = len(family) + return {"probes": probes, "counts": counts} + + +def controls(): + invalid = [(), (0,), (0, 0, 0) * 5, [0, 0, 0], (True, 0, 0), + (-1, 0, 0), (8, 0, 0), (1, 0, 0)] + rejected = 0 + for rows in invalid: + try: + validate(rows) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid-domain control admitted") + star = (6, 0, 0) + require(literal(star) == 19 and literal(star, 1) != 19, + "omitted unary field must change equality") + require(not is_star((2, 4, 0)), "a directed path is not a star") + require(subset_sum((2, 4, 0)) < 19, "directed-path false equality") + require(subset_sum((2, 1, 0)) < 19, "reciprocal false equality") + require(subset_sum((6, 0, 0, 16, 0)) == 133 < 171, + "outside constant-sign cancellation") + require(subset_sum((14, 0, 0, 0)) == 55 < 57, + "three-arrow star false equality") + for field in range(1, 64): + require(abs(literal(star, field)) < 19, "outside attachment control") + return {"invalid_rejections": rejected, "semantic_checks": 6, + "nonzero_field_rejections": 63} + + +def main(): + result = {"marker": "PASS_BINARY_CHARACTER_EXTREMIZERS", + "claim_type": "scoped proof with exact finite equality lemma", + "local": local_equality(), "small": full_small(), + "outside": outside_extensions(), "families": labelled_families(), + "controls": controls(), "python": platform.python_version()} + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + hashes = {} + for name in names: + with (package / name).open("rb") as source: + data = source.read((1 << 20) + 1) + require(len(data) <= 1 << 20, "package-file capacity") + hashes[name] = hashlib.sha256(data).hexdigest() + result["sha256"] = hashes + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()