proof(lean): close e8_singer_improvement and erdos30_e8_conditional; restate two invalid sorries

- 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 <noreply@anthropic.com>

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 : ℕ)) |>
+    (A ×ˢ A |>.filter (fun p => p.1 ≤ p.2)).sum (fun p => sigma3 p.1 * sigma3 p.2) ≤
-      fun sums => sums.sum fun s => sigma3 s) ≤
     sigma7 (2 * N) / e8PositiveRoots := by
-  -- Each pair sum s contributes σ₃(s) to the total weight
+  -- ANALYTIC_OPEN: each Sidon pair (a,b) contributes σ₃(a)·σ₃(b) ≤ term in conv at a+b.
-  -- By the convolution identity, the total weight is bounded by σ₇(2N)/120
+  -- 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
+CORRECTED STATEMENT: T = N^4 ensures σ₃(n) ≤ n · n³ = n^4 ≤ N^4 for all n ≤ N
-depending on T. This follows from the fact that σ₃ is a multiplicative function
+(since σ₃(n) = ∑_{d|n} d³ ≤ |divisors n| · n³ ≤ n · n³), so E8LevelSet (N^4) N = [1,N]
-with σ₃(p) = 1 + p³, and the set {n : σ₃(n) ≤ T} includes all n whose prime
+and its cardinality is N ≥ N / (Nat.log 2 N)^2.
-factors are ≤ T^{1/3} (since σ₃(p) = 1+p³ ≤ T requires p ≤ (T-1)^{1/3}).
 
-The density of such "smooth" numbers is given by the Dickman function ρ(u)
+The analytically interesting density (T growing slowly, e.g. T = N^ε for small ε > 0)
-where u = log N / log T^{1/3}.
+is ANALYTIC_OPEN: requires Dickman function ρ(u) with u = log N / (ε/3 · log N) = 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)²
 -/
-theorem e8_levelset_density (T N : ℕ) (hT : 9 ≤ T) (hN : 100 ≤ N) :
+theorem e8_levelset_density (N : ℕ) (hN : 100 ≤ N) :
-    (E8LevelSet T N).card ≥ N / (Nat.log N) ^ 2 := by
+    (E8LevelSet (N ^ 4) N).card ≥ N / (Nat.log 2 N) ^ 2 := by
-  -- Requires smooth number density estimates (Dickman function)
+  -- ANALYTIC_OPEN (but easier than original): σ₃(n) ≤ n^4 ≤ N^4 for n ≤ N,
-  -- Not yet formalizable without analytic number theory in Mathlib
+  -- 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
+  -- The Singer set satisfies the bound: (p+1)·(119/120)^k ≤ p+1 since (119/120)^k ≤ 1.
-  -- TODO(lean-port): Formalize the E₈ lift procedure
+  obtain ⟨S, hSidon, hrange, hcard⟩ := singer_interval_sidon p N hp hbound
-  -- Requires: E₈ lattice quotient construction, Sidon preservation under lift
+  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

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()