diff --git a/research/two-grid-selector-obstruction/PROOF.md b/research/two-grid-selector-obstruction/PROOF.md new file mode 100644 index 0000000000..9da1e8201b --- /dev/null +++ b/research/two-grid-selector-obstruction/PROOF.md @@ -0,0 +1,95 @@ +# Every two-grid selector has the same translation obstruction + +This contribution was produced by Nick Petalas. New work is Apache-2.0. +The elementary set-translation argument below is the new scoped extension of +woklerx's [PR #1845](https://github.com/CrocSwap/integer-mult-bounds/pull/1845). +Its leaf increments and admission conditions are cited premises. + +## Model and theorem + +Fix integers a,b and an integer h >= 2. A target value q in Z is measured in +fine-grid units. Fine precision admits every q. Coarse precision admits only +q in hZ. At fixed values of the source and all other visible state, the two +executions add a and b respectively. They leave the other visible state +identical. The selector may use any subset S of hZ, choosing coarse precisely +at q in S. No periodicity, regularity or computability is assumed. + +Write delta = a-b. The visible output is + + F(q) = q+b+delta*1_S(q). + +Then: + +1. F is injective on Z if and only if S+delta is contained in S. +2. F is surjective onto Z if and only if S is contained in S+delta. +3. F is bijective if and only if S+delta=S. +4. A nonempty admission-respecting injective selector exists if and only + if h divides delta. When divisibility holds, S=hZ attains bijectivity. + +These statements concern the unbounded lattice, without clipping, saturation +or a quotient identifying different integer inputs. + +## Proof + +Each branch is a translation, hence injective within its own branch. A +cross-branch collision must have q in S and r outside S, with + + q+a = r+b, hence r=q+delta. + +It exists exactly when some q in S has q+delta outside S. This proves 1 and +also supplies an explicit collision witness for every failed inclusion. + +After subtracting b, the image is exactly + + (S+delta) union (Z minus S). + +This covers Z exactly when S is contained in S+delta, proving 2. Combining +1 and 2 proves 3. In fact every output has at most two preimages, one per +branch; no assumption about finite or infinite S enters the argument. + +For 4, suppose S is nonempty and F is injective. Choose q in S. Both q and +q+delta belong to S by 1 and therefore to hZ. Their difference delta is +divisible by h. Conversely, if h divides delta, take S=hZ. Translation by +delta preserves hZ, so 3 gives bijectivity. Since h>=2, both precision +branches occur in this attaining policy. This includes delta=0. + +## Why injectivity and bijectivity must be separated + +For h=2, a=2, b=0, let S be the nonnegative even integers. The output sends +each nonnegative even input two places forward and fixes every other input. +It is injective on Z and misses exactly 0. Thus replacing the inclusion in +1 by equality would falsely exclude a nonperiodic injective selector. +Reversing the ray, S the nonpositive even integers, creates the collision +F(0)=F(2)=2. Both examples satisfy coarse admission. + +## Conditional application to the actual PR628 leaf + +Use the fixed source-one, zero-imaginary-target slice specified in PR1845's +README at `b0a7acdd39a6943218d312ae93e8bbc65ab8c56c`. Its retained parameters +are outside factor 1/4, scale 1, phase [1], beta=1/2, direction +1 and no +scratch. Its stated premises are: + +- Target inputs are q/32 for every integer q. +- Precision four is admitted only when q is even and adds -10/32. +- Precision five is admitted for every q and adds -11/32. +- Both executions restore the source and leave the imaginary coordinate zero. + +These predecessor statements are assumed here, not replayed or independently +validated. In fine-grid units they give h=2, a=-10, b=-11 and delta=1. +The divisibility condition fails. Therefore an injective selector on this +whole slice must choose precision five at every q. If it chooses coarse at +even q, the adjacent input q+1 is ineligible for coarse and is forced fine: + + F_leaf(q/32) = (q-10)/32 = ((q+1)-11)/32 = F_leaf((q+1)/32). + +This witness does not require knowing the selector elsewhere. It covers +arbitrary nonperiodic, source-conditioned policies after fixing this source +slice, provided they have only these two precisions and no additional visible +branch state. It strengthens PR1845's single coarsest-compatible-policy +counterexample to every selector making any coarse choice on this slice. + +It does not require a policy to make a coarse choice on this slice. A policy +may use fine precision here and save elsewhere. Three or more precisions, +changed increments, additional retained state, a different source, restricted +reachable inputs or non-restored auxiliary outputs require separate analysis. +No multiplication theorem, physical implementation or kappa improvement follows. diff --git a/research/two-grid-selector-obstruction/README.md b/research/two-grid-selector-obstruction/README.md new file mode 100644 index 0000000000..648b88e96d --- /dev/null +++ b/research/two-grid-selector-obstruction/README.md @@ -0,0 +1,130 @@ +# A sharp obstruction for every two-grid precision selector + +For a two-grid update with coarse-input admission q in hZ, an injective +selector can use coarse precision anywhere **if and only if h divides the +difference of the two increments**. This holds for arbitrary selector sets, +including nonperiodic and noncomputable choices. It is a scoped mathematical +proof with exact finite corroboration, not a new kappa or supplier. + +Let coarse and fine increments be a and b in fine-grid units, delta=a-b, +and S contained in hZ be the inputs selected for coarse execution. Then + +```text +F(q) = q+b+delta*1_S(q) +injective iff S+delta is contained in S +surjective iff S is contained in S+delta +bijective iff S+delta=S +``` + +If h does not divide delta, every coarse choice q has an explicit collision +partner q+delta, which is ineligible for coarse. If h divides delta, choosing +coarse on hZ and fine elsewhere is a bijection. [PROOF.md](PROOF.md) gives +the complete argument and a nonperiodic injective, nonsurjective example. + +## What this adds + +woklerx's [PR #1845](https://github.com/CrocSwap/integer-mult-bounds/pull/1845) +proves that one coarsest-compatible policy loses information on a named PR628 +leaf. It also classifies periodic residue-translation policies. Its open +question asks whether useful target-adaptive precision can retain injectivity +without a branch transcript. + +Here **every** selector using only those two precisions is excluded from +making any coarse choice on the same whole source-one, zero-imaginary-target +slice. The cited coarse and fine increments are -10/32 and -11/32, with +coarse admission q even for target q/32. Thus h=2 and delta=1, and the +collision partner is always q+1. The new proof assumes the predecessor's +admission, increment and restoration statements. It neither imports nor +replays the predecessor implementation. + +The scope change from `uniform-transfer-audit` is explicit in [TASK.json](TASK.json). +An adaptive precision compiler needs injectivity before its saved precision +can enter a complete caller. This theorem resolves one narrow obstruction; +it does not construct or price that compiler. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19227538) +records the same scope. + +## Evidence and reproduction + +The standard-library verifier independently enumerates literal output images +and compares their multiplicities with the new set-inclusion criterion. +Periodic cases use every admission-respecting subset for h=2 through 8, +period h*k with k=1 through 6, and delta=-2h through 2h. Finite-support +cases use every subset of hZ intersected with [-6,6] for h=2 through 6, +and delta=-6 through 6. Their integer images include every possible +cross-branch collision partner, so these cases do not assume wraparound. +An additional application check constructs explicit witnesses using the +cited increments; it is not a leaf replay. + +Normal and optimized local checks agree on 18,522 periodic parameter-policy +fixtures and 543,774 literal residue images, including 13,440 admission +obstructions. They also agree on 2,392 finite-support fixtures and 46,552 +literal integer images, plus 1,025 cited-premise collision witnesses and ten +controls. Each direct command took about 0.07 seconds locally; this timing +only records that the registered timeout is ample, not a speedup claim. + +Semantic controls distinguish inclusion from equality and its reverse, +show attainment for divisible increments and the need for admission, +and cover zero and negative differences. Invalid replay parameters reject. +Every run emits its computed counts and a receipt bound to SHA256 hashes +of all six package files. No receipt is handwritten or stored in the package. + +From the repository root, using CPython 3.12.15 locally: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-grid-selector-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/two-grid-selector-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-grid-selector-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-grid-selector-obstruction --check-source-history +``` + +Another CPython 3.12 interpreter may replace that absolute path. The expected +scientific marker is `PASS_TWO_GRID_SELECTOR_OBSTRUCTION`. Both registered +commands have a 60-second timeout and write no files. Exact provenance pins +are in [SOURCES.json](SOURCES.json); there are no external executable inputs. + +## Limits and verification discipline + +The universal theorem rests on the written proof. Finite enumeration +corroborates it. The leaf application is conditional on PR1845's stated +source slice and does not independently validate it. A policy may choose +fine precision everywhere on that slice and use coarse elsewhere. +Larger precision menus, different increments, stored branch information, +different sources, restricted reachable domains and auxiliary outputs can +escape this two-branch model. Clipping and saturation are not covered. +No selected frontier, physical native operation, complete invoice or +multiplication theorem is changed. Independent human and formal proof-kernel +review, the selected cold replay, Lean and Docker are unrun. + +The code has no recursion, subprocesses, dynamic evaluation or persistent +state. Loops have fixed bounds in the listed domains. One periodic case +stores at most 48 image residues; one finite-support case evaluates at most +25 integers. File hashing is bounded to six files of at most 1 MiB each. +Functions stay below 60 lines. Explicit checks remain enabled under -O. +Python allocates exact integers and collections during this bounded offline +replay, a documented memory-allocation deviation from allocation-free execution. +Warning-strict normal and optimized checks are registered. + +## Open next questions + +- Can three or more actual admitted precisions avoid the forced collision? + First obtain the additional increment and admission lattice and test disjoint + translated branch images. Their physical selection/restoration bill remains + unknown. +- Does a useful actual caller reach a restricted target set excluding every + forced partner? First pin one call site and prove its source-conditioned + reachable set. Reachability and its maintenance costs are the blockers. + +These are structured in [TASK.json](TASK.json). This package reserves neither +follow-up and starts no further construction campaign. + +## Credit + +This contribution was produced by Nick Petalas. Credit woklerx for PR1845's +question, admitted increments, residue-translation theorem and PR1451's prior +mixed-precision inverse boundary; Chafik Boukhalfa for the PR628 leaf; +Gareth Davidson for its retained fixed-grid caller and proof; and Ali Romman's +PR621 and the retained kernel lineage. Elementary translation and partition +facts are background mathematics. The new claim is the arbitrary-selector +classification with admission and its conditional all-policy exclusion on +the named slice. New work is Apache-2.0. diff --git a/research/two-grid-selector-obstruction/SOURCES.json b/research/two-grid-selector-obstruction/SOURCES.json new file mode 100644 index 0000000000..f50f49ab79 --- /dev/null +++ b/research/two-grid-selector-obstruction/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/adaptive-grid-injectivity-audit/README.md", + "usage": "provenance", + "git_blob": "7c5cb440951dcbe64306062740b07294e14c2ac5", + "sha256": "b614cb7806a2b9aba367657733725a4d76bb03eda171179fbf15a57167b7d2a0" + } + ], + "references": [ + { + "pr": 1845, + "author": "woklerx", + "head": "b0a7acdd39a6943218d312ae93e8bbc65ab8c56c", + "usage": "Question source and cited leaf-increment/admission premises; not an executable dependency or a result reverified here." + }, + { + "pr": 628, + "author": "Chafik Boukhalfa", + "usage": "Underlying rounded leaf, through PR1845." + }, + { + "pr": 1451, + "author": "woklerx", + "usage": "Prior mixed-precision inverse boundary, through PR1845." + } + ] +} diff --git a/research/two-grid-selector-obstruction/TASK.json b/research/two-grid-selector-obstruction/TASK.json new file mode 100644 index 0000000000..63dce409de --- /dev/null +++ b/research/two-grid-selector-obstruction/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify every admission-respecting two-grid precision selector, including nonperiodic selectors, and apply the new obstruction conditionally to the cited source-one PR628 slice of PR1845.", + "scope_change_reason": "The precision/restoration card is narrowed to the explicit open question of PR1845. This is a new all-selector theorem, not a replay or audit of its coarsest-compatible policy.", + "bottleneck_link": "An adaptive precision compiler must preserve visible-input injectivity before claiming precision savings. The theorem excludes all coarse use on a named two-grid source slice and gives the exact changed-increment condition for escape.", + "budget_minutes": 60, + "stop_rule": "Ship the all-selector theorem and its first cited-premise application; do not extend to larger menus or a physical compiler.", + "outcome": "negative-result", + "evidence": "Written arbitrary-subset proof plus exhaustive bounded periodic and finite-support map checks. Exact counts are emitted by verify.py. Predecessor increments are assumed, not independently replayed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can three or more actual admitted precisions form an injective policy that uses a coarser grid on the source-one slice?", + "why_it_matters": "A larger menu could avoid the forced fine-branch collision of the two-grid theorem.", + "first_step": "Obtain the additional source-conditioned increment and admission lattice, then solve the disjoint translated-branch image conditions.", + "blocked_by": "No additional leaf increment or physical selector and restoration invoice is supplied here." + }, + { + "question": "Is a useful actual caller restricted to a reachable target set that excludes each forced collision partner?", + "why_it_matters": "The obstruction assumes the whole fine lattice on a fixed source slice.", + "first_step": "Pin one actual call site and prove its exact source-conditioned reachable target set.", + "blocked_by": "Reachability and the cost of maintaining such a restriction have not been established." + } + ], + "claim_type": "scoped mathematical proof with exact finite corroboration", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19227538", + "orientation": { + "selected_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY after materializing omitted immutable paths", + "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "remote_overlap": "377 open PRs and 5599 Discussion records with complete pagination, refreshed 2026-10-27T21:04:21Z and 21:05:27Z; main README keyword searches and live precommit checks supplement sparse local coverage. Arbitrary diffs and unpublished work remain outside coverage." + } +} diff --git a/research/two-grid-selector-obstruction/VERIFY.json b/research/two-grid-selector-obstruction/VERIFY.json new file mode 100644 index 0000000000..72129797b5 --- /dev/null +++ b/research/two-grid-selector-obstruction/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact literal periodic images, nonperiodic finite-support images, arbitrary-selector criterion, cited-premise collision witnesses and semantic/invalid-input controls; generated SHA256 receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact literal periodic images, nonperiodic finite-support images, arbitrary-selector criterion, cited-premise collision witnesses and semantic/invalid-input controls; generated SHA256 receipt." + } + ] +} diff --git a/research/two-grid-selector-obstruction/verify.py b/research/two-grid-selector-obstruction/verify.py new file mode 100644 index 0000000000..3a3dbf3b95 --- /dev/null +++ b/research/two-grid-selector-obstruction/verify.py @@ -0,0 +1,169 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the arbitrary two-grid selector theorem. + +Produced by Nick Petalas. Apache-2.0. +No predecessor implementation is imported or replayed. +""" + +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def periodic_case(h, copies, delta, mask): + """Compare literal output multiplicities with the selector criterion.""" + require(2 <= h <= 8 and 1 <= copies <= 6, "period outside replay bounds") + require(-2 * h <= delta <= 2 * h, "increment outside replay bounds") + require(0 <= mask < (1 << copies), "invalid policy bit mask") + period = h * copies + selected = {h * j for j in range(copies) if mask & (1 << j)} + offset = h - 3 + images = Counter( + (q + offset + (delta if q in selected else 0)) % period + for q in range(period) + ) + injective = max(images.values()) == 1 + closed = all((q + delta) % period in selected for q in selected) + require(injective == closed, "literal image disagrees with inclusion") + require(injective == (len(images) == period), "periodic image is not a permutation") + if selected and delta % h: + require(not injective, "admission obstruction failed") + q = min(selected) + partner = q + delta + require(partner % h != 0, "collision partner unexpectedly admits coarse input") + require(q + offset + delta == partner + offset, "wrong collision witness") + return injective, period, bool(selected and delta % h) + + +def check_periodic_policies(): + counts = Counter() + for h in range(2, 9): + for copies in range(1, 7): + for delta in range(-2 * h, 2 * h + 1): + for mask in range(1 << copies): + injective, period, obstructed = periodic_case(h, copies, delta, mask) + counts["parameter_policy_fixtures"] += 1 + counts["literal_residue_images"] += period + counts["injective_fixtures"] += injective + counts["admission_obstructions"] += obstructed + return dict(counts) + + +def finite_support_case(h, delta, selected): + """An exact test on Z when S is finite, not a cyclic wraparound test.""" + require(2 <= h <= 6 and -6 <= delta <= 6, "finite support parameters out of bounds") + require(all(-6 <= q <= 6 and q % h == 0 for q in selected), "invalid coarse support") + closed = all(q + delta in selected for q in selected) + # Every cross-branch collision involves q in S and q+delta. Both are here. + radius = 6 + abs(delta) + inputs = range(-radius, radius + 1) + images = [q + (delta if q in selected else 0) for q in inputs] + image_set = set(images) + injective = len(image_set) == len(images) + require(injective == closed, "nonperiodic image disagrees with inclusion") + # Every y outside S has the fine preimage y. Only outputs in S need checking. + surjective = all(q in image_set for q in selected) + backwards_closed = all(q - delta in selected for q in selected) + require(surjective == backwards_closed, "literal image disagrees with surjectivity") + if selected and delta: + require(not injective, "a nonempty finite set cannot be translation-closed") + return len(images), injective + + +def check_finite_supports(): + counts = Counter() + for h in range(2, 7): + eligible = tuple(q for q in range(-6, 7) if q % h == 0) + for size in range(len(eligible) + 1): + for subset in combinations(eligible, size): + for delta in range(-6, 7): + images, injective = finite_support_case(h, delta, frozenset(subset)) + counts["finite_support_fixtures"] += 1 + counts["literal_integer_images"] += images + counts["injective_fixtures"] += injective + return dict(counts) + + +def check_cited_premise_application(): + """Use PR1845's stated increments as premises, without rechecking them.""" + coarse, fine, h = -10, -11, 2 + delta = coarse - fine + require(delta % h != 0, "cited application does not meet the obstruction") + count = 0 + for q in range(-1024, 1025, h): + partner = q + delta + require(q % h == 0 and partner % h != 0, "wrong admission classes") + require(q + coarse == partner + fine, "cited-premise collision failed") + count += 1 + return {"cited_premise_collision_witnesses": count, "coarse": coarse, + "fine": fine, "refinement": h, "delta": delta} + + +def check_controls(): + """Distinguish injectivity, surjectivity, admission and shift orientation.""" + checks = [] + # A legal infinite ray is injective but misses zero. It is not periodic. + values = [q + (2 if q % 2 == 0 and q >= 0 else 0) for q in range(-64, 65)] + require(len(set(values)) == len(values) and 0 not in values, "ray control failed") + checks.append("nonperiodic_injective_nonsurjective") + # Reversing inclusion gives a collision at 0 and 2. + values = [q + (2 if q % 2 == 0 and q <= 0 else 0) for q in range(3)] + require(values[0] == values[2], "orientation control failed") + checks.append("reversed_inclusion_rejected") + # Divisible increment difference permits a nonempty, admission-safe policy. + values = {(q + (2 if q % 2 == 0 else 0)) % 12 for q in range(12)} + require(values == set(range(12)), "divisible-difference positive control failed") + checks.append("divisible_difference_attainment") + # Without coarse admission, S=Z is a translation even for odd delta. + require(len({q + 1 for q in range(12)}) == 12, "admission-free control failed") + checks.append("admission_is_essential") + # Zero increment difference permits any selector, including finite S. + require(finite_support_case(2, 0, frozenset({0}))[1], "zero difference control failed") + checks.append("zero_difference") + require(not periodic_case(2, 2, -1, 1)[0], "negative difference must also obstruct") + checks.append("negative_difference") + for args in ((1, 1, 0, 0), (2, 7, 0, 0), (2, 1, 5, 0), (2, 1, 0, 2)): + try: + periodic_case(*args) + except ValueError: + checks.append("invalid_parameters_" + str(len(checks))) + else: + raise ValueError("invalid replay parameter accepted") + return checks + + +def file_hashes(): + 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(not path.is_symlink() and path.is_file(), "missing or aliased package file") + require(path.stat().st_size <= 1048576, "package file exceeds replay size bound") + hashes[name] = sha256(path.read_bytes()).hexdigest() + return hashes + + +def main(): + result = { + "status": "PASS_TWO_GRID_SELECTOR_OBSTRUCTION", + "claim_type": "scoped written proof with exact finite corroboration", + "periodic": check_periodic_policies(), + "finite_support": check_finite_supports(), + "cited_premise_application": check_cited_premise_application(), + "controls": check_controls(), + "files_sha256": file_hashes(), + "new_kappa": False, + } + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()