eml_from_recognition_cert_holds
plain-language theorem explainer
The declaration certifies existence of a compact structure that equates the oriented compiler gate to the EML function and recovers the exp, log, and subtraction maps from recognition coordinates. Researchers tracing the RS/EML bridge would cite it to confirm the pre-symmetrization compiler layer. The proof is a one-line term that directly supplies the pre-built certificate instance.
Claim. There exists a structure $C$ such that for all real $x,y$, the oriented compiler gate satisfies orientedCompilerGate$(x,y)=$ eml$(x,y)$, eml$(x,1)=$ Real.exp$(x)$, eml$(1,$ eml$(($ eml$(1,x),1),1))=$ Real.log$(x)$, eml$(($ Real.log$(x),$ Real.exp$(y)))=x-y$ whenever $x>0$, and the reciprocal cost quotient holds.
background
The module formalizes the honest RS/EML bridge. It explicitly avoids claiming that the reciprocal cost $J$ alone derives the EML gate, since $J(x)=J(x^{-1})$ forgets orientation. Instead, before reciprocal quotienting, an oriented recognition ledger carries an additive log coordinate; the multiplicative-ratio charts are the maps exp and log; the oriented ledger combiner is subtraction; the induced two-input compiler gate is therefore eml $x y =$ exp $x -$ log $y$. After reciprocal symmetrization the same data yield $J($exp $u)=$ cosh $u - 1$ (T5 J-uniqueness).
proof idea
The proof is a one-line term wrapper that applies the definition emlFromRecognitionCert. That definition assembles four sibling lemmas: oriented_compiler_gate_eq_eml for the gate equality, eml_recovers_exp, eml_recovers_log, eml_recovers_sub for the recovery properties, and reciprocal_cost_forgets_orientation for the quotient clause.
why it matters
This theorem supplies the top-level existence statement for the EMLFromRecognitionCert structure inside the Information.EMLFromRecognition module, closing the compiler-layer bridge described in the module documentation. It directly supports the Recognition Science claim that oriented exp/log data induce the EML gate before J-symmetrization (T5 and the eight-tick octave). No downstream uses are recorded, but the certificate is the required interface for any further work on the RS/EML correspondence or on the alpha-band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.