orientedCompilerGate
The oriented compiler gate maps a pair of reals to the difference of the exponential of the first argument and the logarithm of the second. Researchers tracing the Recognition Science derivation of the EML operation cite this definition when establishing the compiler-layer equivalence prior to reciprocal symmetrization. The definition is realized as the direct composition of the exponentiation map, the logarithm map, and subtraction.
claimDefine the oriented compiler gate $G:ℝ×ℝ→ℝ$ by $G(x,y)=e^x - log y$.
background
The module on EML from Oriented Recognition Coordinates states that before reciprocal symmetrization an oriented recognition ledger carries an additive log coordinate. The maps between additive coordinates and positive ratios are exponentiation and its inverse logarithm. The oriented ledger combiner is ordinary subtraction, so the induced two-input compiler gate is eml(x,y)=exp(x)-log(y). After symmetrization the same data recovers the J-cost as cosh(u)-1. The upstream definitions supply the lift from additive coordinate to ratio via exponentiation, the projection from ratio to additive coordinate via logarithm, and the combiner as subtraction.
proof idea
This definition is a one-line wrapper that composes the oriented ratio lift, the oriented ratio projection, and the oriented subtraction.
why it matters in Recognition Science
This definition supplies the compiler gate shown equal to the EML operation in the theorem oriented_compiler_gate_eq_eml. It forms part of the compact certificate EMLFromRecognitionCert for the RS/EML bridge. The construction fills the compiler-layer claim that the induced gate before reciprocal quotienting is exp x - log y. It connects to the Recognition Science landmarks by preserving orientation prior to the J-uniqueness step that symmetrizes to the cosh form.
scope and limits
- Does not derive the EML gate from the reciprocal cost J alone.
- Does not address the full symmetrized case after reciprocal quotienting.
- Does not claim equivalence outside the oriented ledger setting.
formal statement (Lean)
50def orientedCompilerGate (x y : ℝ) : ℝ :=
proof body
Definition body.
51 orientedSub (orientedToRatio x) (orientedFromRatio y)
52
53/-- The induced oriented compiler gate is exactly EML. -/