diff --git a/research/triangular-parity-sign-cube/README.md b/research/triangular-parity-sign-cube/README.md new file mode 100644 index 0000000000..dc6ca88690 --- /dev/null +++ b/research/triangular-parity-sign-cube/README.md @@ -0,0 +1,154 @@ +# Every full-support signed n=8 symbol has prefix maximum 23/16 + +**Claim type: complete finite certificate**, with an elementary attaining-row +argument. For every one of the 128 symbols + +```text +f = (1, s1/8, s2/16, s3/16, s4/16, s5/16, s6/16, s7/16), +sj in {-1,+1}, +``` + +the largest proper forward-prefix infinity norm of the even-first triangular +parity compiler is exactly **23/16**. Every symbol first attains this value +after macro 11 and retains it through macro 21. All 128 symbols are extremizers. +Their tail l1 is 1/2. The completed Toeplitz matrix has norm 3/2. + +This replaces individual sign examples by an exhaustive result for this fixed +magnitude family. Brian's [general forward-prefix theorem](../triangular-parity-forward-bound/README.md) +already gives 3/2 at tail budget 1/2. The new finite envelope is sharper by 1/16. +This certificate does not establish a sharper bound for other magnitudes, interior +points of a coefficient box, arbitrary dimensions, or child interleavings. +No new kappa, supplier admission or complete multiplication theorem is claimed. + +## Schedule and exact certificate + +Use ordinary power-coordinate indices 0,...,7 throughout. At each node split +`f(z)=e(z^2)+z o(z^2)` and compute truncated series + +```text +k = o/e, s = e-z o k, +U = [I, T(zk); 0, I], L = [I, 0; T(k), I], +T(f) = L diag(T(e),T(s)) U. +``` + +The displayed blocks use even/odd order. The verifier embeds them directly +on the corresponding ordinary coordinate indices. Execute `U`, the entire +even child, the entire Schur child, then `L`, repeating this order at each +node. Include one identity factor at each scalar leaf. Thus the schedule has +22 factors and 21 nonempty proper prefixes. The identity initial cut, if +included, has norm one and does not change any maximum. + +[verify.py](verify.py) independently implements this definition with exact +`Fraction` arithmetic. It constructs the fixed 15-node tree without recursion, +multiplies every chronological 8-by-8 prefix, and compares the final product +to the literal lower-triangular Toeplitz matrix. It imports no predecessor +verifier and does not run a predecessor's certificate. + +The maximum at each cut, taken over the complete 128-symbol domain, is: + +| Proper cut | Maximum infinity norm over all signs | +|---|---| +| 1 through 5 | 2601/2048 | +| 6 through 9 | 21/16 | +| 10 | 85/64 | +| 11 through 21 | 23/16 | + +These are exact maxima from all 2,688 prefix matrices. They are not interval +upper estimates or floating-point results. Each symbol's own maximum is +23/16, even though its earlier cut norms can differ from this table. + +The attaining row has a short explanation. At cut 11 the even child is +complete, so the even output rows are the upper block of +`diag(E,I) U`, namely `[E, zO]`. Its last row, which is ordinary row 6, +contains `f0,...,f6` in permuted order. Its absolute row sum is + +```text +1 + 1/8 + 5/16 = 23/16. +``` + +The Schur-child macros change only odd rows. Row 6 therefore retains that +sum through cut 21. The finite exact enumeration supplies the matching upper +bound at every earlier and later proper cut. It also verifies that no symbol +attains 23/16 before cut 11. The completed last row includes f7, giving 3/2. + +## Reproduce + +From the repository root, with standard-library CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/triangular-parity-sign-cube/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/triangular-parity-sign-cube/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/triangular-parity-sign-cube +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/triangular-parity-sign-cube --check-source-history +``` + +Expected status is `PASS_TRIANGULAR_PARITY_SIGN_CUBE`, with `symbols=128`, +`proper_prefixes=2688`, and `maximum_distribution={"23/16":128}`. +Adding `--details` to either direct invocation emits every sign tuple and +all of its 21 exact cut norms. The generated receipt includes the SHA256 +of this entire ordered certificate and of all five package source files. +It writes nothing. No receipt is hand-written or retained as a separate claim. + +Eight controls reject the wrong root-left sign, a missing root-left shear, +reversed macro order, an omitted symbol, a duplicated symbol, an omitted cut, +a wrong reported maximum, and inclusion of the completed cut as a proper cut. +Explicit exceptions keep every check active under `-O`. + +The verifier uses Python-managed allocation and exact rational objects. This +is a Power of Ten rule-3 deviation: literal allocation-free steady execution +conflicts with `Fraction` and the interpreter. All mathematical work is bounded +by 128 inputs, a 15-node tree, 22 factors and 8-by-8 matrices. The five control +copies are bounded by the same domain. The fixed finite input and no-write +interface constrain live storage; no arbitrary input size is accepted. +Functions stay below 60 lines, loops have explicit finite domains, and there +is no recursion, dynamic evaluation or external command. Warning-strict normal +and optimized replay are registered. No separate static analyzer was available on PATH. + +## Scope, sources and credit + +This contribution is produced by Nick Petalas. Independent human and formal +proof-kernel review are unclaimed. Apache-2.0. + +Credit James Reed for the one-split bound, the nested-prefix question and the +single-symbol series, including +[#4811](https://github.com/CrocSwap/integer-mult-bounds/pull/4811), +[#4812](https://github.com/CrocSwap/integer-mult-bounds/pull/4812), +[#4815](https://github.com/CrocSwap/integer-mult-bounds/pull/4815), +[#4816](https://github.com/CrocSwap/integer-mult-bounds/pull/4816), +[#4820](https://github.com/CrocSwap/integer-mult-bounds/pull/4820), +[#4821](https://github.com/CrocSwap/integer-mult-bounds/pull/4821) and +[#4822](https://github.com/CrocSwap/integer-mult-bounds/pull/4822). +Their individual values remain their results. The original addition here is +the complete sign-family certificate and its sharp cut envelope. + +Credit JoyboyBrian for the +[all-depth four-cut envelope](../triangular-parity-uniform-prefix/README.md) +and its [sharp forward-prefix successor](../triangular-parity-forward-bound/README.md), +which already settles the general 1+eta question; Vlado Vojdanovski for +the shallow parity compiler retained by Cinna Davis in +[SHALLOW-TOEPLITZ.md section 3](../unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md); +and Ryanson Jonathan for the caller's error-ledger context in +[one-factor-of-t](../one-factor-of-t/README.md). No predecessor credit line is changed. + +Canonical base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +[SOURCES.json](SOURCES.json) pins exact source bytes; [TASK.json](TASK.json) +records the changed scope and bounded overlap coverage. The card's historical +baseline command has been superseded by `scripts/research_selected_baseline.py`, +which passed as a source-binding positive control. The selected conditional +record remains kappa=60403/20000000. That orientation check is not a theorem replay. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132735) +reserved this finite sign-family question. + +## Open next questions + +1. Is 23/16 still the exact maximum for this finite family under every legal + child interleaving? Enumerating pairs of legal child cuts is a feasible first + step. This certificate fixes even-first execution; the general theorem gives + only the weaker 3/2 bound for these schedules. +2. Can one derive an analytic coefficient-sensitive envelope that explains + the 1/16 improvement? Start with the row support omitted by the unfinished + root left shear. The fixed-magnitude enumeration does not supply that formula. + +Full gate-level stability, generator normalization, the completed Gaussian +stage, fixed-tape implementation and the dyadic p^100 precision ledger were +not run or proved. There is no complete recursive invoice to admit here. diff --git a/research/triangular-parity-sign-cube/SOURCES.json b/research/triangular-parity-sign-cube/SOURCES.json new file mode 100644 index 0000000000..9f6c318d8e --- /dev/null +++ b/research/triangular-parity-sign-cube/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/triangular-parity-uniform-prefix/README.md", + "usage": "input", + "git_blob": "6e64fb48fbd33b9742f0ba81de77bfb661b80403", + "sha256": "dd0259414df08b5b462cec450df5a0618c30ba112ddf87b2acbb2e39a1c69414" + }, + { + "path": "research/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md", + "usage": "input", + "git_blob": "bc4349b2daea548ffa09e1f38a31f1df86b0b7be", + "sha256": "b384b93f3fb4a8c97da2e617ebc14d55cebb0a739070e7f8dbb66f63e24e9310" + }, + { + "path": "research/triangular-parity-forward-bound/README.md", + "usage": "input", + "git_blob": "d008710585a897b9b568e74c7b867d8c784e4aa8", + "sha256": "745c2105fc614e6ba453327a37e483b808425a40ce3e2b44e2643b0ea1db3781" + } + ] +} diff --git a/research/triangular-parity-sign-cube/TASK.json b/research/triangular-parity-sign-cube/TASK.json new file mode 100644 index 0000000000..c585918a6e --- /dev/null +++ b/research/triangular-parity-sign-cube/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact proper forward-prefix infinity norms for all 128 full-support n=8 symbols with f1=+/-1/8 and f2,...,f7=+/-1/16, using even-first macro execution.", + "scope_change_reason": "The all-size audit card is narrowed to an original complete finite sign-family result suggested by James Reed's single-sign examples. This does not discharge a quantified transfer premise.", + "bottleneck_link": "Scoped precision side result: identifies the exact finite envelope before the root left shear. All-size, gate-level and Gaussian caller precision costs remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first original verified finite law; do not expand to other magnitudes or dimensions.", + "outcome": "completed", + "evidence": "All 128 distinct sign symbols, 2688 proper macro prefixes and 128 independent Toeplitz endpoint identities are checked exactly. Every symbol has maximum 23/16, first attained at cut 11. Eight enumerated mutation controls must fail.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is 23/16 still the exact maximum for this finite family under every legal child interleaving?", + "why_it_matters": "The retained parallel compiler permits other child schedules.", + "first_step": "Enumerate pairs of legal child cuts for the fixed 128-symbol domain.", + "blocked_by": "The certificate fixes even-first execution; the general theorem gives only 3/2." + }, + { + "question": "Is there an analytic coefficient-sensitive envelope explaining the 1/16 improvement?", + "why_it_matters": "It could replace finite family-specific enumeration.", + "first_step": "Analyze the row support omitted by the unfinished root left shear.", + "blocked_by": "The fixed-magnitude census does not supply a coefficient-variable formula." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132735", + "upstream_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "open_prs_at": "2026-10-22T21:08:49Z", + "open_pr_records": 348, + "discussion_records": 3780, + "discussion_fetched_at": "2026-10-22T21:09:37Z", + "coverage_limit": "Remote snapshots are paginated but not atomic; sparse local metadata is incomplete and arbitrary diffs are not searched. Distinctive README searches use all of origin/main.", + "precommit_upstream": "624de9dc66858af0945e5f8a0942488d62280d43", + "precommit_overlap": "Fresh open PRs and 30 latest handoff comments checked at 2026-10-22T21:13Z; no same-question claim. Distinct concurrent eta>1 and gate-cut tasks are excluded." + } +} diff --git a/research/triangular-parity-sign-cube/VERIFY.json b/research/triangular-parity-sign-cube/VERIFY.json new file mode 100644 index 0000000000..a5e64021d5 --- /dev/null +++ b/research/triangular-parity-sign-cube/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/triangular-parity-forward-bound/README.md", + "research/triangular-parity-uniform-prefix/README.md", + "research/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All 128 sign symbols, all 2688 proper prefixes, all 128 Toeplitz endpoints, the sharp cut envelope, and eight rejecting controls; source-hash-bound generated receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All 128 sign symbols, all 2688 proper prefixes, all 128 Toeplitz endpoints, the sharp cut envelope, and eight rejecting controls; source-hash-bound generated receipt." + } + ] +} diff --git a/research/triangular-parity-sign-cube/verify.py b/research/triangular-parity-sign-cube/verify.py new file mode 100644 index 0000000000..6cb7a44a4e --- /dev/null +++ b/research/triangular-parity-sign-cube/verify.py @@ -0,0 +1,182 @@ +#!/usr/bin/env python3 +"""Exact complete sign-family certificate. Standard library, no file writes.""" + +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys + + +CUT_MAXIMA = [F(2601, 2048)] * 5 + [F(21, 16)] * 4 + [F(85, 64)] + [F(23, 16)] * 11 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(): + return [[F(i == j) for j in range(8)] for i in range(8)] + + +def multiply(a, b): + return [[sum((a[i][k] * b[k][j] for k in range(8)), F(0)) + for j in range(8)] for i in range(8)] + + +def norm(a): + return max(sum(map(abs, row), F(0)) for row in a) + + +def split(symbol): + require(len(symbol) in (2, 4, 8) and symbol[0] == 1, "bad node") + even, odd = symbol[::2], symbol[1::2] + m = len(even) + quotient = [F(0)] * m + for j in range(m): + quotient[j] = odd[j] - sum( + (even[k] * quotient[j-k] for k in range(1, j+1)), F(0)) + schur = even.copy() + for j in range(1, m): + schur[j] -= sum((odd[k] * quotient[j-1-k] for k in range(j)), F(0)) + require(schur[0] == even[0] == 1, "constant term changed") + return even, schur, quotient + + +def compile_symbol(symbol, wrong_sign=False): + """Breadth-first split, then bottom-up assemble the fixed 15-node tree.""" + require(len(symbol) == 8 and symbol[0] == 1, "bad root") + nodes = {1: (list(range(8)), list(symbol))} + quotients = {} + for node in range(1, 8): + indices, current = nodes[node] + even, schur, quotient = split(current) + nodes[2*node] = (indices[::2], even) + nodes[2*node+1] = (indices[1::2], schur) + quotients[node] = quotient + words = {node: [identity()] for node in range(8, 16)} + for node in range(7, 0, -1): + indices, _ = nodes[node] + evens, odds = indices[::2], indices[1::2] + m = len(evens) + upper, lower = identity(), identity() + quotient = quotients[node] + for i in range(m): + for j in range(i+1): + lower[odds[i]][evens[j]] = quotient[i-j] + if i > j: + upper[evens[i]][odds[j]] = quotient[i-j-1] + if wrong_sign and node == 1: + lower[1][0] *= -1 + words[node] = [upper] + words[2*node] + words[2*node+1] + [lower] + require(len(words[1]) == 22, "wrong schedule length") + return words[1] + + +def toeplitz(symbol): + return [[symbol[i-j] if i >= j else F(0) for j in range(8)] + for i in range(8)] + + +def execute(symbol, factors): + require(len(factors) == 22, "missing macro") + state = identity() + prefix_norms = [] + for step in range(22): + state = multiply(factors[step], state) + if step < 21: + prefix_norms.append(norm(state)) + require(state == toeplitz(symbol), "wrong endpoint") + return prefix_norms + + +def census(): + rows = [] + for signs in product((-1, 1), repeat=7): + symbol = [F(1), F(signs[0], 8)] + [F(s, 16) for s in signs[1:]] + require(sum(map(abs, symbol[1:]), F(0)) == F(1, 2), "tail budget") + values = execute(symbol, compile_symbol(symbol)) + rows.append({"signs": list(signs), "maximum": str(max(values)), + "prefix_norms": list(map(str, values))}) + require(len(rows) == 128, "incomplete sign domain") + return rows + + +def check_census(rows): + require(len(rows) == 128, "incomplete sign domain") + domain = set(product((-1, 1), repeat=7)) + require({tuple(row["signs"]) for row in rows} == domain, "wrong sign domain") + for row in rows: + values = list(map(F, row["prefix_norms"])) + require(len(values) == 21, "incomplete cut domain") + require(max(values) == F(row["maximum"]) == F(23, 16), "wrong maximum") + require(values.index(F(23, 16)) == 10, "wrong first attaining cut") + maxima = [max(F(row["prefix_norms"][j]) for row in rows) for j in range(21)] + require(maxima == CUT_MAXIMA, "wrong cut envelope") + + +def controls(): + symbol = [F(1), F(1, 8)] + [F(1, 16)] * 6 + factors = compile_symbol(symbol) + missing_left = factors.copy() + missing_left[-1] = identity() + reversed_order = list(reversed(factors)) + mutants = (compile_symbol(symbol, wrong_sign=True), missing_left, reversed_order) + rejected = 0 + for factors in mutants: + try: + execute(symbol, factors) + except ValueError as error: + require(str(error) == "wrong endpoint", "unexpected control failure") + rejected += 1 + require(rejected == 3, "endpoint mutation accepted") + return ["wrong_root_left_sign", "missing_root_left", "reversed_macro_order"] + + +def census_controls(rows): + mutants = [rows[:-1], [rows[0]] + rows[1:-1] + [rows[0]]] + for kind in ("omitted_cut", "wrong_maximum", "completed_cut_is_proper"): + changed = json.loads(json.dumps(rows)) + if kind == "omitted_cut": + changed[0]["prefix_norms"].pop() + elif kind == "wrong_maximum": + changed[0]["maximum"] = "3/2" + else: + changed[0]["prefix_norms"][-1] = "3/2" + mutants.append(changed) + rejected = 0 + for changed in mutants: + try: + check_census(changed) + except ValueError: + rejected += 1 + require(rejected == 5, "census mutation accepted") + return ["omitted_symbol", "duplicated_symbol", "omitted_cut", + "wrong_maximum", "completed_cut_is_proper"] + + +def main(): + require(sys.argv[1:] in ([], ["--details"]), "usage: verify.py [--details]") + rows = census() + check_census(rows) + distribution = Counter(row["maximum"] for row in rows) + package = Path(__file__).resolve().parent + source_hashes = {name: sha256((package / name).read_bytes()).hexdigest() + for name in ("verify.py", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json")} + receipt = {"status": "PASS_TRIANGULAR_PARITY_SIGN_CUBE", "symbols": 128, + "proper_cuts_per_symbol": 21, "proper_prefixes": 2688, + "maximum_distribution": dict(distribution), + "cut_maxima": list(map(str, CUT_MAXIMA)), + "controls": controls() + census_controls(rows), + "certificate_sha256": sha256(json.dumps(rows, sort_keys=True).encode()).hexdigest(), + "source_sha256": source_hashes} + if sys.argv[1:] == ["--details"]: + receipt["certificate"] = rows + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()