Jpow_neg_one
plain-language theorem explainer
A one-rung-down charge gap on the phi ladder costs exactly J(φ), matching the upward gap by reciprocal symmetry of the recognition cost. Cosmology proofs that weight polarized-birth interface edges cite this to collapse the −1 case onto the same positive unit cost as +1. The argument rewrites the integer power as an inverse and applies J-cost symmetry at φ > 0.
Claim. The recognition cost of a charge difference of $-1$ phi-rungs equals the cost of the golden ratio: $J(\varphi^{-1}) = J(\varphi)$, where $J(x) = (x + x^{-1})/2 - 1$ and $\varphi$ is the forced golden ratio.
background
This module weights the polarized-birth edge ledger by recognition cost. After LatticeBallEdges splits every adjacency into carried (monochromatic) versus interface (bichromatic) edges, the cost posted on an ordered adjacency whose charges differ by $d$ integer rungs is $J(\varphi^d)$. Here $J$ is the unique RS cost $J(x) = (x + x^{-1})/2 - 1$ and $\varphi$ is the golden ratio forced as the self-similar fixed point.
The local definition packages that evaluation as a map on integer rung gaps. A zero gap costs nothing ($J(1) = 0$), so carried bulk is free. An interface edge of the polarized field has charges differing by exactly $\pm 1$, so the remaining algebraic fact is that both signs cost the same positive amount $J(\varphi)$.
Reciprocal symmetry of $J$ is the upstream engine: $J(x^{-1}) = J(x)$ for $x > 0$. Combined with $\varphi > 0$, it identifies the down-rung evaluation with the up-rung one.
proof idea
Short tactic proof. First prove $\varphi^{(-1:\mathbb{Z})} = \varphi^{-1}$ by rewriting with the integer-power rules for negation and the unit exponent. Unfold the rung-gap cost definition, substitute that identity, then rewrite with the reciprocal symmetry lemma for $J$ at the positive golden ratio (direction flipped so the goal becomes $J(\varphi^{-1}) = J(\varphi)$).
why it matters
This is the down-rung half of the interface unit cost. Its sole direct consumer is the case-split lemma that any absolute one-rung gap costs exactly $J(\varphi)$: that parent discharges the $+1$ case by the companion up-rung identity and the $-1$ case by this result.
With both signs identified, every forced bichromatic edge of the polarized birth field posts the same positive cost $J(\varphi) = (\sqrt{5}-2)/2 > 0$. The module then multiplies by the interface count to obtain the full recognition cost of 2D diamonds and 3D octahedra, with carried bulk contributing zero. That is the cost-unit form of the compute-watch law: cost tracks the codimension-1 interface, not bulk volume.
Framework landmarks in play are T5 (J uniqueness via the recognition composition law) and T6 ($\varphi$ as the self-similar fixed point). No scaffolding remains; the lemma is fully proved over $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.