coherence_cost_aperiodicity
plain-language theorem explainer
The theorem shows that the J-cost evaluated at the golden ratio equals φ minus 3/2. This supplies the explicit minimal positive cost for any non-trivial aperiodic occupation on the φ-ladder and grounds the differ-by-at-least-two rule in the Rogers-Ramanujan identities. Number theorists or physicists working on aperiodic order and Penrose tilings would cite the equality to justify the J-cost admissibility constraint. The short tactic proof derives the reciprocal identity φ^{-1} = φ - 1 from the quadratic equation φ² = φ + 1 and substitutes into
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. Then $J(φ) = φ - 3/2$, where $φ = (1 + √5)/2$ satisfies $φ² = φ + 1$.
background
J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ that assigns an interaction energy to any ratio of occupied rungs on the φ-ladder. The module shows that adjacent rungs at ratio φ produce positive cost $J(φ) > 0$, which collapses under the golden recurrence and forces the minimal stable gap of two. Upstream lemmas supply the two algebraic facts needed: φ ≠ 0 and φ² = φ + 1. The local setting is the φ-ladder stability analysis that converts the classical Rogers-Ramanujan “differ by ≥ 2” rule into a J-cost minimum.
proof idea
The tactic proof first imports φ ≠ 0 and φ² = φ + 1. It multiplies the quadratic by the reciprocal to obtain φ^{-1} = φ - 1. It then unfolds the definition of Jcost, rewrites the inverse term, and finishes with ring simplification.
why it matters
The equality gives the concrete numerical value of the minimal aperiodic cost that enforces the non-adjacent occupation rule on the φ-ladder, directly supporting the RS reading of the Rogers-Ramanujan identities. It sits inside the T5–T6 segment of the forcing chain where J-uniqueness and the self-similar fixed point are established. No downstream theorems are recorded, so the result remains an isolated algebraic anchor whose extension to composite ladders or to the physical constants remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.