emlFromRecognitionCert
plain-language theorem explainer
The definition assembles a compact certificate showing that the EML compiler gate is induced by oriented exp and log maps on the recognition ledger. Researchers studying the RS/EML bridge cite it to confirm the oriented channel before reciprocal symmetrization to J-cost. It is a direct record that populates the certificate fields from the gate equality and four recovery lemmas.
Claim. The structure asserts that the oriented compiler gate satisfies $∀x,y∈ℝ, orientedCompilerGate(x,y)=eml(x,y)$, that $eml(x,1)=exp(x)$, that a double-application loop recovers $log$, that $eml(log x, exp y)=x-y$ for $x>0$, and that the reciprocal cost is symmetric under sign flip of the log coordinate.
background
This module formalizes the honest RS/EML bridge. An oriented recognition ledger carries an additive log coordinate whose multiplicative-ratio charts are the maps exp and log; the oriented combiner is subtraction, so the induced gate is eml x y = exp x - log y. After reciprocal symmetrization the cost becomes J(exp u)=cosh u -1, which erases orientation because Jlog u = Jlog(-u). The certificate EMLFromRecognitionCert packages the compiler-gate equality together with the four recovery properties. Upstream results include the reflexivity theorem oriented_compiler_gate_eq_eml and the recovery theorems eml_recovers_exp, eml_recovers_log, eml_recovers_sub, and reciprocal_cost_forgets_orientation.
proof idea
The definition is a one-line wrapper that populates the EMLFromRecognitionCert structure by direct reference to oriented_compiler_gate_eq_eml for the gate field and to eml_recovers_exp, eml_recovers_log, eml_recovers_sub, and reciprocal_cost_forgets_orientation for the remaining fields.
why it matters
The certificate is invoked by the downstream theorem eml_from_recognition_cert_holds to establish Nonempty EMLFromRecognitionCert. It supplies the compiler-layer claim of the RS/EML bridge before reciprocal quotienting, separating the oriented log coordinate from its symmetrized J-cost form. This step precedes derivation of J(exp u)=cosh u -1 and connects the oriented ledger to the Recognition Science framework landmarks of the forcing chain and the RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.