diff --git a/research/block4-coordinate-face-tariff/README.md b/research/block4-coordinate-face-tariff/README.md new file mode 100644 index 0000000000..fb07b795e4 --- /dev/null +++ b/research/block4-coordinate-face-tariff/README.md @@ -0,0 +1,193 @@ +# A sharp block-four coordinate-face obstruction + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with an exact finite certificate. No new κ.** At block size +four, let a paid call in direction `v != 0` apply +`C_v = (1+i)I/2 + (1-i)X_v/2`, where `X_v e_x = e_(x+v)` on +`V = C^16`. Write `wt(v)` for its Hamming weight in the specified coordinates. +A program delivering `K y_l` for each of `W` independent arrays, where +`K = C_e3 C_e2 C_e1 C_e0`, satisfies + +``` +sum over paid calls of wt(v) >= 4 W. +``` + +The program may use arbitrary complex register mixing, zero scratch, copies, +erasures, arbitrary diagonal address operators, translations and coordinate +permutations for free. Every address operator acts identically on all digit +columns. Inverse calls have the same weight. Correctness at digit width five +already suffices for the theorem. Thus every all-width unit in this game obeys +it. For coordinate calls alone the exact minimum is `4 W`, attained by applying +four coordinate calls independently to each array. + +The certificate also has a sharp limitation. Its exact call contribution is +`112 wt(v)`, while its target contribution is 448. A weight-four direction +has contribution 448. Consequently this certificate, used alone through the +kept-subspace inequality, gives only `s >= W` when every nonzero direction has +unit price. It does not exclude the unrestricted block-four open shapes. + +## What is new, and what is inherited + +Jacob Alan Sussman's [PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628), +at `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`, supplies the kept-subspace method, +the block-three face certificate, and the relevant small-unit questions. See +[PROOF.md sections 1 and 5](https://github.com/CrocSwap/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/PROOF.md). +The method originates in eumemic's #288 certificate method and Swapnil Jain's +P1/P2 as credited by Sussman. These are cited predecessors; their executables +and reported ranks are not replayed here. + +The new result is the block-four fifth-exterior-power certificate, its exact +compression Gram identity, the direction-weight ranks and the resulting +weighted lower bound with its sharp failure for unit-priced diagonal calls. +Sussman's block-four commutative-slice result allows every direction but has +no phase letters. This result allows arbitrary diagonal phases and restricts +the cost conclusion by direction weight. Neither statement is presented as +containing the other's entire game. General XOR-linear address maps are absent +from this theorem. They need not preserve its certificate. + +This is a changed `complex-rank-shape-decoder` scope. It gives a decision about +a small complex-unit search alphabet, rather than a paid supplier profile. +The card's historical first command was attempted and failed with +`KeyError: 'complex_profile'` against the changed selected-record schema. +The current baseline command was also attempted and stopped at an omitted +sparse-checkout input, `research/fresh-helper-thinned/PROOF.md`. Neither run +is claimed as scientific verification or repaired by this package. The selected +record remains κ = 60403/20000000. The proof below is independent of that ledger. + +## Proof + +### The face space + +Work inside the alternating subspace `exterior^5(V)` of digit width five. +It has dimension `choose(16,5) = 4368`. For `j in {0,1,2,3}` and `b in {0,1}`, +let `V_(j,b)` be the span of addresses with `x_j=b`, and set + +``` +N_(j,b) = exterior^5(V_(j,b)), +N = direct sum over j,b of N_(j,b). +``` + +Two distinct nonopposite coordinate faces intersect in only four addresses. +A five-element subset therefore belongs to at most one face. This proves that +the displayed sum is direct and that `dim N = 8 choose(8,5) = 448`. +For each coordinate `j`, the two faces together have dimension 112. +Translations and coordinate permutations permute these summands. Every diagonal +operator preserves each summand. Therefore every allowed free address operator +preserves `N`. Register mixing sends `N^R` into itself even when singular. + +### Target demand and exact Gram identity + +Let `H` be the normalized Walsh matrix on four bits, +`H_(x,y) = (-1)^(x dot y)/4`, and let `U = exterior^5(H)`. +Write `P` for orthogonal projection onto `N` and `A = P U |_N`. + +If a row face fixes bit `j` and a column face fixes a different bit `k`, +the corresponding eight-by-eight submatrix of `H` has rank four. Its fifth +minors vanish. Thus `A` is block diagonal in the four coordinates. + +For equal row and column coordinates, the two-by-two face block is + +``` +2^(-5/2) [[1,1],[1,-1]] tensor exterior^5(H_3), +``` + +where `H_3` is the normalized eight-by-eight Walsh matrix. It is unitary. +The sign in the bottom-right entry is negative because the exterior degree +is odd. Squaring this block gives `A* A = (1/16) I_448`. Since `U` is unitary, +the leakage operator `L = (I-P) U |_N` satisfies + +``` +L* L = I - A* A = (15/16) I_448. +``` + +In particular the target leakage has rank 448, and all its singular values +are `sqrt(15)/4`. + +The same conclusions hold for `exterior^5(K)`. Indeed, with +`D_(x,x)=(-i)^wt(x)`, the exact identity is `K = -D H D`. +Both diagonal exterior factors preserve `N` and its orthogonal complement, +and are unitary. They conjugate the compression Gram by a unitary factor. +The scalar sign does not affect it. + +### Call cap and its exactness + +A call in direction `v` preserves every face space with `v_j=0`. +These give `112 (4-wt(v))` independent vectors of `N` whose image remains in +`N`. Its leakage rank is therefore at most `112 wt(v)`. + +The verifier constructs every column of `exterior^5(2 C_v)` on `N`, with exact +Gaussian integer coefficients, for each of the fifteen nonzero directions. +It checks the full column Gram `1024 I_448`, the claimed kept columns, and a +modulo-65537 leakage rank of `112 wt(v)`. The embedding sends `i` to 256, +whose square is -1 modulo the checked prime. A nonzero minor in this residue +field is a nonzero Gaussian-integer minor, so this is a characteristic-zero +lower bound. Together with the preceding upper bound it proves equality. +The ranks by direction weight are respectively 112, 224, 336 and 448. +For an invertible operator `g`, `dim(N+gN)-dim N` equals the same quantity for +`g^-1`, so inverse calls obey the same statement. + +### From one array to a program + +For completeness, the kept-subspace argument is as follows. If the state map +is `M: V_5^W -> V_5^R`, with `V_5=V tensor ... tensor V` at width five, track + +``` +Phi(M) = dim(M(N^W) + N^R) - dim(N^R). +``` + +It starts at zero. Free address operations and mixing preserve `N^R`, so they +cannot increase this quotient dimension. Applying an invertible call `g` to +one register increases it by at most `dim(N+gN)-dim N`. This follows by pulling +back `N^R` through that call and adjoining the resulting extra dimensions. +At delivery, projection to the `W` output registers gives independent target +leakages, so `Phi >= 448 W`. Thus +`448 W <= 112 sum wt(v)`, as asserted. Extra scratch, intermediate copies and +erasures do not alter the argument. + +## Exact replay + +From the repository root, use CPython 3.12 with its standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/block4-coordinate-face-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/block4-coordinate-face-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/block4-coordinate-face-tariff --check-source-history +``` + +The registered commands also run optimized Python. All scientific checks use +explicit exceptions, so optimization does not remove them. The verifier checks +all 200,704 compression minors by fraction-free integer determinants. Their +integer compression matrix `B=1024 A` satisfies `B^T B=65536 I` exactly. +It then certifies all fifteen call ranks and rejects nine controls, including +an altered compression entry and the false cap 112 for diagonal directions. +It prints `PASS_BLOCK4_COORDINATE_FACE_TARIFF` with the results and SHA256 hashes +of all five package files. Optional `--receipt PATH` creates that generated +receipt outside the checkout and refuses to overwrite an existing file. +No hand-written receipt or predecessor replay is used. + +The written program theorem uses the displayed finite identities. It has not +been checked by a formal proof kernel or an independent human. No physical +supplier, compilation tariff, rounding analysis or multiplication theorem is +claimed. The exact finite rank computation is specific to block four. + +The verifier uses bounded loops over at most 4368 subsets, 448 source columns, +32 wedge choices per column and fifteen directions. Integer determinant +matrices are at most five-by-five. The sparse elimination has at most 448 +pivots. Managed Python allocation and callbacks for the nine immediate negative +controls are explicit deviations from literal allocation-free and no-indirect- +call versions of the Power of Ten rules. No recursion, generated code or +external mathematical dependencies are used. + +## Open next questions + +- Can a different kept space give a demand-to-cap ratio above 7/2 while allowing + every direction at unit price and arbitrary diagonal phases? The present + exact cap 448 rules out that improvement from this space. Start by identifying + a space that treats diagonal directions differently; general address-map + keptness is a separate obligation. +- Does an exterior coordinate-face construction give a useful weighted law at + other block sizes? Start with the face-compression blocks and their Gram + identity. The present finite rank claim covers only block four. + +See the structured questions and evidence in [TASK.json](TASK.json). diff --git a/research/block4-coordinate-face-tariff/SOURCES.json b/research/block4-coordinate-face-tariff/SOURCES.json new file mode 100644 index 0000000000..80f74a60e2 --- /dev/null +++ b/research/block4-coordinate-face-tariff/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/block4-coordinate-face-tariff/TASK.json b/research/block4-coordinate-face-tariff/TASK.json new file mode 100644 index 0000000000..6c28533260 --- /dev/null +++ b/research/block4-coordinate-face-tariff/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Block-four fifth-exterior-power coordinate-face certificate: demand 448, exact directional call rank 112 wt(v), and the sharp weighted program lower bound.", + "scope_change_reason": "Small-unit obstruction following Jacob Alan Sussman PR4628, rather than a supplier-profile climb. Arbitrary diagonal phases are free; general address maps are excluded. Unit-priced diagonal directions destroy a useful uniform cap for this certificate.", + "bottleneck_link": "A scoped side result for new small complex-unit geometries. It excludes savings using only coordinate calls and arbitrary diagonal phases, and identifies why the obvious face lift cannot exclude unrestricted-direction units.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified original block-four certificate and package it; leave other blocks and changed kept spaces open.", + "outcome": "completed", + "evidence": "Self-contained written proof; exact 200704 target compression minors, scalar Gram identity, all fifteen exact call ranks via analytic upper bounds and modular lower bounds, and nine rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can another kept space exceed demand/cap 7/2 with every nonzero direction at unit price and arbitrary diagonal phases?", + "why_it_matters": "This would address the block-four two-in-seven search, which this certificate cannot exclude.", + "first_step": "Choose a kept space whose cap for diagonal directions stays below its target demand; test a weight-four call first.", + "blocked_by": "No candidate space or general address-map keptness theorem is supplied." + }, + { + "question": "Does the coordinate-face compression give a useful weighted law at other block sizes?", + "why_it_matters": "It could separate axis-only architectures from those using diagonal directions.", + "first_step": "Derive the coordinate-face compression blocks and their exact Gram matrix at a new block size.", + "blocked_by": "The certified ranks here are specific to block four." + } + ], + "upstream_checkpoint": { + "commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "checked_at": "2026-10-22T21:48:26Z" + }, + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133370" +} diff --git a/research/block4-coordinate-face-tariff/VERIFY.json b/research/block4-coordinate-face-tariff/VERIFY.json new file mode 100644 index 0000000000..716389357f --- /dev/null +++ b/research/block4-coordinate-face-tariff/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 integer target compression and Gram; all 15 Gaussian call leakage ranks with proved upper bounds; nine controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same certificate with optimization enabled; explicit checks remain active." + } + ] +} diff --git a/research/block4-coordinate-face-tariff/verify.py b/research/block4-coordinate-face-tariff/verify.py new file mode 100644 index 0000000000..4f7961de84 --- /dev/null +++ b/research/block4-coordinate-face-tariff/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +"""Exact block-four face certificate, with no external mathematical inputs.""" + +import argparse +import hashlib +import json +from itertools import combinations +from pathlib import Path +import sys + +PRIME = 65537 +ROOT_I = 256 +DEGREE = 5 +ADDRESSES = 16 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def face_of(subset): + faces = [(bit, (subset[0] >> bit) & 1) for bit in range(4) + if all(((x >> bit) & 1) == ((subset[0] >> bit) & 1) + for x in subset)] + require(len(faces) <= 1, "five distinct points cannot share two faces") + return faces[0] if faces else None + + +def face_basis(): + basis = tuple(combinations(range(ADDRESSES), DEGREE)) + inside = tuple(s for s in basis if face_of(s) is not None) + require(len(basis) == 4368 and len(inside) == 448, "basis dimensions") + for bit in range(4): + for value in range(2): + require(sum(face_of(s) == (bit, value) for s in inside) == 56, + "face dimension") + return basis, inside + + +def determinant(matrix): + """Fraction-free integer elimination, on matrices of size at most five.""" + size = len(matrix) + require(1 <= size <= DEGREE and all(len(r) == size for r in matrix), + "determinant dimensions") + a = [list(row) for row in matrix] + sign, previous = 1, 1 + for col in range(size - 1): + pivot = next((r for r in range(col, size) if a[r][col]), None) + if pivot is None: + return 0 + if pivot != col: + a[col], a[pivot] = a[pivot], a[col] + sign = -sign + entry = a[col][col] + for row in range(col + 1, size): + for j in range(col + 1, size): + value = a[row][j] * entry - a[row][col] * a[col][j] + require(value % previous == 0, "Bareiss exact division") + a[row][j] = value // previous + a[row][col] = 0 + previous = entry + return sign * a[-1][-1] + + +def target_compression(inside): + """All 448-by-448 compression entries, each a fifth Walsh minor.""" + walsh = [[1 if (x & y).bit_count() % 2 == 0 else -1 + for y in range(ADDRESSES)] for x in range(ADDRESSES)] + for x in range(ADDRESSES): + for y in range(ADDRESSES): + require(sum(walsh[z][x] * walsh[z][y] + for z in range(ADDRESSES)) == (16 if x == y else 0), + "Walsh unitarity") + rows = [] + for target in inside: + row = {} + for j, source in enumerate(inside): + value = determinant([[walsh[x][y] for y in source] for x in target]) + if value: + row[j] = value + require(face_of(target)[0] == face_of(source)[0], + "cross-face compression must vanish") + rows.append(row) + return rows + + +def gram(rows, size, gaussian=False): + result = [{} for _ in range(size)] + for row in rows: + for j, left in row.items(): + for k, right in row.items(): + if gaussian: + value = (left[0] * right[0] + left[1] * right[1], + left[0] * right[1] - left[1] * right[0]) + old = result[j].get(k, (0, 0)) + result[j][k] = (old[0] + value[0], old[1] + value[1]) + else: + result[j][k] = result[j].get(k, 0) + left * right + zero = (0, 0) if gaussian else 0 + return [{k: v for k, v in row.items() if v != zero} for row in result] + + +def check_scalar_gram(rows, size, scalar, gaussian=False): + actual = gram(rows, size, gaussian) + for j, row in enumerate(actual): + require(row == {j: (scalar, 0) if gaussian else scalar}, + "compression Gram identity") + + +def gaussian_product(left, right): + return (left[0] * right[0] - left[1] * right[1], + left[0] * right[1] + left[1] * right[0]) + + +def call_columns(inside, direction): + """Expand wedge^5(2 C_v) using each of the 32 choices per column.""" + require(1 <= direction < ADDRESSES, "nonzero direction") + coefficients = [] + for mask in range(1 << DEGREE): + value = (1, 0) + for bit in range(DEGREE): + value = gaussian_product(value, (1, -1) if mask >> bit & 1 else (1, 1)) + coefficients.append(value) + columns = [] + for source in inside: + column = {} + for mask, value in enumerate(coefficients): + points = tuple(x ^ (direction if mask >> j & 1 else 0) + for j, x in enumerate(source)) + if len(set(points)) < DEGREE: + continue + inversions = sum(points[j] > points[k] for j in range(DEGREE) + for k in range(j + 1, DEGREE)) + sign = -1 if inversions % 2 else 1 + target = tuple(sorted(points)) + old = column.get(target, (0, 0)) + column[target] = (old[0] + sign * value[0], old[1] + sign * value[1]) + columns.append({s: v for s, v in column.items() if v != (0, 0)}) + return columns + + +def columns_to_rows(columns): + rows = {} + for j, column in enumerate(columns): + for target, value in column.items(): + rows.setdefault(target, {})[j] = value + return rows + + +def modular_rank(columns, row_ids): + require(PRIME == 65537 and ROOT_I * ROOT_I % PRIME == PRIME - 1, + "Gaussian residue embedding") + pivots = {} + for column in columns: + current = {row_ids[s]: (a + ROOT_I * b) % PRIME + for s, (a, b) in column.items() if (a + ROOT_I * b) % PRIME} + for _ in range(len(columns) + 1): + if not current: + break + lead = min(current) + if lead not in pivots: + inverse = pow(current[lead], -1, PRIME) + pivots[lead] = {r: v * inverse % PRIME for r, v in current.items()} + break + factor = current[lead] + for row, value in pivots[lead].items(): + updated = (current.get(row, 0) - factor * value) % PRIME + if updated: + current[row] = updated + else: + current.pop(row, None) + else: + raise ValueError("elimination exceeded the column bound") + return len(pivots) + + +def check_call(inside, outside_ids, direction): + columns = call_columns(inside, direction) + rows = columns_to_rows(columns) + check_scalar_gram(rows.values(), len(inside), 1024, gaussian=True) + leakage = [{s: value for s, value in c.items() if s in outside_ids} + for c in columns] + unaffected = [j for j, s in enumerate(inside) + if not (direction >> face_of(s)[0]) & 1] + require(all(not leakage[j] for j in unaffected), "unaffected faces are kept") + upper = len(inside) - len(unaffected) + require(upper == 112 * direction.bit_count(), "direction-weight upper bound") + lower = modular_rank(leakage, outside_ids) + require(lower == upper, "sharp call rank") + return lower + + +def expect_rejection(function): + try: + function() + except ValueError: + return + raise ValueError("negative control accepted") + + +def controls(compression, ranks): + controls_run = 0 + for wrong in (0, 65535, 65537, 1048576): + expect_rejection(lambda: check_scalar_gram(compression, 448, wrong)) + controls_run += 1 + corrupted = [dict(row) for row in compression] + key = next(iter(corrupted[0])) + corrupted[0][key] += 1 + expect_rejection(lambda: check_scalar_gram(corrupted, 448, 65536)) + controls_run += 1 + expect_rejection(lambda: call_columns((), 0)) + controls_run += 1 + for direction in (3, 7, 15): + expect_rejection(lambda: require(ranks[str(direction)] <= 112, + "diagonal call is not an axis call")) + controls_run += 1 + return controls_run + + +def scientific_result(): + require(sys.version_info >= (3, 12), "Python 3.12 or later required") + require(all(PRIME % d for d in range(2, 257)), "residue modulus is prime") + basis, inside = face_basis() + inside_set = set(inside) + outside_ids = {s: j for j, s in enumerate(s for s in basis if s not in inside_set)} + compression = target_compression(inside) + check_scalar_gram(compression, 448, 65536) + ranks = {str(v): check_call(inside, outside_ids, v) for v in range(1, 16)} + require(max(ranks.values()) == 448, "no useful uniform call cap here") + return {"claim_type": "scoped proof with exact finite certificate", + "dimension": len(basis), "face_dimension": len(inside), + "target_compression_scale": 1024, "compression_gram": 65536, + "leakage_gram": "15/16 I_448", "target_demand": 448, + "call_ranks": ranks, "controls": controls(compression, ranks), + "target_minors_checked": len(inside) ** 2} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + result = scientific_result() + package = Path(__file__).resolve().parent + result["source_sha256"] = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("verify.py", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json")} + payload = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.receipt is not None: + require(not args.receipt.resolve().is_relative_to(package.parent.parent), + "receipt must be outside the checkout") + with args.receipt.open("x", encoding="utf-8") as stream: + require(stream.write(payload) == len(payload), "complete receipt write") + print("PASS_BLOCK4_COORDINATE_FACE_TARIFF " + json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()