J_symmetric
plain-language theorem explainer
J(x) equals J(1/x) for every positive real x. Ledger forcing derivations cite this symmetry to obtain reciprocity between events and their reciprocals, which in turn forces balanced double-entry structure. The term proof substitutes the explicit formula for J, records that positivity rules out zero, then reduces the identity by field simplification and ring arithmetic.
Claim. $J(x) = J(x^{-1})$ for all real $x > 0$, where the cost functional is $J(y) := (y + y^{-1})/2 - 1$.
background
The CostAxioms module encodes the three primitive axioms from which Recognition Science derives all structure: normalization J(1) = 0, the recognition composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), and calibration of the second logarithmic derivative at zero. J is the unique solution to these axioms, given explicitly by J(x) = (x + x^{-1})/2 - 1. This symmetry is the immediate first consequence after uniqueness (T5 in the forcing chain).
proof idea
The proof is a one-line term wrapper. It first obtains x ≠ 0 from the positivity hypothesis, unfolds the definition of J, applies field_simp to clear the inverse, and closes with ring to confirm the algebraic identity.
why it matters
This supplies the symmetry step inside the ledger forcing principle, which concludes that recognition events appear in reciprocal pairs and therefore require balanced ledgers of zero net cost. It is invoked directly by reciprocity, by the cost-to-recognition bridge, and by the Higgs mechanism section. In the overall chain it closes the first derived property after J-uniqueness, enabling the eight-tick octave and the forcing of D = 3 that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.