Pith. sign in
module module high

IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCost

show as:
view Lean formalization →

Recognition cost of an ordered adjacency whose cells differ by d phi-rungs equals J(φ^d), with J the forced cost and φ the golden ratio. For the binary polarized birth field, monochromatic carried edges cost zero and each bichromatic interface edge costs J(φ). Cosmology ledgers cite the resulting interface and carried totals. The module defines the per-edge cost, proves the zero-carried and interface cases, and aggregates them from the lattice edge counts.

claimThe recognition cost of an ordered adjacency whose two cells differ by $d$ rungs on the $\varphi$-ladder is $J(\varphi^d)$, where $J(x)=(x+x^{-1})/2-1$ is the forced cost and $\varphi$ is the golden ratio. Same-charge (carried) edges cost $0$; opposite-charge interface edges cost $J(\varphi)$. The interface cost of a polarized birth field is the interface edge count times $J(\varphi)$; the carried cost is identically zero.

background

Recognition Science forces a unique nonnegative cost $J$ on positive reals (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. The self-similar fixed point of the forcing chain is the golden ratio $\varphi$ (T6). On the discrete $\varphi$-ladder, neighboring cells may sit at different rungs; the natural edge cost is then $J$ evaluated at the rung ratio $\varphi^d$.

The companion module on lattice ball edges splits the ordered adjacencies of the L1 ball into monochromatic (carried-internal) edges and bichromatic (forced-distinction) interface edges. In the polarized birth field the charge is $\mathrm{sign}(x)\in{+1,0,-1}$, so the interface is exactly the set of edges that cross a sign change. That module supplies closed counts: interface size $8t-4$ in 2D and $8t^2-8t+4$ in 3D, together with the total adjacency count, hence the carried remainder.

This module attaches the $J$-cost to that combinatorial split. It imports $J$ from Cost and $\varphi$ from Constants, then builds the per-edge and aggregate ledgers used by later graded-rung accounting.

proof idea

The module is definition-led with short algebraic lemmas. It introduces $J(\varphi^d)$ as the rung-difference cost, then records the elementary evaluations $J(\varphi^0)=0$, $J(\varphi^{\pm 1})=J(\varphi)$, and the absolute-value reduction when $|d|=1$. Positivity of $J(\varphi)$ is recorded once.

Edge cost is defined from the level difference of the two cells. Two specializations follow immediately: carried edges (difference zero) cost zero; pure interface edges (difference $\pm 1$ in the binary field) cost $J(\varphi)$. Interface and carried totals are the corresponding sums over the edge sets supplied by the lattice-ball count module: interface total equals count times $J(\varphi)$, carried total is identically zero.

why it matters in Recognition Science

This is Phase 55 of the cosmology ledger: the recognition-cost book for the binary polarized birth field. Downstream, GradedRungCost imports it and lifts the same law from a single sign flip to a multi-valued phi-rung profile. Its doc-comment states the north star explicitly: carry each region at the coarsest phi-rung its recognition allows, paying $J(\varphi)$ per forced unit-rung distinction.

The module therefore closes the cost side of the carried-versus-interface split already counted in LatticeBallEdges. It sits on the forced $J$ (T5) and $\varphi$ (T6), so the numerical factor on every interface edge is not free. Parent consumers that need a bulk-plus-boundary energy for birth or coarsening cite the interface and carried aggregates defined here before generalizing the charge from ${\pm 1,0}$ to arbitrary rung grades.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (22)