eml
plain-language theorem explainer
The eml definition supplies Odrzywolek's EML operator as the oriented exp-log compiler gate. Researchers formalizing the Recognition Science to EML bridge cite this gate when recovering exponentiation, logarithm, and oriented subtraction from an additive ledger coordinate. It is introduced by a direct one-line definition that subtracts the logarithm of the second argument from the exponential of the first.
Claim. The oriented compiler gate is defined by $EML(x,y) := e^x - log(y)$ for real numbers $x,y$.
background
The EMLFromRecognition module formalizes the RS/EML bridge at the compiler layer. An oriented recognition ledger carries an additive log coordinate before reciprocal quotienting. The multiplicative-ratio chart maps are exp and log, while the oriented ledger combiner is subtraction. This produces the two-input gate eml x y = exp x - log y. The module documentation states that the reciprocal cost J alone cannot derive the EML gate because J(x) = J(x^{-1}) forgets orientation; the same data after symmetrization yields J(exp u) = cosh u - 1.
proof idea
The definition is a direct one-line assignment of Real.exp x minus Real.log y.
why it matters
This definition supplies the core operator for the EMLFromRecognitionCert structure, which certifies the RS/EML bridge via compiler_gate, exp_recovery, and log_recovery axioms. It fills the compiler-layer claim in the module's formalization of the honest RS/EML bridge. Downstream results such as eml_recovers_exp and eml_recovers_log recover the exponential and logarithmic functions directly from the gate, while eml_keeps_oriented_channels shows that forward and reverse channels remain separately addressable. The construction preserves orientation before the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.