eml_recovers_exp
plain-language theorem explainer
The declaration shows that the EML operator applied to any real x and the terminal 1 recovers the exponential function exp(x). Researchers verifying the oriented exp-log bridge in Recognition Science would cite this step when assembling the compiler-gate certification. The proof is a one-line simplification that unfolds the eml definition and cancels the log of 1.
Claim. For every real number $x$, the EML operator satisfies $eml(x,1)=e^x$.
background
The module formalizes the compiler-layer bridge from oriented recognition coordinates to the EML gate. The gate is defined by eml x y := exp x - log y, where oriented additive ledger coordinates lift to positive ratios via exponentiation. This rests on the PrimitiveDistinction theorem, which extracts four structural conditions plus three definitional facts from seven independent axioms. The constant scalar field supplies the terminal value 1 used in the recovery. The local setting is the claim that, before reciprocal quotienting, the oriented ledger possesses an additive log coordinate whose multiplicative-ratio charts are precisely exp and log.
proof idea
The proof is a one-line wrapper that applies the definition of eml. Unfolding eml x 1 yields exp x - log 1. The logarithm of the identity terminal is zero, so the expression reduces directly to exp x.
why it matters
This result supplies the exp_recovery field inside the emlFromRecognitionCert definition, which certifies that the EML compiler gate follows from oriented exp/log recognition data. It fills the compiler-layer claim stated in the module documentation and connects to the Recognition Science framework's oriented ledger before J-cost symmetrization. The same exp/log data later yields J(exp u) = cosh u - 1 after reciprocal symmetrization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.