t55_cost_ledger
plain-language theorem explainer
For a polarized 2D diamond of radius t ≥ 1, monochromatic bulk edges cost exactly zero recognition, total cost equals (8t−4)·J(φ) and coincides with the interface cost alone, and J(φ) > 0. Cosmologists tracking the Phase-55 coarsening ledger cite this as the exact cost-unit form of “carry bulk free, pay only the interface.” The proof is a four-conjunct constructor assembling prior zero-carried, card, interface-equality, and positivity lemmas.
Claim. For every natural number $t \ge 1$, the carried bulk cost of the polarized diamond of radius $t$ is zero, the total recognition cost equals $(8t-4)\cdot J(\varphi)$, the total cost equals the interface cost, and $J(\varphi)>0$.
background
Phase 54 (LatticeBallEdges) closed the edge-count ledger on the polarized birth field: every adjacency is either a monochromatic carried edge or a bichromatic interface edge, with exact counts on each side. This module weights that ledger by the recognition cost $J(x)=(x+x^{-1})/2-1$ (Cost.Jcost, unique by the functional equation), evaluated at the phi-rung gap between the two cells’ charges.
Charge on the polarized diamond is $\mathrm{sign}(x)\in{+1,0,-1}$. A carried edge has equal charges, spans zero rungs, and costs $J(\varphi^0)=J(1)=0$. An interface edge joins the spine $x=0$ to a neighbour at $x=\pm 1$, so the charges differ by exactly $\pm 1$ and the edge costs $J(\varphi^{\pm 1})=J(\varphi)$ by reciprocal symmetry. Upstream, carriedCost_eq_zero already records that the same-rung bulk sums to zero, and Jcost_phi_pos gives $J(\varphi)>0$ from $\varphi\ne 1$.
The local setting is therefore the 2D diamond namespace: total cost is the sum of edge costs over all ordered adjacencies, interface cost is the same sum restricted to bichromatic edges, and the headline identity is that the two coincide and equal the interface cardinality times $J(\varphi)$.
proof idea
One-line And-constructor. The four conjuncts are discharged by four prior results: carriedCost_eq_zero t (every monochromatic edge has level gap 0, so $J(\varphi^0)=0$ and the bulk sum vanishes), totalCost_card t ht (total cost equals the interface edge count $(8t-4)$ times $J(\varphi)$, using $t\ge 1$), totalCost_eq_interfaceCost t (splitting the edge set into bichromatic and monochromatic parts, the monochromatic sum is zero), and Jcost_phi_pos (positivity of $J(\varphi)$ from $\varphi>0$ and $\varphi\ne 1$). No new algebra is performed at this site.
why it matters
This is the Phase-55 2D headline: the literal cost-unit statement of the compute-watch law that recognition cost scales with the codimension-1 interface, not with bulk volume. It sits on the T5 J-uniqueness fixed point $J(x)=(x+x^{-1})/2-1$ and the T6 self-similar scale $\varphi$, with the one-rung gap forced by the polarized charge geometry. The same module immediately runs the 3D octahedron analogue (total cost $(8t^2-8t+4)\cdot J(\varphi)$, carried cost still zero), so the diamond ledger is the planar base case of the coarsening cost story. No downstream consumers are wired yet; the declaration is the citation target for any later argument that needs “bulk free, interface paid” in exact $J(\varphi)$ units on the 2D birth diamond.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.