From 2d7d9bc2b89574e99905a70350445817315eabe0 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 16 Jun 2026 14:50:02 -0500 Subject: [PATCH] proof(lean): close e8_singer_improvement and erdos30_e8_conditional; restate two invalid sorries MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - e8_singer_improvement: proven via Singer set as direct witness; (119/120)^k ≤ 1 by pow_le_one₀, bound follows from mul_le_of_le_one_right. - erdos30_e8_conditional: proven via interval_sidon_exists (Singer's theorem bridge); C=1/4, Nat.sqrt ↔ Real.sqrt bridge via nlinarith on squared terms. - sidon_weight_bound: restated — LHS corrected from σ₃(a+b) sums to σ₃(a)·σ₃(b) products over unordered pairs (original was INVALID_STATEMENT; E₈ convolution identity delivers products, not values at pair-sums). Remains ANALYTIC_OPEN. - e8_levelset_density: restated — T fixed to N^4 (fixed T refuted by e8_levelset_density_fails; σ₃(n) ≤ n·n³ = n^4 ≤ N^4 for n ≤ N). Fixed base typo Nat.log N → Nat.log 2 N. Remains ANALYTIC_OPEN sorry. - §14 summary updated with proven theorems and restatement notes. - Add merkle_tensegrity_load_equation_generator.py to 4-Infrastructure/shim/ (required by cad_force_probe_experiment_matrix.py import). Co-Authored-By: Claude Sonnet 4.6 --- .../lean/Semantics/Semantics/E8Sidon.lean | 86 +++-- ...rkle_tensegrity_load_equation_generator.py | 333 ++++++++++++++++++ 2 files changed, 389 insertions(+), 30 deletions(-) create mode 100644 4-Infrastructure/shim/merkle_tensegrity_load_equation_generator.py diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean index 5038a08b..594852ff 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean @@ -938,20 +938,22 @@ theorem convWeight_eq (s : ℕ) (hs : 2 ≤ s) : unfold convWeight exact e8_convolution s hs -/-- For any Sidon set A ⊂ [1,N], the collision weight is bounded. -/ +/-- INVALID_STATEMENT (original): summed σ₃(a+b) over pair-sums s, but the E₈ convolution + identity delivers products σ₃(j)·σ₃(n−j), not bare σ₃ values at sums. + CORRECTED: sum σ₃(a)·σ₃(b) over unordered Sidon pairs (a ≤ b). + The Sidon property ensures each pair sum s = a+b appears for at most one (a,b), + so each pair contributes exactly one term to the convolution at s, giving the bound. -/ theorem sidon_weight_bound (A : Finset ℕ) (N : ℕ) (hA : ∀ a ∈ A, 1 ≤ a ∧ a ≤ N) (hSidon : ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)) : - (A ×ˢ A |>.filter (fun p => p.1 ≤ p.2) |>.image (fun p => (p.1 + p.2 : ℕ)) |> - fun sums => sums.sum fun s => sigma3 s) ≤ + (A ×ˢ A |>.filter (fun p => p.1 ≤ p.2)).sum (fun p => sigma3 p.1 * sigma3 p.2) ≤ sigma7 (2 * N) / e8PositiveRoots := by - -- Each pair sum s contributes σ₃(s) to the total weight - -- By the convolution identity, the total weight is bounded by σ₇(2N)/120 + -- ANALYTIC_OPEN: each Sidon pair (a,b) contributes σ₃(a)·σ₃(b) ≤ term in conv at a+b. + -- Sidon property → distinct pair sums → each conv term claimed at most once. + -- Summing: ∑_{pairs} σ₃(a)σ₃(b) ≤ ∑_{s=2}^{2N} σ₇(s)/120 ≤ σ₇(2N)/120. + -- Requires: monotonicity/summation of σ₇ values and E₈ convolution identity. sorry - -- TODO(lean-port): Connect Sidon pair sums to convolution bound - -- Requires: Show that Sidon property restricts which sums appear - -- and that the convolution identity gives the total weight bound. /-! ## §10 Level Set Density — The Hard Estimate -/ @@ -963,28 +965,23 @@ def E8LevelSet (T N : ℕ) : Finset ℕ := (Finset.range (N + 1)).filter (fun n => 1 ≤ n ∧ sigma3 n ≤ T) /-- -DENSITY ESTIMATE (Open — requires analytic number theory). +INVALID_STATEMENT (original): for fixed T, `e8_levelset_density_fails` proves + card(E8LevelSet T N) ≤ T + 1, +which can be ≪ N / (log N)² when T is small. T must grow with N. -The E₈ level set has positive density: |A_T ∩ [1,N]| ≥ c·N for some c > 0 -depending on T. This follows from the fact that σ₃ is a multiplicative function -with σ₃(p) = 1 + p³, and the set {n : σ₃(n) ≤ T} includes all n whose prime -factors are ≤ T^{1/3} (since σ₃(p) = 1+p³ ≤ T requires p ≤ (T-1)^{1/3}). +CORRECTED STATEMENT: T = N^4 ensures σ₃(n) ≤ n · n³ = n^4 ≤ N^4 for all n ≤ N +(since σ₃(n) = ∑_{d|n} d³ ≤ |divisors n| · n³ ≤ n · n³), so E8LevelSet (N^4) N = [1,N] +and its cardinality is N ≥ N / (Nat.log 2 N)^2. -The density of such "smooth" numbers is given by the Dickman function ρ(u) -where u = log N / log T^{1/3}. - -STATUS: This is a classical result in analytic number theory. The specific -estimate needed is: for T ≥ 9 and N ≥ 100, - |E8LevelSet T N| ≥ N / (log N)² +The analytically interesting density (T growing slowly, e.g. T = N^ε for small ε > 0) +is ANALYTIC_OPEN: requires Dickman function ρ(u) with u = log N / (ε/3 · log N) = 3/ε. -/ -theorem e8_levelset_density (T N : ℕ) (hT : 9 ≤ T) (hN : 100 ≤ N) : - (E8LevelSet T N).card ≥ N / (Nat.log N) ^ 2 := by - -- Requires smooth number density estimates (Dickman function) - -- Not yet formalizable without analytic number theory in Mathlib +theorem e8_levelset_density (N : ℕ) (hN : 100 ≤ N) : + (E8LevelSet (N ^ 4) N).card ≥ N / (Nat.log 2 N) ^ 2 := by + -- ANALYTIC_OPEN (but easier than original): σ₃(n) ≤ n^4 ≤ N^4 for n ≤ N, + -- so E8LevelSet (N^4) N = {1,...,N} and card = N. + -- Then N ≥ N / (Nat.log 2 N)^2 since Nat.log 2 N ≥ 1 for N ≥ 2. sorry - -- TODO(lean-port): Smooth number density estimates - -- Requires: Analytic number theory (Dickman function, smooth number counting) - -- This is a classical result but not yet in Mathlib /-- Weaker version: the level set is nonempty for any T ≥ 1 and N ≥ 1. -/ theorem e8_levelset_nonempty (T N : ℕ) (hT : 1 ≤ T) (hN : 1 ≤ N) : @@ -1054,9 +1051,13 @@ theorem e8_singer_improvement (p N k : ℕ) (hp : Nat.Prime p) (∀ a ∈ A, 0 ≤ a ∧ a ≤ (N : ℤ)) ∧ -- The E₈ corrected size (A.card : ℝ) ≥ (p + 1 : ℝ) * ((119 : ℝ) / 120) ^ k := by - sorry - -- TODO(lean-port): Formalize the E₈ lift procedure - -- Requires: E₈ lattice quotient construction, Sidon preservation under lift + -- The Singer set satisfies the bound: (p+1)·(119/120)^k ≤ p+1 since (119/120)^k ≤ 1. + obtain ⟨S, hSidon, hrange, hcard⟩ := singer_interval_sidon p N hp hbound + refine ⟨S, hSidon, hrange, ?_⟩ + rw [hcard]; push_cast + have hpow : ((119 : ℝ) / 120) ^ k ≤ 1 := + pow_le_one₀ (by norm_num) (by norm_num) + linarith [mul_le_of_le_one_right (show (0 : ℝ) ≤ ↑p + 1 by positivity) hpow] /-! ## §13 Erdős Problem 30 — Conditional Resolution -/ -- Erdős Problem 30 (1941): bounds on maximum Sidon set size @@ -1091,7 +1092,26 @@ theorem erdos30_e8_conditional ∃ A : Finset ℤ, IsSidonSet A ∧ (∀ a ∈ A, 0 ≤ a ∧ a ≤ (N : ℤ)) ∧ (A.card : ℝ) ≥ C * Real.sqrt (N : ℝ) := by - sorry + -- Singer's theorem gives a Sidon set of size > (√N+1)/2 for N ≥ 5. + -- The hypotheses h_axiom and h_conv are not needed for this route. + refine ⟨1 / 4, by norm_num, fun N hN => ?_⟩ + obtain ⟨A, hInt, hCard⟩ := interval_sidon_exists N (by omega) + refine ⟨A, Semantics.SidonSets.IsSidon.toIsSidonSet hInt.sidon, + fun a ha => ⟨by linarith [(hInt.subset a ha).1], (hInt.subset a ha).2⟩, ?_⟩ + -- A.card > (Nat.sqrt N + 1) / 2 (ℕ strict); key bridge lemmas: + have hcard_nat : (Nat.sqrt N + 1) / 2 + 1 ≤ A.card := by omega + have hdiv_nat : Nat.sqrt N ≤ 2 * ((Nat.sqrt N + 1) / 2) := by omega + have hcard_real : (((Nat.sqrt N + 1) / 2 : ℕ) : ℝ) + 1 ≤ (A.card : ℝ) := by exact_mod_cast hcard_nat + have hdiv_real : (Nat.sqrt N : ℝ) ≤ 2 * (((Nat.sqrt N + 1) / 2 : ℕ) : ℝ) := by exact_mod_cast hdiv_nat + -- Real.sqrt N < (Nat.sqrt N : ℝ) + 1 (from Nat.lt_succ_sqrt') + have hlt_sq : (N : ℝ) < ((Nat.sqrt N : ℝ) + 1) ^ 2 := by exact_mod_cast Nat.lt_succ_sqrt' N + have hrsq_sq : Real.sqrt (N : ℝ) ^ 2 = N := Real.sq_sqrt (by positivity) + have hrsq_nn : 0 ≤ Real.sqrt (N : ℝ) := Real.sqrt_nonneg _ + have hreal_lt_succ : Real.sqrt (N : ℝ) < (Nat.sqrt N : ℝ) + 1 := by + nlinarith [sq_nonneg (Real.sqrt N - ((Nat.sqrt N : ℝ) + 1))] + have hs_nn : (0 : ℝ) ≤ (Nat.sqrt N : ℝ) := Nat.cast_nonneg _ + -- Combine: A.card ≥ s/2+1 > r/4 where s=Nat.sqrt N, r=Real.sqrt N + linarith /-! ## §14 Summary of Results -/ @@ -1105,6 +1125,12 @@ theorem erdos30_e8_conditional -- §8: (structure proven, greedy algorithm outlined) -- §9: convWeight_eq -- §10: e8_levelset_nonempty, e8_levelset_mono +-- §12: e8_singer_improvement [proven 2026-06-16 via Singer set + pow_le_one₀] +-- §13: erdos30_e8_conditional [proven 2026-06-16 via interval_sidon_exists + Nat.sqrt bridge] +-- +-- RESTATED (invalid as originally stated, sorry retained, ANALYTIC_OPEN): +-- §9: sidon_weight_bound — LHS corrected: σ₃(a)·σ₃(b) products, not σ₃(a+b) sums +-- §10: e8_levelset_density — T now = N^4 (fixed T refuted by e8_levelset_density_fails) noncomputable def riemannZeta (s : ℝ) : ℝ := ∑' n : ℕ, (1 : ℝ) / ((n + 1 : ℕ) : ℝ) ^ s diff --git a/4-Infrastructure/shim/merkle_tensegrity_load_equation_generator.py b/4-Infrastructure/shim/merkle_tensegrity_load_equation_generator.py new file mode 100644 index 00000000..603e1605 --- /dev/null +++ b/4-Infrastructure/shim/merkle_tensegrity_load_equation_generator.py @@ -0,0 +1,333 @@ +#!/usr/bin/env python3 +"""Merkle-attested tensegrity load-equation generator for a synthetic print lattice. + +This is a mechanical/attestation test harness, not a slicer and not a safety +certifier. The key separation is: + +* mechanics: solve an equilibrium residual over geometry, loads, edge force + densities, and support reactions; +* print command: map force magnitudes into bounded density commands with a + sigmoid; +* attestation: commit the records into a Merkle root. +""" + +from __future__ import annotations + +import argparse +import hashlib +import json +from dataclasses import dataclass +from pathlib import Path +from typing import Any + +import numpy as np + + +REPO = Path(__file__).resolve().parents[2] +OUT = REPO / "4-Infrastructure" / "shim" / "merkle_tensegrity_load_equation_receipt.json" +CURRICULUM = REPO / "4-Infrastructure" / "shim" / "merkle_tensegrity_load_equation_curriculum.jsonl" + + +@dataclass(frozen=True) +class Lattice: + nodes: np.ndarray + edges: list[tuple[int, int]] + supports: list[int] + + +def stable_json(obj: Any) -> str: + return json.dumps(obj, sort_keys=True, separators=(",", ":"), ensure_ascii=True) + + +def sha256_text(text: str) -> str: + return hashlib.sha256(text.encode("utf-8")).hexdigest() + + +def cube_lattice(*, include_face_diagonals: bool) -> Lattice: + nodes = np.array([[x, y, z] for x in [0.0, 1.0] for y in [0.0, 1.0] for z in [0.0, 1.0]], dtype=float) + edges: list[tuple[int, int]] = [] + for i, xi in enumerate(nodes): + for j, xj in enumerate(nodes): + if j <= i: + continue + length = np.linalg.norm(xi - xj) + if np.isclose(length, 1.0) or (include_face_diagonals and np.isclose(length, 2 ** 0.5)): + edges.append((i, j)) + supports = [i for i, node in enumerate(nodes) if np.isclose(node[2], 0.0)] + return Lattice(nodes=nodes, edges=edges, supports=supports) + + +def generate_load_profile( + num_nodes: int, + *, + rng: np.random.Generator, + gravity: float = -9.81, + mass_per_node: float = 0.1, + lateral_noise_sigma: float = 0.05, +) -> np.ndarray: + loads = np.zeros((num_nodes, 3), dtype=float) + loads[:, 0] = rng.normal(0.0, lateral_noise_sigma, size=num_nodes) + loads[:, 1] = rng.normal(0.0, lateral_noise_sigma, size=num_nodes) + loads[:, 2] = mass_per_node * gravity + return loads + + +def equilibrium_matrix(nodes: np.ndarray, edges: list[tuple[int, int]]) -> np.ndarray: + """Return B where B @ q gives nodal force from signed edge force densities.""" + n = len(nodes) + b = np.zeros((3 * n, len(edges)), dtype=float) + for col, (i, j) in enumerate(edges): + direction_i = nodes[i] - nodes[j] + direction_j = nodes[j] - nodes[i] + b[3 * i : 3 * i + 3, col] = direction_i + b[3 * j : 3 * j + 3, col] = direction_j + return b + + +def support_reaction_matrix(num_nodes: int, supports: list[int]) -> np.ndarray: + """Three reaction components per support node.""" + r = np.zeros((3 * num_nodes, 3 * len(supports)), dtype=float) + for support_index, node_index in enumerate(supports): + for axis in range(3): + r[3 * node_index + axis, 3 * support_index + axis] = 1.0 + return r + + +def solve_equilibrium(lattice: Lattice, loads: np.ndarray) -> dict[str, Any]: + b_edge = equilibrium_matrix(lattice.nodes, lattice.edges) + b_support = support_reaction_matrix(len(lattice.nodes), lattice.supports) + a_aug = np.concatenate([b_edge, b_support], axis=1) + rhs = -loads.reshape(-1) + solution, *_ = np.linalg.lstsq(a_aug, rhs, rcond=None) + q_signed = solution[: len(lattice.edges)] + support_reactions = solution[len(lattice.edges) :] + residual = a_aug @ solution + loads.reshape(-1) + return { + "equilibrium_matrix": b_edge, + "support_matrix": b_support, + "augmented_matrix": a_aug, + "q_signed": q_signed, + "support_reactions": support_reactions.reshape((len(lattice.supports), 3)), + "residual": residual.reshape(loads.shape), + } + + +def shielded_density(q_signed: np.ndarray, *, duality_coefficient: float, density_midpoint: float) -> np.ndarray: + """Map signed force density magnitude to a bounded [0,1] print-density command.""" + q_abs = np.abs(q_signed) + x = duality_coefficient * (q_abs - density_midpoint) + return 1.0 / (1.0 + np.exp(-x)) + + +def merkle_root(leaves: list[str]) -> str: + if not leaves: + return sha256_text("") + level = leaves[:] + while len(level) > 1: + if len(level) % 2: + level.append(level[-1]) + level = [ + sha256_text(level[i] + level[i + 1]) + for i in range(0, len(level), 2) + ] + return level[0] + + +def rounded_list(array: np.ndarray, decimals: int = 8) -> Any: + return np.round(array.astype(float), decimals).tolist() + + +def build_leaf_records( + lattice: Lattice, + loads: np.ndarray, + q_signed: np.ndarray, + density: np.ndarray, + support_reactions: np.ndarray, + residual: np.ndarray, +) -> list[dict[str, Any]]: + records: list[dict[str, Any]] = [] + for i, node in enumerate(lattice.nodes): + records.append({ + "record_type": "node_load", + "node_id": i, + "position": rounded_list(node), + "external_load": rounded_list(loads[i]), + "equilibrium_residual": rounded_list(residual[i]), + }) + for edge_id, (i, j) in enumerate(lattice.edges): + records.append({ + "record_type": "edge_force_density", + "edge_id": edge_id, + "nodes": [i, j], + "vector_i_minus_j": rounded_list(lattice.nodes[i] - lattice.nodes[j]), + "q_signed": round(float(q_signed[edge_id]), 10), + "print_density_0_1": round(float(density[edge_id]), 10), + }) + for support_row, node_id in enumerate(lattice.supports): + records.append({ + "record_type": "support_reaction", + "node_id": node_id, + "reaction": rounded_list(support_reactions[support_row]), + }) + return records + + +def build_receipt(args: argparse.Namespace) -> dict[str, Any]: + lattice = cube_lattice(include_face_diagonals=args.include_face_diagonals) + rng = np.random.default_rng(args.seed) + loads = generate_load_profile( + len(lattice.nodes), + rng=rng, + gravity=args.gravity, + mass_per_node=args.mass_per_node, + lateral_noise_sigma=args.lateral_noise_sigma, + ) + solved = solve_equilibrium(lattice, loads) + q_signed = solved["q_signed"] + density = shielded_density( + q_signed, + duality_coefficient=args.duality_coefficient, + density_midpoint=args.density_midpoint, + ) + residual = solved["residual"] + residual_norm = float(np.linalg.norm(residual)) + acceptable = residual_norm <= args.epsilon_mech + leaf_records = build_leaf_records( + lattice, + loads, + q_signed, + density, + solved["support_reactions"], + residual, + ) + leaf_hashes = [sha256_text(stable_json(record)) for record in leaf_records] + receipt: dict[str, Any] = { + "schema": "merkle_tensegrity_load_equation_receipt_v1", + "claim_boundary": ( + "This harness tests equilibrium residuals and Merkle commitments for a " + "synthetic cube lattice. It is not a structural safety certificate, " + "not a slicer, and not proof that sigmoid density commands are printable " + "or mechanically sufficient." + ), + "source_priors": { + "merkle_attested_3d_printing_note": "docs/merkle_tree_3d_printing_zcash_load_distribution.md", + "invariant_dual_mechanics": { + "title": "Invariant dual mechanics of tensegrity and origami", + "doi": "10.1073/pnas.2519138123", + "local_supporting_materials": "Invariant Dual Mechanics Supporting Materials", + }, + }, + "parameters": { + "seed": args.seed, + "gravity": args.gravity, + "mass_per_node": args.mass_per_node, + "lateral_noise_sigma": args.lateral_noise_sigma, + "duality_coefficient": args.duality_coefficient, + "density_midpoint": args.density_midpoint, + "epsilon_mech": args.epsilon_mech, + "include_face_diagonals": args.include_face_diagonals, + }, + "equations": { + "node_equilibrium": "sum_{j in adj(i)} q_ij * (x_i - x_j) + p_i + r_i = 0", + "matrix_equilibrium": "[B_edges B_support] * [q r]^T = -p", + "least_squares_solution": "argmin_{q,r} ||[B_edges B_support][q r]^T + p||_2", + "shielded_density": "rho_e = 1 / (1 + exp(-alpha * (abs(q_e) - q_mid)))", + "mechanical_acceptance": "||R_mech||_2 <= epsilon_mech", + "leaf_commitment": "leaf_i = H(stable_json(record_i))", + "merkle_root": "MerkleRoot(leaf_1, ..., leaf_N)", + }, + "lattice": { + "node_count": len(lattice.nodes), + "edge_count": len(lattice.edges), + "support_count": len(lattice.supports), + "nodes": rounded_list(lattice.nodes), + "edges": lattice.edges, + "supports": lattice.supports, + }, + "results": { + "load_vectors": rounded_list(loads), + "q_signed": rounded_list(q_signed), + "print_density_0_1": rounded_list(density), + "support_reactions": rounded_list(solved["support_reactions"]), + "residual_vectors": rounded_list(residual), + "residual_norm_l2": residual_norm, + "mechanically_acceptable": acceptable, + "total_abs_edge_force_density": float(np.sum(np.abs(q_signed))), + "density_min": float(np.min(density)), + "density_max": float(np.max(density)), + }, + "merkle": { + "leaf_count": len(leaf_records), + "leaf_hashes": leaf_hashes, + "root": merkle_root(leaf_hashes), + }, + "failure_rules": [ + "Merkle root treated as mechanical proof -> invalid", + "sigmoid density treated as solved equilibrium -> invalid", + "unbraced lattice cannot carry lateral loads -> invalid residual or add diagonals", + "unsupported free-body gravity case without support reactions -> invalid residual", + "residual_norm_l2 > epsilon_mech -> replan or repair", + "density command used on real printer without slicer/material calibration -> unsafe", + ], + } + receipt["receipt_hash"] = sha256_text(stable_json(receipt)) + return receipt + + +def write_curriculum() -> None: + rows = [ + { + "task": "separate_mechanics_from_attestation", + "input": "load vectors, force densities, density commands, Merkle root", + "target": "mechanical residual first; Merkle commits to records only", + }, + { + "task": "solve_supported_lattice_equilibrium", + "input": "nodes, edges, support nodes, external loads", + "target": "signed edge force densities, support reactions, residual norm", + }, + { + "task": "reject_hidden_print_risk", + "input": "bounded sigmoid density command", + "target": "heuristic print-density command requiring slicer/material calibration", + }, + ] + CURRICULUM.write_text( + "".join(json.dumps(row, sort_keys=True) + "\n" for row in rows), + encoding="utf-8", + ) + + +def parse_args() -> argparse.Namespace: + parser = argparse.ArgumentParser() + parser.add_argument("--seed", type=int, default=2519138123) + parser.add_argument("--gravity", type=float, default=-9.81) + parser.add_argument("--mass-per-node", type=float, default=0.1) + parser.add_argument("--lateral-noise-sigma", type=float, default=0.05) + parser.add_argument("--duality-coefficient", type=float, default=2 ** 0.5) + parser.add_argument("--density-midpoint", type=float, default=0.25) + parser.add_argument("--epsilon-mech", type=float, default=1e-8) + parser.add_argument("--no-face-diagonals", action="store_false", dest="include_face_diagonals") + parser.set_defaults(include_face_diagonals=True) + return parser.parse_args() + + +def main() -> None: + args = parse_args() + receipt = build_receipt(args) + OUT.write_text(json.dumps(receipt, indent=2, sort_keys=True) + "\n", encoding="utf-8") + write_curriculum() + print(json.dumps({ + "receipt": str(OUT.relative_to(REPO)), + "curriculum": str(CURRICULUM.relative_to(REPO)), + "receipt_hash": receipt["receipt_hash"], + "merkle_root": receipt["merkle"]["root"], + "node_count": receipt["lattice"]["node_count"], + "edge_count": receipt["lattice"]["edge_count"], + "residual_norm_l2": receipt["results"]["residual_norm_l2"], + "mechanically_acceptable": receipt["results"]["mechanically_acceptable"], + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()