Pith. sign in
module module high

IndisputableMonolith.Cosmology.GradedRungCost

show as:
view Lean formalization →

Weights each polarized-birth adjacency by the forced recognition cost J at the phi-rung gap between the two cells. Under the unit-step invariant (adjacent rungs differ by at most one), carried monochromatic edges cost zero and the total ledger collapses onto the interface edge count. Cosmology developments that meter recognition cost under minimal distinction cite this Phase-56 module. The argument is definitional plus short algebraic identities for J on gaps in {0, ±1}.

claimFor a phi-rung field $k$ and ordered adjacency $(p_1,p_2)$, edge cost is $J(\varphi^{k(p_1)-k(p_2)})$ with $J(x)=(x+x^{-1})/2-1$. Unit-step requires $|k(p_1)-k(p_2)|\le 1$ on every edge of $E$. Then carried (monochromatic) cost is zero, total cost equals interface cost, and both equal the interface edge cardinality (graded cost ledger).

background

Recognition Science posts the T5-unique cost $J(x)=(x+x^{-1})/2-1$ at every distinction. In polarized birth, the upstream module closed an unweighted edge ledger: every adjacency is either a carried monochromatic edge or a forced bichromatic interface edge, with exact partition total = interface + carried.

This module lifts that count ledger to a cost ledger by evaluating $J$ at the phi-rung gap $\varphi^{k(u)-k(v)}$ between integer charges on the two cells. The minimal-distinction invariant UnitStep forces adjacent rungs to differ by at most one, so admissible gaps are only $0,\pm 1$. Gap zero gives $J(1)=0$; nonzero unit gaps give the constant unit-step cost.

Upstream PolarizedBirthInterfaceCost supplies the combinatorial carried/interface split that is weighted here.

proof idea

Definitions introduce edgeCost on a single ordered adjacency, then interfaceCost, carriedCost, and totalCost by summing over the polarized edge partition from the upstream ledger. Under UnitStep, carried edges have rung gap zero, so $J(\varphi^0)=J(1)=0$ and carriedCost vanishes. Hence totalCost equals interfaceCost. Further lemmas identify interface and total cost with interface edge cardinality (the graded cost ledger, t56). Structure is definitional scaffolding plus short algebraic rewrites from $J$ and the gap restriction; no deep analysis.

why it matters in Recognition Science

Phase 56 of the cosmology stack: it is the bridge from the unweighted coarsening ledger to a J-weighted cost meter on the phi ladder. Downstream RecognitionUnitStepPreservation (Phase 58) takes the graded-rung cost law as the runtime cost meter that active mean-move dynamics must respect, then records the honest negative fact that blind global preservation of UnitStep by pairResolve is false. RungDescentUnitStep is the positive complement: integer-rung descent does preserve UnitStep, and it depends on the same cost-law hypothesis. The module therefore pins where T5 $J$-uniqueness and the phi ladder enter interface accounting before dynamics and descent theorems.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (15)