totalCost_mul
plain-language theorem explainer
For radius t ≥ 1, the total recognition cost of the polarized 2D diamond equals (8t − 4) times J(φ) as a real product. Cosmology proofs that need ordinary real arithmetic (differences, growth rates) cite this form rather than the nsmul statement. The proof is a one-line rewrite of totalCost_card through nsmul_eq_mul.
Claim. For every natural number $t \ge 1$, the total recognition cost of the polarized diamond field of radius $t$ equals $(8t - 4) \cdot J(\varphi)$, where $J(x) = (x + x^{-1})/2 - 1$ and $\varphi$ is the golden ratio.
background
The module weights the polarized-birth edge ledger by the Recognition Science cost $J(x) = (x + x^{-1})/2 - 1$. Carried (monochromatic) edges span zero phi-rungs and cost $J(1) = 0$; interface (bichromatic) edges span exactly one rung and cost $J(\varphi)$. Thus the whole field cost is the interface count times $J(\varphi)$.
For the 2D diamond, that count is $8t - 4$ when $t \ge 1$. The sibling theorem totalCost_card already states the cost as the natural multiple $(8t - 4) \bullet J(\varphi)$. Downstream arithmetic over $\mathbb{R}$ prefers ordinary multiplication, which is what this declaration supplies.
$J$ is the unique cost forced by the Recognition Composition Law (T5); $\varphi$ is the self-similar fixed point (T6). Positivity $J(\varphi) > 0$ is recorded separately in the module.
proof idea
One-line wrapper. Rewrite with totalCost_card t ht, which gives totalCost t = (8*t - 4) • J(φ), then apply nsmul_eq_mul to turn the natural scalar multiple into real multiplication ((8*t - 4 : ℕ) : ℝ) * J(φ).
why it matters
This is the real-arithmetic face of the 2D compute-watch law: recognition cost scales with the codimension-1 interface, not bulk volume. Parent theorems costIncrement and runCost_growth both open by rewriting through this form.
costIncrement extracts the constant per-cycle bill $8 \cdot J(\varphi)$ (differential compute-watch). runCost_growth integrates from radius 1 to $T$ to get $8(T-1) \cdot J(\varphi)$, i.e. $\Theta(T)$ growth against brute-force $\Theta(T^3)$ volume-times-ticks. Both need subtraction and casting over $\mathbb{R}$, so the nsmul statement alone is awkward.
In the broader RS chain this is the cost-unit reading of interface-only activity on the eight-tick octave geometry, with $J$ from T5 and $\varphi$ from T6. The 3D octahedron analogue $(8t^2 - 8t + 4) \cdot J(\varphi)$ lives beside it in the same module narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.