orientedSub
plain-language theorem explainer
orientedSub defines the oriented ledger combiner as ordinary subtraction on the real line. Workers constructing the oriented compiler gate that recovers the EML form cite it to retain additive structure before J-symmetrization. The definition proceeds by direct one-line assignment of a minus b.
Claim. The oriented ledger combiner before reciprocal symmetrization is given by $a - b$ for $a, b ∈ ℝ$.
background
The module formalizes the RS/EML bridge from oriented recognition coordinates. It states that the reciprocal cost J satisfies J(x) = J(x^{-1}) and therefore forgets orientation. The compiler-layer claim is that before reciprocal quotienting an oriented ledger has an additive log coordinate, the ratio charts are exp and log, the combiner is subtraction, and the induced gate is eml(x, y) = exp(x) - log(y). After symmetrization the same data yields J(exp u) = cosh u - 1.
proof idea
The definition is introduced directly as the difference a - b.
why it matters
This definition supplies the combiner used by orientedCompilerGate to produce the oriented EML gate. It realizes the pre-symmetrization step in the module's compiler-layer claim. The construction connects to the Recognition Science forcing chain at the point where orientation is retained before J-uniqueness (T5) is imposed. The downstream declaration states that the induced gate is exactly EML.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.