totalCost
plain-language theorem explainer
Defines the total recognition cost of the polarized birth field at radius t as the sum of per-edge costs over every ordered adjacency. Cosmologists tracking the compute-watch law cite it: bulk monochromatic edges contribute nothing, so the sum collapses to interface count times J(φ). The body is a one-line Finset sum of the local edge cost.
Claim. For each natural number $t$, the total recognition cost is $\mathrm{totalCost}(t) := \sum_{p \in E(t)} J\bigl(\varphi^{q(p_1)-q(p_2)}\bigr)$, where $E(t)$ is the ordered adjacency set of the lattice ball of radius $t$ and $q$ is the polarized charge field taking values in $\{+1,0,-1\}$.
background
The module weights the Phase-54 edge-count ledger by the forced recognition cost $J(x)=(x+x^{-1})/2-1$ (unique by the Recognition Composition Law / functional equation). The polarized birth field assigns each lattice cell a charge $q\in{+1,0,-1}$. Across an ordered adjacency the engine posts $J(\varphi^{\Delta q})$.
Upstream, $E(t)$ is the Finset of all ordered adjacencies of the diamond (or octahedron) ball of radius $t$. The local edgeCost is $J$ at the phi-rung gap between the two endpoints' charges. Carried (monochromatic) edges have equal charges, so $\Delta q=0$ and $J(\varphi^0)=J(1)=0$. Interface (bichromatic) edges span exactly one rung and cost $J(\varphi)>0$.
Spatial dimension is the forced $D=3$ from the forcing chain, though the same cost construction is written for the 2D diamond and 3D octahedron cases treated in the module.
proof idea
Pure definition: a noncomputable real-valued Finset sum. No tactics. It folds the already-defined per-adjacency cost over the full ordered edge set $E(t)$. Downstream identities that evaluate the sum (interface count times $J(\varphi)$, carried contribution zero) are separate theorems; this declaration only names the aggregate.
why it matters
This is the cost-unit statement of the north-star compute-watch law: recognition cost scales with the codimension-1 interface, not with bulk volume. The module doc records the closed forms once the sum is evaluated: 2D diamond $\mathrm{totalCost}(t)=(8t-4)\cdot J(\varphi)$, 3D octahedron $\mathrm{totalCost}(t)=(8t^2-8t+4)\cdot J(\varphi)$, with carried cost identically zero. $J(\varphi)=(\sqrt{5}-2)/2>0$ is a genuine positive unit cost. It sits on the T5 J-uniqueness and T6 $\varphi$-fixed-point landmarks and turns the combinatorial interface/carried split into a literal recognition ledger. No downstream dependents are wired yet in the graph; the definition is the named aggregate those evaluations act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.