diff --git a/research/p104-metric-energy/PROOF.md b/research/p104-metric-energy/PROOF.md new file mode 100644 index 0000000000..24fb252a14 --- /dev/null +++ b/research/p104-metric-energy/PROOF.md @@ -0,0 +1,148 @@ +# Sharp common-metric orthogonality energy on P104 + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Statement and normalization + +Let R be the 120 E8 root lines represented by unit vectors in R^8. Choose +one sign on each line. The quantities below are independent of these signs. +Let F and G be any two disjoint orthonormal frames contained in R, each with +eight lines, and put P = R \ (F union G). Thus P has 104 lines. + +For a real symmetric 8 by 8 matrix A, write + + A0 = A - tr(A) I/8, + E_P(A) = sum_{unordered {u,v} subset P, u perpendicular v} (u^T A v)^2, + D_F(A0) = sum_{u in F} (u^T A0 u)^2, + X_FG(A0) = sum_{u in F, v in G, u perpendicular v} (u^T A0 v)^2. + +All norms below are Frobenius norms. The new quantitative identity is + + E_P(A) = 37 ||A0||^2 + (17/2) [D_F(A0) + D_G(A0)] + X_FG(A0). (1) + +Consequently E_P(A) >= 37 ||A0||^2 for every such P. The constant 37 is +sharp uniformly over this family. Section 4 gives an equality example and an +invertible rational common deformation attaining it arbitrarily near identity. + +The claim is a scoped proof using exact finite E8 premises, with a finite +equality certificate. It is not a statement about independent motions of the +120 lines, arbitrary masked fitting matrices, or a complete supplier. + +## 1. Exact finite E8 premises + +The verifier constructs one integer vector r per line. Its squared norm is 8. +There are 56 vectors 2(e_i +/- e_j), i < j, with the first nonzero coordinate +positive, and 64 vectors (1,s_1,...,s_7), with s_i in {1,-1} and an even +number of minus signs. Set u=r/sqrt(8). + +Two finite identities are checked directly, without a predecessor executable: + + sum_{v in R, v perpendicular u} v v^T = 9(I-u u^T) (2) + E_R(A) = 54 [||A||^2 - tr(A)^2/8] = 54 ||A0||^2. (3) + +For (2), every one of the 120 stars has 63 lines. In integer coordinates the +checked identity is sum s s^T = 72 I - 9 r r^T, with all 64 entries checked +for every r. This proves (2) exactly. + +For (3), use the 36 independent entries a of symmetric A, with eight diagonal +entries followed by the 28 upper off-diagonal entries. For an orthogonal pair +r,s, the coefficient vector c satisfies c.a = r^T A s. The verifier sums +H = sum c c^T over all 3,780 unordered orthogonal pairs. It checks all 1,296 +entries of + + H = 3456 W - 432 t t^T, + W = diag(1 repeated 8 times, 2 repeated 28 times), + t = (1 repeated 8 times, 0 repeated 28 times). + +Since a^T W a = ||A||^2 and t.a = tr(A), division by 64 gives (3). +This coefficient identity proves (3) for all real symmetric A, not only +sampled matrices. No floating eigenvalue computation is a premise. + +## 2. Removing one frame + +Let L_F(A) be the energy of all orthogonal pairs of R having at least one +endpoint in F. Summing (2) over u in F gives + + sum_{u in F} sum_{v perpendicular u} (u^T A v)^2 + = 9 [||A||^2 - sum_{u in F}(u^T A u)^2]. + +Pairs internal to F occur twice in this sum and once in L_F. Because F is +an orthonormal basis and A is symmetric, their energy is + + sum_{unordered u,v in F} (u^T A v)^2 + = (1/2) [||A||^2 - sum_{u in F}(u^T A u)^2]. + +Therefore, for every frame F in R, + + L_F(A) = (17/2) [||A||^2 - sum_{u in F}(u^T A u)^2]. (4) + +This argument quantifies over arbitrary frames. It does not infer a universal +frame statement from the two frames used for the equality example. + +## 3. Removing two frames and the deformation consequence + +Disjointness gives the exact inclusion-exclusion identity + + E_P(A) = E_R(A) - L_F(A) - L_G(A) + X_FG(A). + +All energies on orthogonal pairs are unchanged by adding a scalar matrix. +Apply (3) and (4) to A0. Since 54 - 2(17/2) = 37, this is (1). +Every residual term is a square, so the lower bound follows. Equality holds +exactly when the two frame diagonals and every cross-frame orthogonal defect +of A0 vanish. + +For any common real linear map T, put M=T^T T. The deformed inner product +between originally orthogonal unit roots is (Tu)^T(Tv)=u^T M v. Thus + + ||M - tr(M) I/8|| <= sqrt(E_P(M)/37). (5) + +In particular an invertible common T preserving every such zero has +T^T T=cI with c>0. Exact qualitative rigidity has prior literature in this +repository; the contribution here is the sharp quantitative identity (1) +and its equality certificate. Equation (5) uses absolute inner products +before any separate normalization of the deformed lines. It does not price +metric changes, physical native maps or recursive work. + +## 4. Sharpness and rational common deformations + +In integer coordinates take F to be + + 2(e_0+e_1), 2(e_0-e_1), ..., 2(e_6+e_7), 2(e_6-e_7), + +and G to be the eight Sylvester rows + + g_i[j] = (-1)^{popcount(i AND j)}, 0 <= i,j < 8. + +Normalize all these vectors by sqrt(8). They are disjoint E8 frames. Let A +have the following nonzero entries, together with their symmetric partners: + + A[0,7]=-1, A[1,6]=-1, A[2,5]=1, A[3,4]=1. + +Then tr(A)=0, A^2=I and ||A||^2=8. Direct integer evaluation checks both +zero frame diagonals and every required cross-frame zero. In this example +P has 2,860 unordered orthogonal pairs and there are 32 orthogonal F-G pairs. +Their literal energy sum is E_P(A)=296=37*8. The pair counts refer to this +explicit example; they are not asserted for every pair of deleted frames. + +For any nonzero rational s with |s|<1, T_s=I+sA is invertible and + + T_s^T T_s = (1+s^2)I+2sA. + +Its trace-free part is 2sA. By homogeneity it attains equality in (5), and +T_s tends to I as s tends to zero. Hence the constant cannot increase even +when restricted to positive definite common metrics from rational invertible +maps arbitrarily near the identity. + +## Evidence boundary + +The standard-library verifier checks the full E8 coefficient identity and +all stars, the two explicit frame deletions, all coefficients of (1) for +the example, and the literal equality sum. The written removal argument +supplies the quantifiers over every pair of disjoint frames and every real +symmetric matrix. Seven controls discriminate omitted data, changed constants, +invalid frame boundaries and a changed witness. Source hashes in its printed +receipt bind the exact proof, implementation and metadata bytes. + +No human or proof-kernel review is claimed. The selected result, all five +framework assumptions, native/dirty restoration, compiler, precision/tape, +complete invoice and multiplication theorem are unchanged. diff --git a/research/p104-metric-energy/README.md b/research/p104-metric-energy/README.md new file mode 100644 index 0000000000..64cfaaa94b --- /dev/null +++ b/research/p104-metric-energy/README.md @@ -0,0 +1,99 @@ +# Sharp common-metric orthogonality energy on P104 + +This contribution was produced by Nick Petalas. Apache-2.0. + +A common ambient deformation of a two-frame-punctured E8 configuration obeys +an exact sum-of-squares constraint. For any real symmetric metric A, let +A0=A-tr(A)I/8 and sum the squared values u^T A v over unordered orthogonal +unit-root pairs remaining after two disjoint frames are removed. Then + + E_P(A) = 37 ||A0||_F^2 + + (17/2) sum_{u in the two frames}(u^T A0 u)^2 + + sum_{orthogonal u,v in different deleted frames}(u^T A0 v)^2. + +Thus E_P(A) >= 37 ||A0||_F^2. An explicit rational symmetric involution has +norm squared 8 and energy 296, proving the uniform constant sharp. Rational +invertible common maps I+sA attain equality arbitrarily near identity. +For M=T^T T, the defect energy bounds distance from a conformal metric by +||M-tr(M)I/8||_F <= sqrt(E_P(M)/37). + +Claim type: scoped proof with exact finite premises and an equality +certificate. [PROOF.md](PROOF.md) gives the quantified argument. [verify.py](verify.py) +uses integer arithmetic and the standard library. This is a quantitative +obstruction to changing the common ambient metric while keeping the E8 +orthogonality constraints approximately exact. It supplies no new kappa. + +## Evidence and reproduction + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-metric-energy/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p104-metric-energy/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-metric-energy +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-metric-energy --check-source-history +``` + +Any CPython 3.12 interpreter can replace the local absolute path. Expected +status: `PASS_P104_METRIC_ENERGY`. The checker enumerates 120 root lines, +3,780 full orthogonal pairs and all 120 stars, checks 1,296 coefficients per +quadratic identity, and evaluates all 2,860 orthogonal pairs of the explicit +sharp example. Seven controls reject changed premises or stronger constants. +The printed receipt is generated from current file hashes and computed values. +No generated files or logs are written into the checkout. + +Local normal and optimized direct checks and both registered commands passed +on CPython 3.12.15, macOS 27.0.1 arm64. Each direct command took 0.13 seconds +in the initial timed run. Hosted CI is recorded separately in the PR body. + +The checker has fixed dimension eight, 36 symmetric coordinates and at most +7,140 candidate root pairs. Every loop ranges over one of these fixed finite +collections. Managed Python allocation is bounded by those inventories; no +fixed-allocation claim is made. Six fixed callbacks are used only for rejecting +controls. Functions have at most 26 physical lines. Warning-strict normal and +optimized execution supply the local Python diagnostics; no external static +analyzer was available. These are implementation limits, not extra premises +of the mathematical theorem. + +## Scope, predecessors and novelty + +The exact E8 masked-realization questions and qualitative rigidity precede +this result. Credit Brett Halligan / [PR1212](https://github.com/CrocSwap/integer-mult-bounds/pull/1212), +Aaron Wang / PR1292, Josie Elliston / PR1389 and PR1399, and their retained +E8 decoder lineage. Their broader decoder theorems are context, not premises +replayed here. The root coordinates and elementary frame identities are +standard. No predecessor implementation is imported or copied. The new step +is the explicit quantitative energy identity, constant 37 and sharpness family. + +This changes the `complex-rank-shape-decoder` card to a geometry boundary +question. It quantifies the absolute orthogonality defect forced by a common +ambient deformation. It does not bound independent port motions, +general fitting matrices, normalized correlation errors, helper topology or +productive credits. The sharp example is not identified with the selected +frame-pair orbit. The lower bound itself holds for every disjoint frame pair. +No selected supplier replay, physical implementation, full signed invoice, +formal proof-kernel check or complete multiplication theorem is supplied. +Independent human and formal proof-kernel review are unclaimed. + +The selected-binding orientation command passed at base +`2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8. The selected +conditional kappa remains 781451/250000000. Its five framework assumptions +remain. Live open PRs, active Discussions, account history, claims, main +READMEs and merged formula/object searches were checked before claiming; +these bounded and sparse searches do not establish literature priority. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294832) +records the original question. + +## Open next questions + +- Is 37 also the sharp constant for each individual disjoint-frame orbit, + including the selected P104 orbit? First fix that orbit and evaluate the + residual squares on trace-free symmetric matrices. This could strengthen + a source-specific obstruction. The present uniform theorem does not identify + the selected orbit's equality space. +- Can a useful decoder change escape common-metric rigidity through independent + port motions while retaining legal labels and a favorable complete bill? + First exhibit one arbitrary-input local identity with its restored outputs + and actual consumer. Native realization and the complete invoice remain open. + +See [TASK.json](TASK.json) for the structured questions and scope declaration. diff --git a/research/p104-metric-energy/SOURCES.json b/research/p104-metric-energy/SOURCES.json new file mode 100644 index 0000000000..0fda350627 --- /dev/null +++ b/research/p104-metric-energy/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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" + } + ] +} diff --git a/research/p104-metric-energy/TASK.json b/research/p104-metric-energy/TASK.json new file mode 100644 index 0000000000..6f32aa887b --- /dev/null +++ b/research/p104-metric-energy/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "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": "Sharp common-metric orthogonality energy on every two-disjoint-frame puncture of E8, with a rational equality family.", + "scope_change_reason": "Replace a complete coframe itinerary search with an originally posed quantitative geometry obstruction for one common ambient deformation. No complete signed invoice is claimed.", + "bottleneck_link": "The complex supplier binds. A common ambient metric deformation is a possible changed-geometry route; the sum-of-squares identity constrains its absolute orthogonality defects, without excluding independent line motions or new helper topologies.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified quantitative identity and sharp equality example; leave orbit-specific constants and different deformation models as open questions.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py: exact E8 energy coefficients, 120 tight stars, frame deletion identities, sharp energy 296 and seven controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is 37 sharp for every individual disjoint-frame orbit, including the selected P104 orbit?", + "why_it_matters": "An orbit-specific constant could strengthen the quantitative obstruction.", + "first_step": "Fix the selected frame-pair orbit and compute the kernel of the residual squares in equation (1).", + "blocked_by": "The present sharp example is not identified with the selected frame-pair orbit." + }, + { + "question": "Can independently moved ports yield a legal improved decoder outside the common-metric class?", + "why_it_matters": "The common-metric obstruction does not cover this possible escape.", + "first_step": "Give one arbitrary-input local identity, restored boundary and physical consumer, then price its complete signed invoice.", + "blocked_by": "No native realization, complete caller or favorable complete bill is supplied here." + } + ] +} diff --git a/research/p104-metric-energy/VERIFY.json b/research/p104-metric-energy/VERIFY.json new file mode 100644 index 0000000000..8b4de3c31a --- /dev/null +++ b/research/p104-metric-energy/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 all-E8 quadratic identity, all tight stars, frame removal, sum of squares, sharp equality and seven controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete certificate and controls with Python assertions disabled." + } + ] +} diff --git a/research/p104-metric-energy/verify.py b/research/p104-metric-energy/verify.py new file mode 100644 index 0000000000..87c9935fd0 --- /dev/null +++ b/research/p104-metric-energy/verify.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Exact finite premises and equality witness for PROOF.md. Apache-2.0.""" +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path + +DIM = 8 +PAIRS = tuple(combinations(range(DIM), 2)) +SIZE = DIM + len(PAIRS) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def roots(): + """One integer representative per E8 line, with squared norm eight.""" + result = [] + for i, j in PAIRS: + for sign in (1, -1): + row = [0] * DIM + row[i], row[j] = 2, 2 * sign + result.append(tuple(row)) + for signs in product((1, -1), repeat=DIM - 1): + if signs.count(-1) % 2 == 0: + result.append((1,) + signs) + need(len(result) == len(set(result)) == 120, "120 distinct root lines") + return tuple(result) + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y, strict=True)) + + +def zero_matrix(size): + return [[0] * size for _ in range(size)] + + +def row_form(x, y): + """Coefficients of x^T A y in the 36 entries of symmetric A.""" + return tuple(x[i] * y[i] for i in range(DIM)) + tuple( + x[i] * y[j] + x[j] * y[i] for i, j in PAIRS + ) + + +def add_outer(matrix, row): + nonzero = tuple((i, value) for i, value in enumerate(row) if value) + for i, a in nonzero: + for j, b in nonzero: + matrix[i][j] += a * b + + +def energy_matrix(edges): + matrix = zero_matrix(SIZE) + for x, y in edges: + add_outer(matrix, row_form(x, y)) + return matrix + + +def orthogonal_edges(lines): + return tuple((x, y) for x, y in combinations(lines, 2) if dot(x, y) == 0) + + +def metric_entry(i, j): + return (1 if i < DIM else 2) if i == j else 0 + + +def trace_entry(i, j): + return int(i < DIM and j < DIM) + + +def check_full_energy(matrix): + for i in range(SIZE): + for j in range(SIZE): + need(matrix[i][j] == 3456 * metric_entry(i, j) + - 432 * trace_entry(i, j), "Full E8 energy coefficient") + + +def check_stars(lines): + for x in lines: + star = tuple(y for y in lines if dot(x, y) == 0) + need(len(star) == 63, "Every orthogonal star has 63 lines") + for i in range(DIM): + for j in range(DIM): + actual = sum(y[i] * y[j] for y in star) + need(actual == 72 * int(i == j) - 9 * x[i] * x[j], + "Every E7 star is a tight frame") + + +def frames(lines): + first = tuple(x for x in lines if sum(bool(v) for v in x) == 2 + and next(i for i, v in enumerate(x) if v) // 2 + == max(i for i, v in enumerate(x) if v) // 2) + second = tuple(tuple((-1) ** ((i & j).bit_count() % 2) + for j in range(DIM)) for i in range(DIM)) + check_frames(lines, first, second) + return first, second + + +def check_frames(lines, first, second): + for frame in (first, second): + need(len(frame) == len(set(frame)) == DIM, "Frame cardinality") + need(set(frame) <= set(lines), "Frame lines belong to E8") + for i in range(DIM): + for j in range(DIM): + need(dot(frame[i], frame[j]) == 8 * int(i == j), + "Frame is orthonormal after normalization") + need(set(first).isdisjoint(second), "Deleted frames are disjoint") + + +def check_deletion(all_edges, frame): + deleted = energy_matrix(tuple((x, y) for x, y in all_edges + if x in frame or y in frame)) + diagonal = energy_matrix(tuple((x, x) for x in frame)) + for i in range(SIZE): + for j in range(SIZE): + need(2 * deleted[i][j] == 1088 * metric_entry(i, j) + - 17 * diagonal[i][j], "Frame deletion energy coefficient") + return diagonal + + +def witness(): + matrix = zero_matrix(DIM) + for i, j, sign in ((0, 7, -1), (1, 6, -1), (2, 5, 1), (3, 4, 1)): + matrix[i][j] = matrix[j][i] = sign + return matrix + + +def bilinear(x, matrix, y): + return sum(x[i] * matrix[i][j] * y[j] + for i in range(DIM) for j in range(DIM)) + + +def check_witness(matrix, live_edges, first, second): + need(sum(matrix[i][i] for i in range(DIM)) == 0, "Witness trace zero") + norm = sum(value * value for row in matrix for value in row) + need(norm == 8, "Witness Frobenius norm squared") + for i in range(DIM): + for j in range(DIM): + need(sum(matrix[i][k] * matrix[k][j] for k in range(DIM)) + == int(i == j), "Witness squares to identity") + for x in first + second: + need(bilinear(x, matrix, x) == 0, "Zero frame diagonals") + for x in first: + for y in second: + if dot(x, y) == 0: + need(bilinear(x, matrix, y) == 0, "Zero cross-frame defect") + energy64 = sum(bilinear(x, matrix, y) ** 2 for x, y in live_edges) + need(energy64 == 64 * 37 * norm == 18944, "Sharp energy 296") + return norm, energy64 + + +def check_sos(live_matrix, cross_matrix, diagonal_first, diagonal_second): + for i in range(SIZE): + for j in range(SIZE): + rhs = (4736 * metric_entry(i, j) - 864 * trace_entry(i, j) + + 17 * (diagonal_first[i][j] + diagonal_second[i][j]) + + 2 * cross_matrix[i][j]) + need(2 * live_matrix[i][j] == rhs, "P104 sum-of-squares coefficient") + + +def rejects(operation, message): + try: + operation() + except ValueError: + return + raise ValueError("Control accepted: " + message) + + +def controls(lines, all_edges, first, second, live_edges, full_matrix): + rejects(lambda: check_full_energy(energy_matrix(all_edges[:-1])), + "one missing full-energy edge") + rejects(lambda: check_stars(lines[:-1]), "one missing root line") + rejects(lambda: check_frames(lines, first, first), "repeated frame") + rejects(lambda: check_frames(lines, first[:-1], second), "short frame") + changed = [row[:] for row in full_matrix] + changed[0][0] += 1 + rejects(lambda: check_full_energy(changed), "one changed coefficient") + changed_witness = witness() + changed_witness[0][0] = 1 + rejects(lambda: check_witness(changed_witness, live_edges, first, second), + "changed equality witness") + need(100 * 18944 < 64 * 3701 * 8, "37.01 fails on equality witness") + return 7 + + +def run(): + lines = roots() + need(all(dot(x, x) == 8 for x in lines), "Root normalization") + all_edges = orthogonal_edges(lines) + need(len(all_edges) == 3780, "Full orthogonal pair count") + full_matrix = energy_matrix(all_edges) + check_full_energy(full_matrix) + check_stars(lines) + first, second = frames(lines) + live = tuple(x for x in lines if x not in first + second) + live_edges = orthogonal_edges(live) + cross = tuple((x, y) for x in first for y in second if dot(x, y) == 0) + need((len(live), len(live_edges), len(cross)) == (104, 2860, 32), + "Equality example inventory") + diagonal_first = check_deletion(all_edges, first) + diagonal_second = check_deletion(all_edges, second) + check_sos(energy_matrix(live_edges), energy_matrix(cross), + diagonal_first, diagonal_second) + norm, energy64 = check_witness(witness(), live_edges, first, second) + control_count = controls(lines, all_edges, first, second, live_edges, full_matrix) + return {"status": "PASS_P104_METRIC_ENERGY", "root_lines": len(lines), + "full_orthogonal_pairs": len(all_edges), "stars_checked": len(lines), + "quadratic_coefficients_per_identity": SIZE ** 2, + "example_live_lines": len(live), "example_orthogonal_pairs": len(live_edges), + "sharp_constant": 37, "witness_norm_squared": norm, + "witness_energy": energy64 // 64, "rejecting_controls": control_count} + + +def main(): + result = run() + here = Path(__file__).resolve().parent + names = ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json") + result["source_sha256"] = {name: sha256((here / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()