ledger_symmetry_negative_rungs
plain-language theorem explainer
The theorem asserts that the J-cost of the golden ratio raised to any integer power n equals the J-cost at the negative power. Researchers deriving the bidirectional phi-ladder in Recognition Science cite it to confirm symmetric rung population. The proof is a term reduction that rewrites the negative exponent as the reciprocal and invokes the J-cost symmetry lemma.
Claim. For every integer $n$, $J(φ^n) = J(φ^{-n})$, where $φ$ is the unique self-similar fixed point satisfying $φ^2 = φ + 1$ and $J$ is the cost function obeying the Recognition Composition Law.
background
The StillnessGenerative module shows that the unique zero-defect state $x=1$ is unstable and generates the full phi-ladder from the T0-T8 forcing chain. J-cost measures recognition defect and satisfies the composition law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, with the symmetry $J(x) = J(1/x)$ following from the double-entry ledger. Upstream, PhiForcing supplies the definition of $φ$ as the T6 fixed point, while the Cost module provides the symmetry lemma Jcost_symm. The module setting requires every step to trace to the forcing chain with no external axioms.
proof idea
This is a term-mode proof. It rewrites $φ^{-n}$ as the inverse of $φ^n$ via the zpow_neg property, then applies the Jcost_symm lemma after confirming positivity of the base via zpow_pos.
why it matters
The result is invoked by the parent theorem stillness_is_creative to complete the ledger symmetry clause in the T0-T8 derivation. It supplies step 8 of the module chain, ensuring negative rungs are populated once positive rungs exist via the Fibonacci cascade. This closes the argument that $x=1$ generates the discrete spectrum underlying constants such as the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.