diff --git a/research/oneway-pair-correlation/PROOF.md b/research/oneway-pair-correlation/PROOF.md new file mode 100644 index 0000000000..587438ed6c --- /dev/null +++ b/research/oneway-pair-correlation/PROOF.md @@ -0,0 +1,107 @@ +# One-way coupled full guards have strictly negative correlation + +This scoped algebraic proof was produced by Nick Petalas. Apache-2.0. + +## Statement and cited inputs + +Let K be a finite field of order q, let m>=2, and let U,V be rank-one +idempotents on K^m with UV nonzero and VU=0. Set P=I-U and Q=I-V. +Choose G uniformly from the complete group GL_m(K). Let A and B be the +events that every leading principal minor through order m-1 of GPG^-1 +and GQG^-1, respectively, is nonzero. Write p=Pr(A)=Pr(B) and +J=Pr(A and B). Then + +```text +J < (1-q^(-m)) p^2 < p^2. +``` + +Consequently Cov(1_A,1_B) < -q^(-m) p^2. This answers Open next question 1 +of [#4769](https://github.com/CrocSwap/integer-mult-bounds/pull/4769). +It is a new inequality for the one-way coupling, using the counting laws +as cited dependencies. The binary strict-correlation result is already in +#4274; the all-field quantitative bound is new here. This is not a replay +or audit of the predecessor proofs. + +Use Nick Petalas's marginal law in +[#4227](https://github.com/CrocSwap/integer-mult-bounds/pull/4227) and +one-way joint law in #4769. Their exact retained proof blobs are pinned +as historical provenance in SOURCES.json. Put + +```text +n=m-1 >= 1, t=q^m, s=q^2-q+1, +alpha=s^2, beta=q^3-q+1, gamma=q^3-q^2+1. +``` + +The cited formulas, with the latter's rational normalization cancelled, are + +```text +p = (q-1)s^n / [q^n(t-1)], + +J = (q-1)[(q-1)alpha^n-(q-2)beta^n-gamma^n] + / [q^(2n)(t-1)(t-q)]. (1) +``` + +All denominators are positive and p>0. Dividing gives + +```text +J/p^2 = (t-1)/(t-q) * (1-D), +D = [(q-2)beta^n+gamma^n] / [(q-1)alpha^n]. (2) +``` + +## The new comparison + +The following identities hold for every real q>=2: + +```text +beta-gamma = q(q-1) > 0, +q*gamma-alpha = (q-1)^3 > 0. (3) +``` + +Also gamma=q^2(q-1)+1>0 and alpha>0. The nonnegative weights q-2 and 1 +sum to q-1, so (3) and the positive integer n give + +```text +D >= gamma^n/alpha^n > q^(-n). (4) +``` + +The first inequality is equality at q=2, but the second is always strict. +Insert (4) into (2), multiplying only by positive quantities: + +```text +J/p^2 < (t-1)/(t-q) * (1-q^(-n)) + = (t-1)/t + = 1-q^(-m). +``` + +This proves the claim in every characteristic, including extension fields. +There is no finite cutoff or untested tail. The polynomial comparison +holds for every real q>=2; the header probability interpretation requires +q to be a prime power. + +Nick Petalas's orthogonal-kernel comparison in +[#4767](https://github.com/CrocSwap/integer-mult-bounds/pull/4767) +uses 2*beta^n-gamma^n and q*beta-alpha. Here the joint law has a different +weighted correction, and its least base gamma suffices through the second +identity in (3). That proof pattern is predecessor credit. Only the +one-way correlation statement and its comparison are claimed here. + +## Complete-header hypothesis and limits + +A literal binary example shows why a restricted header catalogue does +not inherit the inequality. Take + +```text +U=[[1,1],[0,0]], V=[[0,0],[0,1]], G=[[1,0],[1,1]]. +``` + +Here UV is nonzero, VU=0, and G^-1=G. Both conjugated requests have first +diagonal entry 1, so both pass. If the header domain consists only of G, +then J=p=1, which violates the displayed bound. Thus a physical caller's +restricted catalogue needs a separate theorem. + +The argument supplies no header selection, emission, dispatch, dirty +restoration, precision, stock or complete physical invoice. Those costs +remain unknown. Two-way coupling and larger request families are outside +the claim. No new kappa, supplier admission, selected-frontier change or +complete multiplication theorem follows. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/oneway-pair-correlation/README.md b/research/oneway-pair-correlation/README.md new file mode 100644 index 0000000000..fd61284966 --- /dev/null +++ b/research/oneway-pair-correlation/README.md @@ -0,0 +1,104 @@ +# Strict one-way corank-one correlation over every finite field + +This scoped algebraic proof was produced by Nick Petalas. Apache-2.0. + +## Result and evidence + +Let U,V be rank-one idempotents over F_q^m with UV nonzero and VU=0. +The two requests I-U,I-V use a complete, uniformly weighted GL_m(F_q) +header. Each passes when every leading principal minor through order m-1 +is nonzero. For every finite field and every m>=2, + +```text +Pr(A and B) < (1-q^(-m)) Pr(A)Pr(B) < Pr(A)Pr(B). +``` + +This settles Open next question 1 of +[#4769](https://github.com/CrocSwap/integer-mult-bounds/pull/4769). +The new step in [PROOF.md](PROOF.md) uses +`q*gamma-alpha=(q-1)^3>0` to bound the one-way formula's weighted +correction in every dimension. The marginal and joint counting laws are +cited dependencies. Their proofs are not audited or rechecked here. +The binary strict-correlation result is already in #4274; the new claim +is the all-field quantitative bound. #4767 supplied the analogous +orthogonal-kernel proof pattern and retains its credit. + +The verifier checks the polynomial identity by coefficient convolution +and compares exact rational expressions at every integer +2<=q<=64, 2<=m<=65, a total of 4,032 parameter pairs. Non-prime-power q +check only the algebra. Five fixtures include q=4 and the one-way value +J=53/351 with p=49/117 at q=3,m=3. Ten scenario controls cover independence, +wrong or missing corrections, a literal singleton-header counterexample +and six invalid finite-check inputs. A separate reversed-sign polynomial +control also rejects. All checks remain active under optimized Python. +The generated stdout receipt binds all six package files by SHA256. +No receipt is handwritten or committed. + +This is an algebraic side result, with the explicit card scope change in +[TASK.json](TASK.json). [SOURCES.json](SOURCES.json) pins the task catalogue, +selected record and the three cited retained proofs as historical +provenance at canonical main 624de9dc66858af0945e5f8a0942488d62280d43. +There are no live external code inputs or third-party dependencies. + +## Reproduce + +From the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/oneway-pair-correlation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/oneway-pair-correlation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/oneway-pair-correlation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/oneway-pair-correlation --check-source-history +``` + +Use another CPython 3.12 installation in place of the local interpreter +path elsewhere. Expected markers are `PASS_ONEWAY_PAIR_CORRELATION`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The last command needs a publication commit and full Git history. +The direct verifier writes nothing and works from a Git-free package copy. + +## Limits and implementation constraints + +The universal statement rests on the written proof and cited counting +laws. Finite execution corroborates only the stated parameter domain. +Exactly two fixed one-way coupled kernels and the complete uniform header +domain are essential. The literal restricted-header example violates the +bound when its domain has one element. Two-way coupling and larger request +families remain open. + +Selection, emission, dispatch, dirty restoration, precision, stock and +the complete physical caller bill remain unknown. No new kappa, supplier +admission, selected-frontier change or complete multiplication theorem is +claimed. Independent human and formal proof-kernel review are unclaimed. +Lean, Docker and selected operator replay are unrun. + +The verifier has no recursion, subprocesses, dynamic code loading or +external mutable state. Its parameter grid stops at q=64,m=65; polynomial +inputs have at most four coefficients; fixtures and controls are fixed +finite tuples. Six sequential file reads each have a 1 MiB capacity check. +Every function is below 60 physical lines. Power of Ten rules 3 and 9 +have managed-runtime deviations for CPython allocation and standard +iterator dispatch, confined to these bounded domains. Explicit contracts, +normal and optimized warning-strict execution, and syntax diagnostics +check the affected paths. Fixed-capacity native arithmetic would require +a separately specified integer representation and is not supplied here. + +## Open next questions + +1. What correlation signs occur when both UV and VU are nonzero? This would + distinguish the remaining rank-one coupling types. First derive a joint + count for one named two-way pair and compare it with the cited marginal; + the one-way joint law does not apply to that pair. +2. Can a named odd-field producer use a fully charged one-way shared-header + caller? Pin its kernel pair and actual header domain, then price selection, + emission, dispatch, restoration and stock. Unknown physical costs block + any supplier consequence. Structured first steps are in TASK.json. + +## Credit + +Nick Petalas's #4769/#4274 supplied the one-way joint law, #4227 supplied +the corank-one marginal law, and #4767 supplied the orthogonal comparison +and its proof pattern. The earlier binary strict-correlation proof remains +#4274's credit. Cinna Davis supplied the BIT request context; source527, +commdata2338 and Jose Manuel retain normalizer and recursive-closure +lineage credit. No predecessor package is changed. diff --git a/research/oneway-pair-correlation/SOURCES.json b/research/oneway-pair-correlation/SOURCES.json new file mode 100644 index 0000000000..1b8f74a475 --- /dev/null +++ b/research/oneway-pair-correlation/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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-pair-correlation/PROOF.md", + "usage": "provenance", + "git_blob": "fd2522be59e8c4d992688c4b5a229e88792e136b", + "sha256": "a3db8d9bfb191e7cbeb04dd3b2844692e0e5e3574f0f4d461a5e685f17f24716" + }, + { + "path": "research/oneway-all-field-closed-form/PROOF.md", + "usage": "provenance", + "git_blob": "6ccfc8cc732a238e9897d68549c228bce318fc73", + "sha256": "e30ea17fea8614a5fae3294e18ffb478cbd835d1b6c6aff4cadb2ad3757f79aa" + }, + { + "path": "research/projector-header-density/PROOF.md", + "usage": "provenance", + "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d", + "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262" + } + ] +} diff --git a/research/oneway-pair-correlation/TASK.json b/research/oneway-pair-correlation/TASK.json new file mode 100644 index 0000000000..53c4a285a4 --- /dev/null +++ b/research/oneway-pair-correlation/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "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": "Prove strict negative correlation, with J < (1-q^(-m))Pr(A)Pr(B), for one-way coupled corank-one full guards over every finite field and m>=2.", + "scope_change_reason": "Take Open next question 1 of the merged one-way joint-law package #4769. This is a written algebraic side result, not a proof-assistant formalization or a predecessor audit.", + "bottleneck_link": "A quantified shared-header inequality resolves an open counting implication. It does not price a header producer or remove physical caller obligations, so it is not a supplier improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified dimension-uniform correlation bound and package it; leave other couplings and physical callers as open questions.", + "outcome": "completed", + "evidence": "PROOF.md; exact coefficient-convolution identity; all 4,032 integer parameter pairs 2<=q<=64,2<=m<=65; five rational fixtures; ten scenario controls plus one polynomial sign control; generated file-bound stdout receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What correlation signs occur when both UV and VU are nonzero?", + "why_it_matters": "It distinguishes the remaining coupling types of two rank-one kernels.", + "first_step": "Pin one two-way pair, derive its joint full-guard count, and compare it with the existing marginal law.", + "blocked_by": "The one-way joint law requires VU=0 and does not cover this pair." + }, + { + "question": "Can a named odd-field producer use a fully charged one-way shared-header caller?", + "why_it_matters": "A complete caller is needed before any header-density result can affect the supplier invoice.", + "first_step": "Pin the actual kernel pair and header domain, then price selection, emission, dispatch, dirty return and stock.", + "blocked_by": "No such physical producer or complete paid ledger is supplied." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131543", + "checked_at": "2026-10-22T19:46:02Z", + "upstream_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "coverage": "Complete cached pagination of 299 open PR bodies and 3,712 Discussion records; 105 local notes searched with 6,214 HEAD note paths omitted by sparse checkout. Main README and merged-PR searches for the formula, coupling and correlation were also run. Arbitrary diffs and unpublished work are outside coverage." + }, + "claim_type": "scoped algebraic proof with finite corroboration" +} diff --git a/research/oneway-pair-correlation/VERIFY.json b/research/oneway-pair-correlation/VERIFY.json new file mode 100644 index 0000000000..f444a635f0 --- /dev/null +++ b/research/oneway-pair-correlation/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": "Exact polynomial comparison, 4,032 rational parameter pairs, five fixtures, ten scenario controls and a polynomial sign control." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same explicit mathematical checks and rejection controls with assertions disabled." + } + ] +} diff --git a/research/oneway-pair-correlation/verify.py b/research/oneway-pair-correlation/verify.py new file mode 100644 index 0000000000..22eaa8ba0b --- /dev/null +++ b/research/oneway-pair-correlation/verify.py @@ -0,0 +1,141 @@ +"""Exact checks of the one-way correlation inequality; standard library only.""" + +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path + + +MAX_Q = 64 +MAX_M = 65 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def convolution(left: tuple[int, ...], right: tuple[int, ...]) -> tuple[int, ...]: + require(1 <= len(left) <= 4 and 1 <= len(right) <= 4, "polynomial capacity") + result = [0] * (len(left) + len(right) - 1) + for i, a in enumerate(left): + for j, b in enumerate(right): + result[i + j] += a * b + return tuple(result) + + +def check_polynomial() -> list[int]: + alpha = convolution((1, -1, 1), (1, -1, 1)) + q_gamma = (0, 1, 0, -1, 1) + difference = tuple(a - b for a, b in zip(q_gamma, alpha, strict=True)) + cube = convolution(convolution((-1, 1), (-1, 1)), (-1, 1)) + (0,) + require(difference == cube, "q gamma - alpha = (q-1)^3") + require(difference != tuple(-a for a in cube), "reversed-sign control") + return list(difference) + + +def probabilities(q: int, m: int) -> tuple[Fraction, Fraction]: + require(type(q) is int and 2 <= q <= MAX_Q, "q outside finite check domain") + require(type(m) is int and 2 <= m <= MAX_M, "m outside finite check domain") + n, t = m - 1, q**m + s, beta, gamma = q * q - q + 1, q**3 - q + 1, q**3 - q * q + 1 + p = Fraction((q - 1) * s**n, q**n * (t - 1)) + j = Fraction( + (q - 1) * ((q - 1) * s ** (2 * n) - (q - 2) * beta**n - gamma**n), + q ** (2 * n) * (t - 1) * (t - q), + ) + return p, j + + +def compare(q: int, m: int) -> Fraction: + p, j = probabilities(q, m) + n, t = m - 1, q**m + alpha, beta, gamma = (q * q - q + 1) ** 2, q**3 - q + 1, q**3 - q * q + 1 + correction = Fraction((q - 2) * beta**n + gamma**n, (q - 1) * alpha**n) + require(beta > gamma > 0, "ordered positive bases") + require(q * gamma - alpha == (q - 1) ** 3 > 0, "positive polynomial") + require(correction >= Fraction(gamma**n, alpha**n) > Fraction(1, q**n), + "dimension-uniform power comparison") + ratio = j / p**2 + require(ratio == Fraction(t - 1, t - q) * (1 - correction), "ratio identity") + require(0 <= j <= p <= 1, "probability ranges") + require(ratio < Fraction(t - 1, t) < 1, "strict quantitative bound") + return ratio + + +def restricted_header_control() -> None: + header = ((1, 0), (1, 1)) + u, v = ((1, 1), (0, 0)), ((0, 0), (0, 1)) + for i in range(2): + for j in range(2): + require(sum(header[i][k] * header[k][j] for k in range(2)) % 2 + == int(i == j), "literal header inverse") + uv = sum(u[i][k] * v[k][j] for k in range(2)) % 2 + vu = sum(v[i][k] * u[k][j] for k in range(2)) % 2 + require(uv == int(i == 0 and j == 1) and vu == 0, "one-way coupling") + for kernel in (u, v): + diagonal = sum(header[0][i] * (int(i == j) - kernel[i][j]) * header[j][0] + for i in range(2) for j in range(2)) % 2 + require(diagonal == 1, "both singleton full guards pass") + require(not Fraction(1) < Fraction(3, 4), "restricted-domain rejection") + + +def mutation_controls() -> int: + p, j = probabilities(2, 2) + upper = Fraction(3, 4) * p**2 + require(not p**2 < upper, "independence cannot pass") + denominator = 2**2 * (2**2 - 1) * (2**2 - 2) + for wrong_numerator in (9 + 5, 9): + mutant = Fraction(wrong_numerator, denominator) + require(not mutant < upper, "wrong or missing correction rejected") + require(j == Fraction(1, 6), "boundary fixture") + restricted_header_control() + rejected = 0 + for args in ((1, 2), (2, 1), (65, 2), (2, 66), (2.0, 2), (True, 2)): + try: + probabilities(*args) + except ValueError: + rejected += 1 + require(rejected == 6, "finite-domain rejection controls") + return 4 + rejected + + +def file_hashes() -> dict[str, str]: + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = package / name + require(path.stat().st_size <= 1024 * 1024, "package-file capacity") + hashes[name] = sha256(path.read_bytes()).hexdigest() + return hashes + + +def main() -> None: + polynomial = check_polynomial() + cases = 0 + for q in range(2, MAX_Q + 1): + for m in range(2, MAX_M + 1): + require(compare(q, m) < 1, "each comparison completed") + cases += 1 + fixtures = ((2, 2, "1/2", "1/6"), (2, 3, "9/28", "1/12"), + (3, 3, "49/117", "53/351"), (4, 2, "13/20", "7/20"), + (5, 2, "7/10", "13/30")) + examples = [] + for q, m, expected_p, expected_j in fixtures: + p, j = probabilities(q, m) + require(p == Fraction(expected_p) and j == Fraction(expected_j), + "exact fixture") + examples.append({"q": q, "m": m, "p": str(p), "J": str(j), + "J_over_p_squared": str(compare(q, m))}) + print(json.dumps({"status": "PASS_ONEWAY_PAIR_CORRELATION", + "claim_type": "scoped algebraic proof with finite corroboration", + "integer_parameter_cases": cases, "q_range": [2, MAX_Q], + "m_range": [2, MAX_M], "controls": mutation_controls(), + "q_gamma_minus_alpha_coefficients": polynomial, + "examples": examples, "sha256": file_hashes()}, sort_keys=True)) + + +if __name__ == "__main__": + main()