diff --git a/research/compact-maximal-invariant-guard/PROOF.md b/research/compact-maximal-invariant-guard/PROOF.md new file mode 100644 index 0000000000..18b47a9af4 --- /dev/null +++ b/research/compact-maximal-invariant-guard/PROOF.md @@ -0,0 +1,152 @@ +# A maximal invariant guard on one complete two-digit quotient + +This contribution was produced by Nick Petalas. Claim type: finite optimal-guard +certificate with a scoped written invariance and repair argument. Apache-2.0. + +## Contract + +Use the unchanged later-source compact word in Douglas Colkitt's +`notes/compact-control-movement.tex`, with the explicit packed semantics in +Arham Tahir's PR1603. Fix + +```text +n=2, K=3, G=1, rho=2, B=2, C=B^n=4, Y=2^((n+1)K-rho)=128. +s=(y,t,u,c), 0<=y<128, 0<=t,u,c<4. +``` + +Here y is the target quotient after removing its two unchanged low bits. +Both processed source bits are in c, and t,u are the complete compact fields. +All upper target bits remain. In particular, equality modulo 16, the width +of the observed selected bits, is insufficient. The full target has nine +bits, the quotient has seven, and the omitted highest selected bit is retained +in the comparison. Source spectators and the arbitrary back field retain +the source note's unchanged swap-sandwich contract. + +For two-bit z, define + +```text +m(z) = z_0 + 8 z_1 +p(y) = bit_0(y) + 2 bit_3(y). +``` + +The earlier-source map P_z on y,t consists of these four updates, in order: + +```text +y += 2(z_0 t_0 + 8 z_1 t_1) modulo 128 +t += p(y) modulo 4 +y += z_0(1-2t_0) + 8z_1(1-2t_1) modulo 128 +t -= p(y XOR m(z)) modulo 4. +``` + +Every t digit is read from its current value. At radix two, the control +parities equal the two-bit integer u and loading c means u+c modulo four. +Thus S applies P_u and P_((u+c) mod 4), returning u,c unchanged. The intended +involution is T(s)=(y XOR m(c),t,u,c). Each elementary rotation is independent +of its destination, so S is a permutation on all 8,192 states. + +Write H for PR1603's sufficient carry guard, specialized to this geometry. +The executable `carry_guard` is the direct specialization of that predicate. +Its all-size sufficiency and invariance remain predecessor results. + +## New guard and exact finite theorem + +Define + +```text +B_extra = {s: c=0, t=1, u=2, y odd} +H_plus = H union B_extra. +``` + +On this entire quotient, H_plus is exactly the largest subset on which +S=T that is invariant under T. It is also the largest S-invariant subset +of agreement. Its size is 2,432, while H has 2,368 states. B_extra consists +of exactly 64 states and is disjoint from H. The good fraction increases +from 37/128 to 19/64. No other geometry or asymptotic optimum is asserted. + +### Written proof of the added branch + +Take y odd, t=1, u=2, c=0, and put a=bit_3(y). The temporary digits are +(1,0), and the controls are (0,1). The first target rotation is zero. +The temporary load is + +```text +t_loaded = 1 + (1+2a) modulo 4 = 2+2a modulo 4. +``` + +The second target rotation is therefore -8 if a=0, and +8 if a=1. +It toggles bit 3 and preserves bit 0. The unload restores t=1 because +the selected bits of y_new XOR 8 are the original selected bits. Hence + +```text +P_2(y,1) = (y+8(2a-1) modulo 128, 1). +``` + +The next P_2 sees 1-a and reverses the displacement exactly, including +wraparound. Since c=0, these are precisely S's two calls and T is identity. +Thus S=T on B_extra. T fixes this branch, so it is invariant. + +The branch lies outside H: the inactive saturated low temporary digit and +odd low target produce carry d_1=1 into the active high digit. H excludes +that carry. At even y the same t,u,c triple is already in H, so dropping +the odd qualifier from the union changes no accepted state. + +Combining this branch with the credited invariance and sufficiency of H +proves the improvement in writing. Its maximality is the finite theorem below. + +### Finite completeness argument + +Let E={s:S(s)=T(s)}. For any involution T, its largest invariant subset +contained in E is E intersect T(E). This general observation is already in +PR1603 and is not a new theorem claimed here. Equivalently, retain exactly +the complete cycles of the permutation S that lie inside E. Every +S-invariant subset is a union of complete S cycles. On a retained cycle, +S=T, so that cycle has length one or two and is T-invariant. This proves +that this cycle algorithm computes the unique largest admissible core. + +The verifier builds S by ten literal rotations on full nine-bit targets. +It executes all 32,768 full-target states, including all four low-bit lifts +of every quotient state, and compares every output field to a separate +quotient implementation. Both S and T are checked to be permutations. +The cycle algorithm partitions all 8,192 quotient states. Its retained +bitmap equals the explicit H_plus predicate entry for entry. Every added +state is checked to have the displayed four field conditions, and the +entire explicit branch is present. This establishes finite maximality +without a conjectured extrapolation or a census of predecessor results. + +The generated receipt hashes the core bitmap in the order +`index=(((c*4+u)*4+t)*128+y)`, with the lowest index in the low bit of each +byte. The bitmap is not handwritten. Normal verification writes no files. + +## Current-address repair consequence + +Since S and T preserve H_plus and agree there, the correction T S^-1 fixes +H_plus and permutes its complement. The retained extract/sort/reinsert +algorithm therefore has exactly 5,760 quotient records to repair, rather +than 5,824 with H. The finite checker installs a distinct payload tag at +every state, applies S, constructs all current-address keys T(S^-1(q)), +sorts all exceptional records and verifies every final destination tag. +It also checks that a wrong key T(q) produces an incorrect complete map. + +With the predecessor notation V=MP, address width L and payload width P, +the declared repair bound stays + +```text +O(V + M L^3 + delta M L(P+L)). +``` + +For this complete rectangle, delta changes from 91/128 to 45/64. The +64-record reduction is an exact counting consequence, not a measured +runtime saving. Every one of the twelve compact swaps, ten rotations, +source accesses, back-field returns and highest-bit completion remains paid. +The new predicate adds a constant number of field comparisons to H. The +finite sort replay is a logical record permutation, not a physical tape +implementation or a supplier admission. + +## Limits + +Maximality is proved by exhaustion only for the stated n=2 geometry. The +written branch argument also concerns precisely those parameters. No +all-n carry automaton, production predicate change, complete compiler, +native interface, recursive stock, precision, physical routing, analytic +transfer, new kappa or selected-frontier change is supplied. Independent +human and formal proof-kernel review are unclaimed. diff --git a/research/compact-maximal-invariant-guard/README.md b/research/compact-maximal-invariant-guard/README.md new file mode 100644 index 0000000000..964c228158 --- /dev/null +++ b/research/compact-maximal-invariant-guard/README.md @@ -0,0 +1,138 @@ +# Maximal invariant two-digit compact-control guard + +This contribution was produced by Nick Petalas. Apache-2.0. +Claim type: finite optimal-guard certificate and scoped written repair proof. + +For the unchanged later-source compact word at +`n=2, K=3, G=1, rho=2`, the exact largest invariant agreement guard is + +```text +H_plus = H from PR1603 OR (c=0 AND t=1 AND u=2 AND y is odd). +``` + +Here y is the full seven-bit target quotient, t,u are the complete two-bit +compact fields, and c contains the two processed source bits. The entire +quotient has 8,192 states. All nine physical target bits, including the two +low spectator bits and every upper bit, are accounted for. + +| Same complete quotient | PR1603 carry guard H | Maximal guard H_plus | +|---|---:|---:| +| Accepted states | 2,368 | 2,432 | +| Good fraction | 37/128 | 19/64 | +| Exceptional repair records | 5,824 | 5,760 | + +The 64 added states form one exact cancellation branch. An inactive +saturated low temporary digit sends a carry into the active high digit. +The old guard excludes it. With zero processed source bits, the two actual +subcalls reverse each other's displacement on this branch. The intended +map is identity there. [PROOF.md](PROOF.md) gives this calculation, the +finite maximality argument and the retained repair bill. + +This answers one small multi-digit instance of Arham Tahir's PR1603 open +question. Aaron Wang's PR1823 counts raw agreement; woklerx's PR1856 reduces +that census with a full-modulus carry defect. Those results are credited +context. Their mathematical executables are neither imported nor replayed. +The general involution-core observation is also credited prior work. The +new result is the explicit maximal multi-digit guard and its strict +64-record reduction on this complete quotient. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/compact-maximal-invariant-guard/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/compact-maximal-invariant-guard/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/compact-maximal-invariant-guard +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/compact-maximal-invariant-guard --check-source-history +``` + +Substitute another CPython 3.12 executable elsewhere. Direct replay prints +`PASS_COMPACT_MAXIMAL_INVARIANT_GUARD` in generated JSON stdout. The receipt +binds every package file by SHA256 and includes the exact accepted-set bitmap +hash. No receipt is handwritten and normal replay writes no files. + +The bounded check executes all 32,768 full-target cases and compares every +field with a separate quotient implementation. It partitions the complete +raw permutation into cycles and retains exactly those wholly in agreement. +This algorithm, which does not use the explicit guard formula, agrees with +H_plus on all 8,192 states. Every extra state is classified, both invariances +are checked and all 8,192 distinct payload tags reach their intended output +after repairing precisely the 5,760 exceptional records. + +Controls reject agreement without invariance, removal of each of the three +extra-branch field conditions and incorrect current-address repair keys. +The new branch is required by a positive witness, the even-parity overlap +with H is retained, and seven invalid inputs fail in both Python modes. +The source note and PR1603 proof are authenticated live text inputs, without +executing predecessor code. The registered runner checks the remaining +historical catalogue and selected-record pins. + +Local CPython 3.12.15 on macOS 27.0.1 arm64 passes both direct commands +and the registered package replay. The direct checks took 0.105 and 0.104 +seconds, within their 60-second caps. These durations establish local +timeout headroom and are not a speedup claim. Normal and optimized receipts +agree byte for byte. In-memory compilation and whitespace checks pass. + +## Limits and relevance + +Maximality is finite and specific to the displayed geometry. The extra +branch has c=0. This does not establish an improvement on nonzero processed +source slices or on production parameter families. The wider all-n symbolic +agreement problem remains open. The card's changed scope to a written +descriptor interface result is explicit in TASK.json. + +The inherited complete repair bound retains +`O(V + M L^3 + delta M L(P+L))`; only this rectangle's exact delta changes +from 91/128 to 45/64. No runtime speedup is claimed. All twelve compact +swaps, ten rotations and the separate highest-bit completion remain paid. +The payload replay is a logical permutation. Physical tape execution, +compiler, native supply, ownership/stock, precision and analytic transfer +are unproved here. No selected cold replay, Lean, Docker, new kappa or +selected-frontier change is claimed. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +Can a symbolic multi-digit carry calculation characterize an invariant +enlargement that includes nonzero processed source slices? First use the +complete-map and full-target-modulus tests on one additional geometry, then +prove a bounded carry-state description. No extrapolation from this one +finite cancellation branch is justified. The state bound, physical guard +implementation and complete caller bill remain blockers. + +## Credit and provenance + +Arham Tahir / Arham-Tahir64, PR1603, supplies H, its all-n invariance proof +and the explicit multi-digit open question. Aaron Wang / navinor, PR1823, +supplies the raw-agreement census context. Woklerx / PR1856 supplies the +full-target-modulus warning and integer-lift context. Douglas Colkitt +supplies the unchanged compact word and exceptional-record repair contract. +Credit Hanson Sun / bbMisk, PR1247/1219; Sagar Thakrar / thakrarsagar, +PR1475; John-Michael Smith / jp3isme, PR763; martinxxx9 / PR1108; and the +retained compact-control lineage. Their source files and credit lines are +unchanged. No general literature-priority claim is made for elementary +permutation or involution facts. + +Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. +The selected source-binding baseline passed with selected PR6030 unchanged. +Live open PRs, recent account contributions, merged searches, main README +searches and Discussion claims were checked before reservation. The overlap +snapshot covered 387 open PRs, 6,322 Discussion records and all 8,917 tracked +README/TASK/ledger notes. Arbitrary diffs and unpublished work remain outside +that text coverage. Absence of a match is not a novelty certificate. + +Advance claim: +https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362365 + +## Verifier bounds + +All mathematical loops have fixed bounds from the 8,192-state quotient, +four low-bit lifts, two digits, four phases and a fixed control list. +Permutation traversal uses an explicit 8,192-step cap per cycle and visits +each state once. There is no recursion, subprocess, network operation, +runtime code generation or external mathematical implementation. +Functions fit within 60 physical lines. Explicit failures remain active +under optimized Python. Python dynamically allocates integer and collection +objects; fixed-size domains bound these allocations, rather than providing +a static-memory guarantee. The registered commands enable warnings as errors. diff --git a/research/compact-maximal-invariant-guard/SOURCES.json b/research/compact-maximal-invariant-guard/SOURCES.json new file mode 100644 index 0000000000..a983515b22 --- /dev/null +++ b/research/compact-maximal-invariant-guard/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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": "notes/compact-control-movement.tex", + "usage": "input", + "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357", + "sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6" + }, + { + "path": "research/compact-late-carry-guard/PROOF.md", + "usage": "input", + "git_blob": "89f39f3b557b2bb0c1c26d2d7d255121f6db8fb5", + "sha256": "1cc589e40f94fa64add255f81c381720ddef933c7cfa7d07ef6263c2cf1e8b85" + } + ] +} diff --git a/research/compact-maximal-invariant-guard/TASK.json b/research/compact-maximal-invariant-guard/TASK.json new file mode 100644 index 0000000000..cefd4c2f5b --- /dev/null +++ b/research/compact-maximal-invariant-guard/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact maximal invariant agreement guard and current-address repair on the complete n=2,K=3,G=1,rho=2 later-source compact quotient.", + "scope_change_reason": "Replace a proof-kernel campaign with one written descriptor interface proof and finite optimal-guard certificate answering PR1603's multi-digit open question. This is a scoped side result, not a selected-caller or all-size formalization.", + "bottleneck_link": "A strictly larger invariant complete-map agreement guard removes exceptional repair records while preserving the unchanged raw word and full repair contract. This finite geometry does not alter the binding supplier moment.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified strict guard enlargement; do not extend to further geometries or claim a production improvement.", + "outcome": "completed", + "evidence": "PROOF.md plus independent literal full-target execution, complete permutation-cycle maximality and exact tagged current-address repair in verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a symbolic multi-digit carry calculation produce an invariant enlargement including nonzero processed source slices?", + "why_it_matters": "The delivered strict enlargement is confined to zero processed source bits in one finite geometry.", + "first_step": "Keep the full target modulus, inspect one additional complete geometry, and derive a bounded carry-state predicate before any extrapolation.", + "blocked_by": "No all-n state bound, physical guard implementation or complete caller bill is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362365", + "source_pr": 1603, + "source_author": "Arham-Tahir64", + "related_context_prs": [ + 1823, + 1856 + ], + "scope_limits": "Finite optimality only. The general involution-core observation and predecessor sufficient guard are cited prior work, not new results or audit deliverables." + } +} diff --git a/research/compact-maximal-invariant-guard/VERIFY.json b/research/compact-maximal-invariant-guard/VERIFY.json new file mode 100644 index 0000000000..a8607943cc --- /dev/null +++ b/research/compact-maximal-invariant-guard/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "notes/compact-control-movement.tex", + "research/compact-late-carry-guard/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Full 32768-state literal target map, 8192-state maximal invariant guard and tagged repair, rejection controls and source pins." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete certificate and controls with optimization enabled." + } + ] +} diff --git a/research/compact-maximal-invariant-guard/verify.py b/research/compact-maximal-invariant-guard/verify.py new file mode 100644 index 0000000000..ece4e3ce7f --- /dev/null +++ b/research/compact-maximal-invariant-guard/verify.py @@ -0,0 +1,275 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact maximal invariant guard on one complete two-digit quotient.""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +Y = 128 +C = 4 +SIZE = Y * C * C * C +State = tuple[int, int, int, int] + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def checked_state(state: State) -> State: + need(isinstance(state, tuple) and len(state) == 4, "four-field state") + need(all(type(x) is int for x in state), "integer state fields") + need(0 <= state[0] < Y, "target quotient range") + need(all(0 <= x < C for x in state[1:]), "compact/source range") + return state + + +def mask(source: int) -> int: + return (source & 1) + 8 * ((source >> 1) & 1) + + +def pack(target: int) -> int: + return (target & 1) + 2 * ((target >> 3) & 1) + + +def early(target: int, temporary: int, controls: int) -> tuple[int, int]: + target = (target + 2 * ((controls & 1) * (temporary & 1) + + 8 * ((controls >> 1) & 1) * ((temporary >> 1) & 1))) % Y + temporary = (temporary + pack(target)) % C + target = (target + (controls & 1) * (1 - 2 * (temporary & 1)) + + 8 * ((controls >> 1) & 1) + * (1 - 2 * ((temporary >> 1) & 1))) % Y + temporary = (temporary - pack(target ^ mask(controls))) % C + return target, temporary + + +def raw(state: State) -> State: + target, temporary, control, source = state + target, temporary = early(target, temporary, control) + target, temporary = early(target, temporary, (control + source) % C) + return target, temporary, control, source + + +def ideal(state: State) -> State: + target, temporary, control, source = state + return target ^ mask(source), temporary, control, source + + +def carry_guard(state: State) -> bool: + """PR1603's H, specialized to n=2, K=3, G=1, rho=2.""" + target, temporary, control, source = state + carry = 0 + for i in range(2): + ti = (temporary >> i) & 1 + ui = (control >> i) & 1 + ci = (source >> i) & 1 + active = ui | ci + parity = (target >> (3 * i)) & 1 + wide = (target >> (3 * i + 1)) & 3 + if active and (carry or ti == 1): + return False + if i == 0 and (ui + ci >= 2 or wide + active * ti >= 4): + return False + carry = (ti + parity + carry) // 2 + return True + + +def safe(state: State) -> bool: + target, temporary, control, source = checked_state(state) + extra = source == 0 and temporary == 1 and control == 2 and target % 2 == 1 + return carry_guard(state) or extra + + +def literal_full(state: State, low: int) -> tuple[int, int, int, int]: + """Ten full-field rotations; uses division, full 9-bit targets and digits.""" + target, temporary, control, source = state + target = 4 * target + low + loaded = (control + source) % 4 + for current_control in (control, loaded): + z = [current_control % 2, current_control // 2] + for phase in range(4): + if phase in (0, 2): + digits = [temporary % 2, temporary // 2] + offset = 0 + for i, place in enumerate((4, 32)): + value = 2 * digits[i] if phase == 0 else 1 - 2 * digits[i] + offset += z[i] * value * place + target = (target + offset) % 512 + else: + amount = 0 + for i, place in enumerate((4, 32)): + bit = (target // place) % 2 + if phase == 3: + bit = (bit + z[i]) % 2 + amount += bit * (i + 1) + temporary = (temporary + (amount if phase == 1 else -amount)) % 4 + restored_control = (loaded - source) % 4 + return target, temporary, restored_control, source + + +def index(state: State) -> int: + target, temporary, control, source = state + return (((source * C + control) * C + temporary) * Y + target) + + +def decode(number: int) -> State: + number, target = divmod(number, Y) + number, temporary = divmod(number, C) + source, control = divmod(number, C) + return target, temporary, control, source + + +def literal_permutation() -> tuple[list[int], list[int], int]: + actual = [0] * SIZE + wanted = [0] * SIZE + full_cases = 0 + for number in range(SIZE): + state = decode(number) + need(index(state) == number, "index round trip") + target_state = ideal(state) + wanted[number] = index(target_state) + for low in range(4): + result = literal_full(state, low) + quotient, retained_low = divmod(result[0], 4) + need(retained_low == low, "low target spectator") + normalized = (quotient, *result[1:]) + need(normalized == raw(state), "full/lifted execution mismatch") + if low == 0: + actual[number] = index(normalized) + full_cases += 1 + need(sorted(actual) == list(range(SIZE)), "raw permutation") + need(sorted(wanted) == list(range(SIZE)), "ideal permutation") + return actual, wanted, full_cases + + +def invariant_cycles(actual: list[int], wanted: list[int]) -> list[bool]: + """Keep exactly the complete raw-permutation cycles contained in agreement.""" + visited = [False] * SIZE + core = [False] * SIZE + for start in range(SIZE): + if visited[start]: + continue + cycle = [] + current = start + for _ in range(SIZE): + if visited[current]: + break + cycle.append(current) + visited[current] = True + current = actual[current] + need(current == start, "permutation cycle closure") + if all(actual[v] == wanted[v] for v in cycle): + for v in cycle: + core[v] = True + need(all(visited), "complete permutation partition") + return core + + +def core_check(actual: list[int], wanted: list[int], core: list[bool]) -> dict: + old = [carry_guard(decode(i)) for i in range(SIZE)] + formula = [safe(decode(i)) for i in range(SIZE)] + need(formula == core, "explicit guard is not the maximal invariant core") + need(all(not old[i] or core[i] for i in range(SIZE)), "old guard inclusion") + need(all(core[i] == core[wanted[i]] for i in range(SIZE)), "T invariance") + need(all(core[i] == core[actual[i]] for i in range(SIZE)), "S invariance") + extra = [i for i in range(SIZE) if core[i] and not old[i]] + need((sum(old), sum(core), len(extra)) == (2368, 2432, 64), "guard counts") + need(all(decode(i)[1:] == (1, 2, 0) and decode(i)[0] % 2 for i in extra), + "complete extra-branch classification") + bitmap = bytes(sum(core[8 * j + k] << k for k in range(8)) + for j in range(SIZE // 8)) + return {"old_good": sum(old), "maximal_good": sum(core), "extra": len(extra), + "core_bitmap_sha256": sha256(bitmap).hexdigest(), + "extra_witness": list(decode(extra[0]))} + + +def repair_check(actual: list[int], wanted: list[int], core: list[bool]) -> dict: + inverse = [0] * SIZE + payload = [0] * SIZE + for original, current in enumerate(actual): + inverse[current] = original + payload[current] = original + holes = [current for current in range(SIZE) if not core[current]] + records = sorted((wanted[inverse[current]], payload[current]) for current in holes) + need([key for key, _ in records] == holes, "repair destinations are exact holes") + for key, tag in records: + payload[key] = tag + need(all(payload[wanted[i]] == i for i in range(SIZE)), "full payload endpoint") + wrong = payload[:] + for current in holes: + wrong[wanted[current]] = inverse[current] + wrong_count = sum(wrong[wanted[i]] != i for i in range(SIZE)) + need(wrong_count > 0, "wrong current-key repair control") + need(len(holes) == 5760, "exact repair-record count") + return {"records": len(holes), "old_records": SIZE - 2368, + "endpoint_tags": SIZE, "wrong_key_misplacements": wrong_count} + + +def controls(actual: list[int], wanted: list[int], core: list[bool]) -> dict: + agreement = [actual[i] == wanted[i] for i in range(SIZE)] + need(any(agreement[i] and not agreement[wanted[i]] for i in range(SIZE)), + "agreement-only predicate unexpectedly invariant") + witness = next(i for i in range(SIZE) if agreement[i] and not core[i]) + need(safe((1, 1, 2, 0)) and not carry_guard((1, 1, 2, 0)), + "missing new branch control") + need(safe((0, 1, 2, 0)) and carry_guard((0, 1, 2, 0)), + "even parity is already covered by the old guard") + altered = 0 + for field in (1, 2, 3): + found = False + for state in product(range(Y), range(C), range(C), range(C)): + extra = state[0] % 2 == 1 + for j, value in ((1, 1), (2, 2), (3, 0)): + if j != field: + extra = extra and state[j] == value + if extra and not core[index(state)]: + found = True + break + need(found, "deleted extra-branch condition was not rejected") + altered += 1 + invalid = [(-1, 0, 0, 0), (Y, 0, 0, 0), (0, -1, 0, 0), + (0, 0, C, 0), (0, 0, 0, C), (False, 0, 0, 0), (0, 0, 0)] + for state in invalid: + try: + safe(state) + except ValueError: + continue + raise ValueError("invalid state accepted") + return {"agreement_only_witness": list(decode(witness)), + "extra_condition_mutations": altered, "invalid_inputs": len(invalid), + "new_branch_required": True, "even_branch_already_in_old_guard": True} + + +def source_pins() -> int: + entries = json.loads((HERE / "SOURCES.json").read_text())["files"] + live = [entry for entry in entries if entry["usage"] == "input"] + for entry in live: + data = (ROOT / entry["path"]).read_bytes() + need(sha256(data).hexdigest() == entry["sha256"], "source drift: " + entry["path"]) + return len(live) + + +def main() -> None: + pins = source_pins() + actual, wanted, full_cases = literal_permutation() + core = invariant_cycles(actual, wanted) + result = {"status": "PASS_COMPACT_MAXIMAL_INVARIANT_GUARD", + "claim_type": "finite optimal-guard certificate and scoped repair proof", + "geometry": {"n": 2, "K": 3, "G": 1, "rho": 2}, + "quotient_states": SIZE, "full_target_cases": full_cases, + "guard": core_check(actual, wanted, core), + "repair": repair_check(actual, wanted, core), + "controls": controls(actual, wanted, core), "live_source_pins": pins} + result["package_sha256"] = { + p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()