reciprocal_cost_forgets_orientation
plain-language theorem explainer
The theorem shows that the log-domain cost Jlog is even, so its value at any real u equals its value at -u. Workers formalizing the EML compiler gate from oriented recognition coordinates cite this to confirm that reciprocal symmetrization erases directional information. The proof is a one-line wrapper that applies the Jcost symmetry lemma to the positive argument exp u and simplifies via the definition of Jlog.
Claim. $Jlog(u) = Jlog(-u)$ for every real number $u$.
background
The module formalizes the honest RS/EML bridge from oriented recognition coordinates. Before reciprocal quotienting an oriented ledger carries an additive log coordinate whose maps are exp and log and whose combiner is subtraction; after symmetrization the induced cost becomes even. Jlog is the composition Jcost ∘ exp, where Jcost is the base cost function. The upstream lemma Jcost_symm states that Jcost x = Jcost x^{-1} whenever x > 0.
proof idea
The proof is a one-line wrapper. It invokes Jcost_symm on the positive real exp u to obtain Jcost (exp u) = Jcost (exp u)^{-1}. Simpa then rewrites using the definition Jlog t := Jcost (exp t) together with exp (-u) = (exp u)^{-1} to reach Jlog u = Jlog (-u).
why it matters
This theorem supplies the reciprocal_cost_quotient field inside the emlFromRecognitionCert definition, which certifies that the EML compiler gate follows from oriented exp/log recognition data. The module documentation notes that reciprocal quotienting forgets orientation, yielding J(exp u) = cosh u - 1. In the Recognition Science framework the result closes the step from oriented ledger to the symmetric J-cost appearing in the phi-ladder and eight-tick octave constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.