diff --git a/research/two-facet-downset-inertia/README.md b/research/two-facet-downset-inertia/README.md new file mode 100644 index 0000000000..1a447b6081 --- /dev/null +++ b/research/two-facet-downset-inertia/README.md @@ -0,0 +1,222 @@ +# Sharp integer inertia certificates for two-facet downsets + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped mathematical proof with exact finite corroboration.** +Every finite downset with at most two maximal members and at least one +nonempty member admits a nonsingular, symmetric, nonnegative integer matrix +supported on disjoint pairs, with exactly as many positive eigenvalues as +its largest star. Thus its optimal number of nonnegative eigenvalues is +exactly that star size. + +This proves the two-facet case of Ellis, Filmus and Friedgut's +[Conjecture I, section 4](https://arxiv.org/html/2609.28404v1#S4), recorded as +C070 in David Ganz's [atlas, PR2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849). +The contribution is the explicit construction and all-size congruence below. +No global literature priority is claimed. The general downset conjecture, +physical suppliers and a new kappa remain outside scope. + +## Statement and explicit entries + +Write the downset as + +```text +D = 2^(C union A) union 2^(C union B), +C, A, B pairwise disjoint; |A|=a >= b=|B|; |C|=c. +``` + +For two distinct maximal members, take their intersection as C and their +differences as A,B, so a,b >= 1. A single maximal member is included by +taking B empty. Unused ground elements do not affect the construction. +Fix an injection iota:B -> A. + +First set c=0 and list all subsets S of A, followed by all **nonempty** +subsets T of B. Define the base matrix K as follows: + +- Within either of these two lists, K(U,V)=1 if U and V are disjoint, + and zero otherwise. +- Between S subset A and nonempty T subset B, put + K(S,T)=K(T,S)=h(|S intersect iota(T)|), where + h(0)=1 and h(k)=2^k-1 for k>=1. + +These cross pairs are always disjoint in the actual ground set. The +injection only defines weights; it does not identify ground elements. +For general c, put + +```text +M((R,U),(R',V)) = 1[R intersect R' is empty] K(U,V). +``` + +Here R,R' subset C and U,V are base labels. In particular M is symmetric, +integral and nonnegative, and M(X,Y)=0 whenever X intersect Y is nonempty. +The empty-set diagonal is 1, as permitted by the conjecture. + +Let N=2^c(2^a+2^b-1), and let s be the largest star size. Then + +```text +s = 2^(a-1) if c=0, +s = N/2 if c>=1. +inertia(M) = (s, N-s, 0). +det(M) = (-1)^(N-s) 3^e, +e = 2^c(2^(b-1)-1) if b>=1, and e=0 if b=0. +``` + +The c=0 case has a>=1 by the nonempty-member hypothesis. The case +a=b=0,c>=1 is the ordinary full cube and is included separately below. + +## All-size proof + +For the Boolean cube on r elements, let Z_r(S,T)=1[T subset S], +J_r(T,T)=(-1)^|T|, and D_r(S,T)=1[S intersect T is empty]. +Order subsets by any linear extension of inclusion. Then Z_r is unit +lower triangular, and + +```text +D_r = Z_r J_r Z_r^T, +``` + +since its (S,T) entry is the sum of (-1)^|U| over U subset S intersect T. +For r>=1 exactly half the diagonal entries of J_r have each sign. + +Assume b>=1, so a>=1. Let Z' and J' be the restrictions of Z_b and J_b +to nonempty subsets. Set u(T)=(-1)^(|T|+1). Summing over nonempty +subsets proves Z'u=1. Deleting the empty row and column from D_b gives + +```text +D_b[nonempty,nonempty] = Z'(J' + uu^T)Z'^T. +``` + +Let e0 denote the empty-subset coordinate in the A cube. Define a +2^a by (2^b-1) matrix E whose column T is the coordinate vector at +iota(T) if T has positive even cardinality, and zero if T has odd +cardinality. Distinct nonzero columns are distinct coordinate vectors, +all at positive diagonal entries of J_a, and none at e0. Therefore + +```text +J_a E = E, e0^T E = 0, +E^T E = diag(1[|T| is positive and even]). +``` + +Put H=e0 u^T + 2E. The cross block of K is Z_a H Z'^T: its entry +is 1 plus twice the number of nonempty even subsets of +iota^(-1)(S) intersect T. For intersection size k, that number is +zero if k=0 and 2^(k-1)-1 otherwise. This is exactly the prescribed h(k). +Consequently congruence by diag(Z_a,Z') reduces K to + +```text + [ J_a H ] + [ H^T J' + uu^T ]. +``` + +Eliminate the invertible upper-left block J_a. Its Schur complement is + +```text +J' + uu^T - H^T J_a H = J' - 4E^T E. +``` + +This is diagonal: -3 on nonempty even subsets of B, and -1 on odd +subsets. It is negative definite. Sylvester's law of inertia gives +exactly 2^(a-1) positive eigenvalues of K, with every other eigenvalue +negative. All congruence factors used have determinant one. There are +2^(b-1)-1 entries -3, so |det K|=3^(2^(b-1)-1). + +If b=0, K=D_a; its zeta congruence gives the same inertia conclusion +when a>=1 and determinant of absolute value one. If a=b=0, K=[1]. + +For c>=1 the full matrix is D_c tensor K. The symmetric invertible +matrix D_c has equally many positive and negative eigenvalues, so +tensoring with any invertible symmetric K gives N/2 eigenvalues of +each sign. Also |det D_c|=1, so |det M|=|det K|^(2^c). +This proves all stated determinant and inertia formulas, including +the a=b=0 case. + +For c=0, a coordinate in A lies in 2^(a-1) members; one in B lies +in 2^(b-1) members. For c>=1, a coordinate in C lies in N/2 members. +The other star sizes are 2^c 2^(a-1) and 2^c 2^(b-1) when those +coordinates exist, each at most N/2. Thus the positive count equals s. + +Finally, any symmetric disjointness-supported matrix has a zero +principal block on a star of size s. Its quadratic form vanishes on +that s-dimensional coordinate subspace. If it had fewer than s +nonnegative eigenvalues, its negative eigenspace would intersect that +subspace nontrivially, contradicting negative definiteness there. +This proves optimality among all real supported symmetric matrices. + +## First fixture and verification + +For a=b=2,c=0 there are seven sets and s=2. The ordinary disjointness +matrix has inertia (3,4,0). The construction changes just the weight +between the two full exclusive facets from 1 to 3, producing inertia +(2,5,0) and determinant -3. Weight 2 instead gives inertia (2,4,1), +so its zero eigenvalue still leaves three nonnegative eigenvalues. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/two-facet-downset-inertia/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/two-facet-downset-inertia/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-facet-downset-inertia +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-facet-downset-inertia --check-source-history +``` + +Any CPython 3.12 can replace the local interpreter path. The standalone +standard-library verifier needs only its package; it does not load atlas +code or fetch the paper. The source pin identifies the originating +question, not a mathematical dependency needed by the proof. + +The verifier enumerates all **49 triples** a>=b>=0,c>=0 with +1<=a+b+c<=6, including degenerate single-cube presentations. It constructs +each matrix literally, checks every support entry, counts each star, +checks the integer zeta congruence, and computes inertia and determinant +by independent exact rational symmetric elimination, with 1-by-1 and +2-by-2 pivots. This covers matrices through order 64. These finite checks +corroborate the all-size proof; they do not replace it. + +Eight control checks include the unweighted failure, the first positive +fixture, the singular weight-two modification, zero-diagonal pivots, +zero eigenvalue counting and invalid inputs. Explicit exceptions keep +checks active under optimization. JSON output records each case and +SHA-256 of the package files; no receipt is hand-written or stored. + +The bounded loops use at most six ground coordinates and matrix order +64. Each function fits within 60 lines. Python allocates rational +numbers and lists dynamically; this managed-runtime deviation is bounded +by these fixed domains and the fixed five-file package inventory. +Warnings are errors in both registered modes. No additional static +analyzer is assumed. No recursive calls or background processes occur. + +## Scope, overlap and credit + +David Ganz's PR2849 supplies atlas C070 and its research direction. +Ellis, Filmus and Friedgut formulate the spectral conjecture; their +general intersecting-family and projection-packing theorems are not +reproved or needed here. The Boolean zeta identity and Sylvester +congruence are classical tools. This package adds a constructive +two-facet specialization, including the weights, inertia and determinant. +The atlas's credit lines and all predecessor files remain unchanged. + +Canonical base is ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority +revision 7. TASK.json marks the formal-interface-lemma card as changed: +this is an algebraic side result on an explicit open certificate +question, with no claimed implication for the selected supplier. +Live open/account PRs, active Discussions, recent account handoffs, +local reservations, merged searches and main README searches showed +no matching two-facet inertia contribution. The cached overlap search +covered 311 open PRs and 4,483 Discussion records; only 187 of 7,091 +HEAD notes were materialized. Targeted main-tree searches supplement +that sparse coverage. Unpublished work and global literature priority +remain outside the novelty claim. + +Independent human and formal proof-kernel review are unclaimed. +No Lean, Docker, selected cold replay, physical caller, compiler, +precision, storage or complete multiplication theorem is certified. + +## Open next questions + +Can a disjointness-supported integer matrix achieve the largest-star +inertia for downsets with three maximal sets? Start with three pairwise +disjoint two-element facets and write the zeta-basis cross blocks. +This tests whether positive directions can be coupled without increasing +the final positive count. The blocker is simultaneous control of the +three Schur interactions; the two-facet negative complement alone does +not settle it. The full spectral conjecture remains separate. diff --git a/research/two-facet-downset-inertia/SOURCES.json b/research/two-facet-downset-inertia/SOURCES.json new file mode 100644 index 0000000000..273bbdfee5 --- /dev/null +++ b/research/two-facet-downset-inertia/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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/pure-math-atlas-400/volumes/03-combinatorics.md", + "usage": "input", + "git_blob": "63ecb48e31e8f15c06c6c9813cfb8092870605d8", + "sha256": "b80927e2a5d68e22d3c0687a9ec8267a11b5a1c4a68b06c3f80b8164c2c66b2c" + } + ] +} diff --git a/research/two-facet-downset-inertia/TASK.json b/research/two-facet-downset-inertia/TASK.json new file mode 100644 index 0000000000..fcd2a05c7e --- /dev/null +++ b/research/two-facet-downset-inertia/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct a sharp nonnegative integer inertia certificate for every downset with at most two maximal members.", + "scope_change_reason": "The selected formal-interface card concerns caller bindings. This is an algebraic side result on the explicitly open atlas C070 certificate problem, without a supplier or formalization claim.", + "bottleneck_link": "Algebraic side result: supplies exact supported-matrix certificates for one infinite family; no selected supplier cost or kappa implication is asserted.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified two-facet construction and package it; leave three-facet extensions open.", + "outcome": "completed", + "evidence": "README all-size zeta/Schur congruence; verify.py checks all 49 parameter triples through six ground coordinates, exact inertia and determinant, and eight controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the sharp integer inertia construction extend to three maximal sets?", + "why_it_matters": "Would enlarge the proved subclass of Conjecture I beyond the two-facet case.", + "first_step": "Write the zeta-basis cross blocks for three pairwise disjoint two-element facets.", + "blocked_by": "Three interacting Schur blocks need simultaneous control; the two-facet complement does not provide it." + } + ] +} diff --git a/research/two-facet-downset-inertia/VERIFY.json b/research/two-facet-downset-inertia/VERIFY.json new file mode 100644 index 0000000000..3ef82e9d99 --- /dev/null +++ b/research/two-facet-downset-inertia/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/pure-math-atlas-400/volumes/03-combinatorics.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal supported matrices, integer zeta congruence, exact rational inertia/determinants, largest stars, and eight controls on all 49 triples through six coordinates." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact checks with optimization enabled; explicit exception guards remain active." + } + ] +} diff --git a/research/two-facet-downset-inertia/verify.py b/research/two-facet-downset-inertia/verify.py new file mode 100644 index 0000000000..cc0b6f9a8e --- /dev/null +++ b/research/two-facet-downset-inertia/verify.py @@ -0,0 +1,222 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the two-facet inertia construction. + +Produced by Nick Petalas. Apache-2.0. +Standard library only. No files are written. +""" + +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path + + +MAX_GROUND = 6 +MAX_ORDER = 64 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(left, right): + require(left and right and len(left[0]) == len(right), "matrix shape") + columns = tuple(zip(*right)) + return [[sum(x * y for x, y in zip(row, col)) for col in columns] + for row in left] + + +def transpose(matrix): + return [list(row) for row in zip(*matrix)] + + +def zeta(width, nonempty=False): + require(0 <= width <= MAX_GROUND, "zeta width") + labels = range(int(nonempty), 1 << width) + return [[int(t & s == t) for t in labels] for s in labels] + + +def inertia(matrix): + """Symmetric rational elimination, including zero-diagonal 2x2 pivots.""" + size = len(matrix) + require(1 <= size <= MAX_ORDER, "inertia size") + require(all(len(row) == size for row in matrix), "square matrix") + require(matrix == transpose(matrix), "symmetric matrix") + work = [list(map(Fraction, row)) for row in matrix] + positive = negative = zero = 0 + determinant = Fraction(1) + for _ in range(size): + if not work: + break + pivot = next((i for i in range(len(work)) if work[i][i]), None) + if pivot is not None: + work[0], work[pivot] = work[pivot], work[0] + for row in work: + row[0], row[pivot] = row[pivot], row[0] + value = work[0][0] + positive += value > 0 + negative += value < 0 + determinant *= value + work = [[work[i][j] - work[i][0] * work[0][j] / value + for j in range(1, len(work))] + for i in range(1, len(work))] + continue + pair = next(((i, j) for i in range(len(work)) + for j in range(i + 1, len(work)) if work[i][j]), None) + if pair is None: + zero += len(work) + determinant = Fraction(0) + break + order = list(pair) + [i for i in range(len(work)) if i not in pair] + work = [[work[i][j] for j in order] for i in order] + value = work[0][1] + positive += 1 + negative += 1 + determinant *= -value * value + work = [[work[i][j] - (work[i][0] * work[1][j] + + work[i][1] * work[0][j]) / value + for j in range(2, len(work))] + for i in range(2, len(work))] + require(positive + negative + zero == size, "inertia exhausted") + return (positive, negative, zero), determinant + + +def base_matrix(a, b, weighted=True): + require(0 <= b <= a and a + b <= MAX_GROUND, "exclusive sizes") + labels = [(s, 0) for s in range(1 << a)] + labels += [(0, t) for t in range(1, 1 << b)] + split = 1 << a + matrix = [] + for i, (s, t) in enumerate(labels): + row = [] + for j, (u, v) in enumerate(labels): + if i < split and j < split: + value = int(s & u == 0) + elif i >= split and j >= split: + value = int(t & v == 0) + else: + count = ((s & v) if i < split else (u & t)).bit_count() + value = max(1, (1 << count) - 1) if weighted else 1 + row.append(value) + matrix.append(row) + return labels, matrix + + +def certificate(a, b, c): + require(0 <= c and 1 <= a + b + c <= MAX_GROUND, "ground size") + base_labels, base = base_matrix(a, b) + labels = [core | (s << c) | (t << (c + a)) + for core in range(1 << c) for s, t in base_labels] + size = len(base) + matrix = [[int(x & y == 0) * base[i][j] + for y in range(1 << c) for j in range(size)] + for x in range(1 << c) for i in range(size)] + return labels, matrix + + +def check_congruence(a, b): + """Check the claimed zeta factorization by literal integer products.""" + _, matrix = base_matrix(a, b) + first = 1 << a + size = len(matrix) + left = [[0] * size for _ in range(size)] + for i, row in enumerate(zeta(a)): + left[i][:first] = row + if b: + for i, row in enumerate(zeta(b, nonempty=True), start=first): + left[i][first:] = row + normal = [[0] * size for _ in range(size)] + for s in range(first): + normal[s][s] = (-1) ** s.bit_count() + for t in range(1, 1 << b): + j = first + t - 1 + normal[j][j] = (-1) ** t.bit_count() + for u in range(1, 1 << b): + normal[j][first + u - 1] += ( + (-1) ** (t.bit_count() + u.bit_count())) + normal[0][j] = normal[j][0] = (-1) ** (t.bit_count() + 1) + if t.bit_count() % 2 == 0: + normal[t][j] = normal[j][t] = 2 + require(multiply(multiply(left, normal), transpose(left)) == matrix, + "zeta congruence") + + +def expected(a, b, c, size): + positive = size // 2 if c else 1 << (a - 1) + exponent = ((1 << (b - 1)) - 1) * (1 << c) if b else 0 + negative = size - positive + return (positive, negative, 0), (-1) ** negative * 3 ** exponent + + +def check_case(a, b, c): + labels, matrix = certificate(a, b, c) + size = len(matrix) + require(len(set(labels)) == size, "distinct set labels") + require(all(value >= 0 and isinstance(value, int) + for row in matrix for value in row), "nonnegative integers") + for i, s in enumerate(labels): + for j, t in enumerate(labels): + require(not s & t or matrix[i][j] == 0, "disjointness support") + star = max(sum(bool(s & (1 << i)) for s in labels) + for i in range(a + b + c)) + wanted, determinant = expected(a, b, c, size) + require(star == wanted[0], "largest star") + actual, direct_det = inertia(matrix) + require(actual == wanted and direct_det == determinant, "exact inertia") + return {"a": a, "b": b, "c": c, "order": size, + "inertia": actual, "determinant": int(direct_det), "star": star} + + +def rejection_controls(): + _, plain = base_matrix(2, 2, weighted=False) + controls = {"unweighted": inertia(plain)[0] == (3, 4, 0)} + _, good = base_matrix(2, 2) + controls["first_fixture"] = inertia(good) == ((2, 5, 0), Fraction(-3)) + good[3][6] = good[6][3] = 2 + controls["coupling_threshold"] = inertia(good)[0] == (2, 4, 1) + controls["off_diagonal_pivot"] = ( + inertia([[0, 1], [1, 0]]) == ((1, 1, 0), Fraction(-1))) + controls["zero_multiplicity"] = ( + inertia([[0, 0], [0, 0]]) == ((0, 0, 2), Fraction(0))) + for name, value in (("asymmetric", [[1, 2], [0, 1]]), + ("nonsquare", [[1], [2]])): + controls[name] = False + try: + inertia(value) + except ValueError: + controls[name] = True + controls["invalid_sizes"] = False + try: + certificate(1, 2, 0) + except ValueError: + controls["invalid_sizes"] = True + require(all(controls.values()), "control failure") + return controls + + +def main(): + rows = [] + for ground in range(1, MAX_GROUND + 1): + for c in range(ground + 1): + for b in range((ground - c) // 2 + 1): + a = ground - c - b + if b > a: + continue + check_congruence(a, b) + rows.append(check_case(a, b, c)) + controls = rejection_controls() + package = Path(__file__).resolve().parent + files = [package / name for name in ( + "README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")] + result = {"status": "PASS_TWO_FACET_DOWNSET_INERTIA", + "claim_type": "scoped proof with finite exact corroboration", + "cases": rows, "case_count": len(rows), "controls": controls, + "control_count": len(controls), + "source_sha256": {p.name: sha256(p.read_bytes()).hexdigest() + for p in files}} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()