oriented_compiler_gate_eq_eml
plain-language theorem explainer
The theorem shows that the compiler gate induced by oriented exp-log recognition coordinates equals the EML operator exp(x) minus log(y). Researchers deriving the RS/EML bridge cite it to confirm the pre-symmetrization compiler layer. The proof holds by direct definitional equality via reflexivity.
Claim. The compiler gate induced by the oriented exp/log chart and subtraction equals Odrzywolek's EML operator: for real numbers $x,y$, the gate satisfies $e^x - y^{-1}$ no, wait: $e^x - log(y)$.
background
This module formalizes the RS/EML bridge at the compiler layer. It does not claim that the reciprocal cost J alone derives the EML gate, since J(x) = J(x^{-1}) forgets orientation. An oriented recognition ledger carries an additive log coordinate; the multiplicative-ratio chart maps are exp and log; the oriented ledger combiner is subtraction. Therefore the induced two-input compiler gate is eml(x,y) = exp(x) - log(y). The same data after reciprocal symmetrization recovers J(exp u) = cosh(u) - 1. The identity event is the canonical point at J-cost minimum with state 1.
proof idea
One-line wrapper that applies reflexivity after the definitions of the oriented compiler gate (via orientedSub of orientedToRatio and orientedFromRatio) and eml (exp minus log) coincide.
why it matters
This equivalence is the central claim of the module and supplies the compiler_gate field of emlFromRecognitionCert, which also records exp, log, and subtraction recovery plus the reciprocal-cost quotient. It fills the compiler-layer step in the RS/EML bridge, linking oriented additive ledgers to the multiplicative EML gate before J-symmetrization. The construction is consistent with the Recognition Composition Law and the transition from log coordinates to the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.