diff --git a/research/binary-character-remainder-gap/README.md b/research/binary-character-remainder-gap/README.md new file mode 100644 index 0000000000..26dfd91cd1 --- /dev/null +++ b/research/binary-character-remainder-gap/README.md @@ -0,0 +1,155 @@ +# A sharp uniform bound for the binary full-guard remainder spectrum + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +**Claim type: scoped mathematical proof with an exhaustive finite local lemma.** +For every zero-diagonal binary k-by-k matrix c, define the character sum +from Nick Petalas's [#4275](https://github.com/CrocSwap/integer-mult-bounds/pull/4275): + +```text +Z(c) = sum_{sigma in {0,1,2}^k} + (-1)^{sum_{i,j} c_ij [sigma_i=1] [sigma_j=2]}. +``` + +For every k >= 3, the spectrum has the following uniform separation: + +```text +c = 0: Z(c) = 3^k +exactly one nonzero entry: Z(c) = 7*3^(k-2) +at least two nonzero entries: 0 < Z(c) <= 19*3^(k-3). +``` + +The last bound is sharp at every k >= 3. Two arrows with a common tail, +c_12=c_13=1 and every other entry zero, attain it. At k=2 the only +two-entry character has Z=5. Thus the single-entry modes are exactly the +nontrivial maximum, and the rest are separated by a factor at most 19/21. + +This answers the structural-spectrum part of Ryanson Jonathan's +[#4607](https://github.com/CrocSwap/integer-mult-bounds/pull/4607) open +question without constructing the k=6 table of 2^30 characters. That +package supplies the five-event probability theorem and its open question; +its spectrum is cited context and is not replayed here. This result does +not prove the full-guard probability inequality for arbitrary k. + +## Proof + +### Positivity + +Fix S, the set of coordinates where sigma=1. Sum first over T, the subset +of S's complement where sigma=2. Binary character orthogonality gives + +```text +Z(c) = sum_{S: sum_{i in S} c_ij = 0 (mod 2) for every j outside S} 2^(k-|S|). +``` + +Every term is nonnegative and S empty contributes 2^k, so Z(c)>0. For one +arrow, exactly one of the nine assignments at its two endpoints has negative +sign. Its sum is seven; isolated coordinates multiply it by three. + +### The finite conditioned lemma + +Fix every coordinate outside a chosen set of h vertices. The exponent on +the remaining coordinates consists of their induced directed edges, an +arbitrary binary coefficient on each indicator [sigma_i=1] and +[sigma_i=2], and one constant. The constant changes only the sign. All +possible induced fields must be allowed, even when they do not arise from +a particular outside graph. + +The following exhaustive finite lemma bounds the absolute value of this +conditioned sum. The verifier evaluates every edge mask and every one of +the 2^(2h) fields by its literal 3^h signed assignments. The maxima by +number of directed edges are: + +```text +h=2: one edge 7; two edges 5. +h=3: one edge 21; two edges 19; three edges 17; + four edges 15; five edges 13; six edges 15. +``` + +The two-edge h=2 row has 16 field cases. The h=3 rows with at least two +edges have 57*64=3648 graph/field cases. All are enumerated. This finite +lemma, rather than an extrapolation of small spectra, is the +computer-assisted component of the universal proof. + +### Exhaustive graph split + +View the nonzero entries of c as directed arrows with no loops. + +1. If a reciprocal pair occurs, condition outside its two vertices. The + two-edge lemma and the triangle inequality give Z(c) <= 5*3^(k-2), + which is at most 19*3^(k-3). +2. Otherwise, if two arrows share a vertex, their endpoints form a set of + three vertices containing at least two arrows. Its induced graph may + contain further arrows. Every corresponding row of the h=3 lemma is + at most 19. Conditioning and summing over outside assignments gives + Z(c) <= 19*3^(k-3). +3. If neither case occurs, the arrows form a directed matching. For r>=2 + arrows the sum factors as 7^r*3^(k-2r). Its ratio to 3^k is + (7/9)^r <= 49/81 < 19/27. + +These cases cover every matrix with at least two entries. The two-arrow +common-tail example has sum 9+9+1=19, according to whether its central +coordinate is 0, 2 or 1. Padding it with isolated coordinates proves sharpness. + +## Reproduction and evidence + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/binary-character-remainder-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/binary-character-remainder-gap +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/binary-character-remainder-gap --check-source-history +``` + +Other machines may substitute their CPython 3.12 path. The direct command +prints `PASS_BINARY_CHARACTER_REMAINDER_GAP` in a generated JSON receipt +bound to all five package files. It writes no files. Both registered +commands run the same checks, normally and with -O, with warnings as errors. + +The verifier enumerates every conditioned two- and three-vertex graph, +including all unary fields. It also checks the proof's graph split and +bound on every zero-diagonal character at k=2,3,4, comparing the literal +sum with the separate positive subset formula. These are new-lemma +checks, without predecessor code or a predecessor spectrum table. +Controls reject invalid dimensions, nonzero diagonal, negative or Boolean +rows, a false bound of 18, and reciprocal-pair misclassification. Padded +sharpness examples are checked at every k=3..8. + +## Scope, credit and limits + +Nick Petalas's #4275 supplies the exact character formula and header +interpretation. Ryanson Jonathan's #4607 supplies the explicit structural +remainder question and five-event predecessor theorem. Nick Petalas's +#4599 supplies the earlier four-event result. Cinna Davis supplied the BIT +request context; source527, commdata2338 and Jose Manuel retain the +normalizer lineage credit. Exact retained sources are provenance-only pins +in SOURCES.json. No predecessor executable or spectrum table is imported. + +The independent-moment card is explicitly changed to this original +spectral side result. It concerns shared-header densities, and does not +reprice a paid supplier. The claim is restricted to binary characters with +zero diagonal and the exact three-state weights above. An arbitrary +signed or reweighted distribution has a different spectrum. No probability +comparison at all k, general negative association, request producer, +header selection/emission, physical invoice, supplier admission, new kappa +or complete multiplication theorem is established. Lean, Docker, selected +cold replay and independent human review are unrun. + +All loops have fixed finite checker domains: local dimensions at most +three, full character dimension at most four, and sharpness dimension at +most eight. There is no recursion or dynamic code execution. Functions +fit within sixty lines. CPython dynamic allocation deviates from fixed +allocation; these bounds and one-MiB package-file limits bound live work. +Warning-strict normal and optimized runs are the available diagnostics. + +## Open next questions + +1. Can this uniform 19/21 remainder gap prove an explicit eventual + full-guard product inequality for every fixed k? First combine it with + the k(k-1) negative single-entry modes and the exact finite-GL factor + in #4275. The resulting dimension threshold may be large; dimensions + below it remain a separate obligation. +2. Which character graphs attain 19*3^(k-3)? First classify equality in + the conditioned local lemma and its outside-field triangle inequality. + This package provides a sharp family but no complete equality classification. diff --git a/research/binary-character-remainder-gap/SOURCES.json b/research/binary-character-remainder-gap/SOURCES.json new file mode 100644 index 0000000000..b0b8a8f5db --- /dev/null +++ b/research/binary-character-remainder-gap/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/corankone-triple-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8", + "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f" + }, + { + "path": "research/five-event-guard-correlation/README.md", + "usage": "provenance", + "git_blob": "ffcdb61c6e3619f440453e18499ecf6a7a2b3f6f", + "sha256": "1fb2d6ae867323dc1330bb5581def650b1d1c81e365043b104db73d803ebcb19" + } + ] +} diff --git a/research/binary-character-remainder-gap/TASK.json b/research/binary-character-remainder-gap/TASK.json new file mode 100644 index 0000000000..b6430fdd80 --- /dev/null +++ b/research/binary-character-remainder-gap/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "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_status": "changed", + "actual_scope": "Prove the sharp uniform 19*3^(k-3) bound for every binary full-guard character with at least two entries.", + "scope_change_reason": "Takes Ryanson Jonathan #4607 structural-spectrum open question, as original mathematics rather than a paid-ledger audit.", + "bottleneck_link": "Scoped shared-header spectral side result; no physical caller or paid-profile change.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified structural bound; leave probability consequences and equality classification open.", + "outcome": "completed", + "evidence": "README.md contains the universal reduction; verify.py exhausts its conditioned local lemma and generates a source-hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the uniform remainder gap give an explicit eventual product inequality for each fixed k?", + "why_it_matters": "Would replace a full character table for large dimensions.", + "first_step": "Combine the remainder gap, negative single-entry multiplicity, and exact finite-GL factor of #4275.", + "blocked_by": "An explicit dimension threshold and all lower dimensions remain unproved." + }, + { + "question": "Which character graphs attain the remainder bound?", + "why_it_matters": "Would determine the exact third-mode multiplicity.", + "first_step": "Analyze equality in the local lemma and conditioned triangle inequality.", + "blocked_by": "Only one sharp family is proved; complete equality classification is absent." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144279", + "upstream_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "priority_revision": 7, + "overlap_utc": "2026-10-23T10:55:00Z", + "coverage": "Live 100 open PRs and 200 own PRs; 40 recent hub comments and 12 active discussions; targeted all-main README and merged-PR searches. Overlap cache covers 305 open PRs at 2026-10-23T10:52:39Z and 4291 Discussion records at 10:53:31Z, both completely paginated. Sparse local helper searches 167 of 6918 main notes, supplemented by targeted git grep on origin/main. Unpublished work and arbitrary code diffs excluded." + } +} diff --git a/research/binary-character-remainder-gap/VERIFY.json b/research/binary-character-remainder-gap/VERIFY.json new file mode 100644 index 0000000000..79f07e4252 --- /dev/null +++ b/research/binary-character-remainder-gap/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive conditioned local lemma, structural graph split, positive subset identity, sharpness and invalid/false-bound controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same theorem checks and explicit rejection controls under optimized Python." + } + ] +} diff --git a/research/binary-character-remainder-gap/verify.py b/research/binary-character-remainder-gap/verify.py new file mode 100644 index 0000000000..c6bce36d53 --- /dev/null +++ b/research/binary-character-remainder-gap/verify.py @@ -0,0 +1,180 @@ +"""Exact local lemma and finite corroboration for the uniform character bound.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def checked_rows(rows): + k = len(rows) + need(2 <= k <= 8, "finite checker supports dimensions 2 through 8") + need(all(type(row) is int and 0 <= row < 1 << k for row in rows), + "invalid binary row") + need(all(not (row >> i & 1) for i, row in enumerate(rows)), + "character matrix must have zero diagonal") + return k + + +def character(rows, fields=0): + """Literal three-state sum, including arbitrary unary fields.""" + k = checked_rows(rows) + need(type(fields) is int and 0 <= fields < 1 << (2 * k), "invalid field") + total = 0 + for states in itertools.product(range(3), repeat=k): + right = sum(1 << j for j, state in enumerate(states) if state == 2) + parity = sum((rows[i] & right).bit_count() + for i, state in enumerate(states) if state == 1) + parity += sum(fields >> (2 * i + state - 1) & 1 + for i, state in enumerate(states) if state) + total += 1 if parity % 2 == 0 else -1 + return total + + +def subset_character(rows): + """Sum out all label-2 coordinates by exact binary orthogonality.""" + k = checked_rows(rows) + total = 0 + for left in range(1 << k): + xor_row = 0 + for i in range(k): + if left >> i & 1: + xor_row ^= rows[i] + if xor_row & (((1 << k) - 1) ^ left) == 0: + total += 1 << (k - left.bit_count()) + return total + + +def matrix(k, mask): + edges = tuple((i, j) for i in range(k) for j in range(k) if i != j) + need(0 <= mask < 1 << len(edges), "edge mask outside finite domain") + rows = [0] * k + for bit, (i, j) in enumerate(edges): + if mask >> bit & 1: + rows[i] |= 1 << j + return tuple(rows) + + +def local_lemma(): + """Enumerate every local graph and every induced unary field.""" + summary = {} + for k in (2, 3): + maxima = {} + counts = {} + witnesses = {} + for mask in range(1 << (k * (k - 1))): + weight = mask.bit_count() + if not weight: + continue + for fields in range(1 << (2 * k)): + value = abs(character(matrix(k, mask), fields)) + counts[weight] = counts.get(weight, 0) + 1 + if weight not in maxima or value > maxima[weight]: + maxima[weight] = value + witnesses[weight] = [mask, fields] + expected = {1: 7, 2: 5} if k == 2 else { + 1: 21, 2: 19, 3: 17, 4: 15, 5: 13, 6: 15} + need(maxima == expected, "conditioned local lemma failed") + summary[k] = {"max_abs_by_entries": maxima, + "field_cases_by_entries": counts, + "maximizers": witnesses} + return summary + + +def structural_case(rows): + """Return the exhaustive graph case used by the universal proof.""" + k = checked_rows(rows) + edges = tuple((i, j) for i in range(k) for j in range(k) + if rows[i] >> j & 1) + if len(edges) <= 1: + return "zero" if not edges else "single" + for i, j in edges: + if rows[j] >> i & 1: + return "reciprocal" + for a in range(len(edges)): + for b in range(a): + if set(edges[a]) & set(edges[b]): + return "three_vertices" + need(len({v for edge in edges for v in edge}) == 2 * len(edges), + "remaining graph is not a directed matching") + return "matching" + + +def finite_corroboration(): + counts = {} + for k in range(2, 5): + classes = dict.fromkeys( + ("zero", "single", "reciprocal", "three_vertices", "matching"), 0) + for mask in range(1 << (k * (k - 1))): + rows = matrix(k, mask) + value = character(rows) + need(value == subset_character(rows) and value >= 1 << k, + "positive subset identity differs from literal character") + case = structural_case(rows) + classes[case] += 1 + if case == "zero": + need(value == 3 ** k, "zero character differs") + elif case == "single": + need(value == 7 * 3 ** (k - 2), "single-entry mode differs") + elif k == 2: + need(value == 5, "two-coordinate reciprocal value differs") + else: + need(value <= 19 * 3 ** (k - 3), "uniform remainder bound fails") + counts[k] = classes + return counts + + +def rejection_controls(): + invalid = ((0,), (1, 0), (0, -1), (False, 0), (0,) * 9) + rejected = 0 + for rows in invalid: + try: + character(rows) + except ValueError: + rejected += 1 + need(rejected == len(invalid), "invalid-domain control was accepted") + star = (6, 0, 0) + need(character(star) == 19 and character(star) > 18, + "strictly smaller remainder bound must fail") + need(character((2, 1)) == 5 and character((2, 1)) != 7, + "two reciprocal entries cannot be a single-entry mode") + for k in range(3, 9): + need(character((6,) + (0,) * (k - 1)) == 19 * 3 ** (k - 3), + "padded sharpness example fails") + need(49 * 27 < 19 * 81, "matching comparison fails") + return {"invalid_domains_rejected": rejected, + "false_strict_bound_rejected": True, + "reciprocal_misclassification_rejected": True, + "sharpness_dimensions": list(range(3, 9))} + + +def source_hashes(): + package = Path(__file__).resolve().parent + expected = {"README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"} + files = {path.name for path in package.iterdir() if path.is_file()} + need(files == expected, "unexpected or missing package file") + hashes = {} + for name in sorted(expected): + path = package / name + need(path.stat().st_size <= 1024 * 1024, "package file exceeds read bound") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def main(): + result = {"status": "PASS_BINARY_CHARACTER_REMAINDER_GAP", + "local_lemma": local_lemma(), + "finite_characters": finite_corroboration(), + "controls": rejection_controls(), + "source_sha256": source_hashes(), + "no_new_kappa": True} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()