gapCost
plain-language theorem explainer
The gap cost for a natural number k is the J-cost evaluated at the k-th power of the golden ratio, quantifying the interaction energy between phi-ladder rungs separated by k steps. Partition theorists and Recognition Science researchers would reference this when proving stability constraints for Rogers-Ramanujan identities. The definition is a direct composition of the Jcost function with phi exponentiation, requiring no additional lemmas.
Claim. For each natural number $k$, the gap cost is defined by $J(phi^k)$, where $J(x) = (x + x^{-1})/2 - 1$ denotes the recognition cost of the positive real ratio $x$ and $phi$ is the golden ratio.
background
The phi-ladder consists of discrete positions at powers of the golden ratio, with occupation patterns governed by minimization of J-cost. The J-cost function measures the recognition cost of a multiplicative ratio and is non-negative by upstream results from ObserverForcing. The module derives the differ-by-at-least-2 rule from the fact that gap-1 occupations incur positive cost and collapse via the identity phi^2 = phi + 1.
proof idea
The declaration is a one-line definition that substitutes the argument phi raised to k into the Jcost function. It relies on the prior definition of Jcost and the constant phi without invoking any further theorems.
why it matters
This definition supplies the cost measure used by the gap cost monotonicity and non-negativity theorems, which in turn support the Rogers-Ramanujan stability theorem establishing that partitions must differ by at least 2 to avoid positive J-cost. It implements the J-uniqueness step of the forcing chain by making the phi-ladder the unique stable configuration space. It leaves open the full derivation of the mod-5 congruence side of the identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.