flat_zero_cost
plain-language theorem explainer
Flat spacetime, represented by the unit scale factor, carries zero J-cost. Workers on the discrete-to-continuum limit cite this to fix the vacuum baseline before deriving the Einstein equations from J-cost stationarity. The proof is a one-line term that invokes the unit lemma for the cost function.
Claim. $J(1)=0$, where $J(x)=(x-1)^2/(2x)$ is the cost function on positive reals.
background
The module establishes that J-cost on a simplicial ledger equals the Regge action up to the factor 8 phi^5, so that stationarity of J-cost reproduces the Regge equations and their continuum limit is the Einstein field equations. J-cost is defined via the Recognition Composition Law as J(x)=(x-1)^2/(2x), which expands to the quadratic form (delta epsilon)^2/2 in log coordinates. The upstream lemma Jcost_unit0 records the direct algebraic consequence that this expression vanishes at x=1.
proof idea
One-line wrapper that applies the lemma Jcost_unit0. That lemma is obtained by direct simplification of the definition J(x)=(x-1)^2/(2x) at the point x=1.
why it matters
The result supplies the flat_cost_zero field inside the continuum_bridge_cert theorem, which certifies the full chain from J-cost stationarity through the Regge action to the Einstein field equations. It therefore closes the zero-cost anchor required by the derivation chain stated in the module documentation, linking the T5 J-uniqueness property to the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.