orientedCompilerGate
plain-language theorem explainer
orientedCompilerGate composes exponentiation on the first input, logarithm on the second, and subtraction to realize the EML gate from oriented ledger coordinates. Researchers establishing the Recognition Science to EML bridge at the compiler layer cite this definition when separating the oriented case from reciprocal symmetrization. The definition is a direct one-line composition of the three oriented primitives.
Claim. Define the oriented compiler gate by $g(x,y) := e^x - y$ for $x,y$ real, where the first argument is lifted by exponentiation and the second is projected by logarithm before subtraction.
background
The module formalizes the RS/EML bridge at the compiler layer. Before reciprocal quotienting, an oriented recognition ledger carries an additive log coordinate; the ratio maps are exponentiation and logarithm; the combiner is subtraction. This yields the gate $eml(x,y) = e^x - y$ (distinct from the symmetrized $J$ that forgets orientation). Upstream definitions supply the three primitives: orientedToRatio lifts additive coordinates to positive ratios via $e^u$, orientedFromRatio recovers the additive coordinate via logarithm, and orientedSub performs the oriented ledger combination by subtraction.
proof idea
One-line wrapper that applies the oriented ratio maps followed by subtraction.
why it matters
The definition supplies the left-hand side of the equality proved in oriented_compiler_gate_eq_eml and is required by the certificate structure EMLFromRecognitionCert. It fills the compiler-layer claim stated in the module doc-comment: the induced two-input gate is exactly eml before any reciprocal symmetrization. The construction sits inside the larger Recognition Science program that derives physics from the forcing chain and the Recognition Composition Law, separating the oriented exp/log stage from the later J-cost symmetrization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.