JCostStable
plain-language theorem explainer
JCostStable defines the property that a list of occupied rungs on the phi-ladder has no two indices differing by exactly 1. Researchers connecting Zeckendorf representations to Recognition Science cost analysis cite this definition when translating the classical non-consecutive condition. The definition is introduced directly as the Prop that encodes minimum gap 2 between any pair of distinct elements.
Claim. A list of natural numbers $occupied$ is J-cost stable if for all $i, j$ in the list with $i ≠ j$, $|i - j| ≥ 2$.
background
The module interprets Zeckendorf representations as partitions on the phi-ladder where stability is measured by J-cost. Zeckendorf's theorem asserts every positive integer equals a unique sum of non-consecutive Fibonacci numbers; the module recasts the gap ≥ 2 requirement as the absence of adjacent rung occupations, since consecutive Fibonacci numbers satisfy the collapse identity that raises total J-cost. Upstream results supply the cost primitives: in MultiplicativeRecognizerL4 the cost of a recognizer is its derivedCost on positive ratios, while in ObserverForcing the cost of any recognition event is the Jcost of its state.
proof idea
The declaration is a definition whose body is the direct universal statement that every pair of distinct indices in the list satisfies absolute difference at least 2. No lemmas are applied; the body simply transcribes the non-adjacency condition into a Prop.
why it matters
JCostStable is invoked by the downstream theorem zeckendorf_is_Jcost_stable, which establishes that every Zeckendorf representation satisfies the stability predicate. The definition therefore supplies the precise link between the 1939 Zeckendorf theorem and the Recognition Science phi-ladder analysis, including the J-uniqueness fixed point and the eight-tick octave structure. It closes one step in the chain that equates classical integer partitions with admissible J-cost configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.