runCost_growth
plain-language theorem explainer
The run-total recognition cost of growing a 2D polarized diamond from radius 1 to T equals exactly 8(T-1) J(φ). Cosmologists citing the compute-watch law use this as the integrated cost identity: growth is Θ(T), not volume-times-ticks Θ(T³). The proof rewrites both endpoints by the closed form totalCost t=(8t-4)J(φ) and simplifies the real difference by ring arithmetic.
Claim. For every natural number $T\ge 1$, the difference of total recognition costs on the 2D polarized diamond satisfies $\mathrm{totalCost}(T)-\mathrm{totalCost}(1)=8(T-1)\,J(\varphi)$, where $J(x)=(x+x^{-1})/2-1$ is the unique recognition cost and $\varphi$ is the golden-ratio fixed point.
background
In the polarized birth field each lattice adjacency is either monochromatic (carried) or bichromatic (interface). Carried edges span zero phi-rungs, so they cost $J(1)=0$. Interface edges join the spine charge $0$ to a neighbour at $\pm 1$, span one rung, and cost exactly $J(\varphi)$ by reciprocal symmetry of $J$. The whole recognition cost of the field is therefore the interface edge count times $J(\varphi)$.
For the 2D diamond the closed form is $\mathrm{totalCost}(t)=(8t-4)J(\varphi)$, with carried cost identically zero. The module weights the Phase-54 edge-count ledger by the forced cost $J$, unique from the recognition functional equation. This is the cost-unit statement of the compute-watch law: cost tracks the codimension-1 interface, not the bulk volume the engine carries for free.
proof idea
Rewrite both sides with the closed-form identity totalCost_mul: totalCost $T=(8T-4)J(\varphi)$ and totalCost $1=4J(\varphi)$. The hypotheses $T\ge 1$ give the Nat inequalities $4\le 8T$ and $8\le 8T$ needed to cast the subtractions $8T-4$ and $8T-8$ into $\mathbb{R}$. After those cast equalities, a single ring simplification yields the difference $8(T-1)J(\varphi)$.
why it matters
This is the integrated form of the compute-watch law for the 2D diamond: the engine posts $\Theta(T)$ recognition cost to grow the world from radius 1 to $T$, strictly sub-extensive against brute-force volume-times-ticks $\Theta(T^3)$. It rests on the interface-cost factorization (carried bulk free, interface paid at $J(\varphi)$) and on the closed form totalCost $t=(8t-4)J(\varphi)$. The differential sibling is the constant per-cycle increment $8J(\varphi)$ for $t\ge 1$. No downstream dependents are recorded yet; the result closes the run-total cost identity inside PolarizedBirthInterfaceCost. Framework landmarks in play: J-uniqueness (T5) and $\varphi$ as the self-similar fixed point (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.