EMLFromRecognitionCert
plain-language theorem explainer
This structure certifies the bridge from oriented recognition coordinates to the EML operator in Recognition Science. It asserts equality of the oriented compiler gate with the EML operator and recovery of the exponential, logarithmic, and subtraction operations, plus evenness of the log-domain cost. Researchers on the RS/EML connection would cite it as the compact certificate. The declaration is a structure definition assembling five lemmas.
Claim. The certificate consists of five assertions: the oriented compiler gate induced by the exp/log chart and subtraction equals the EML operator $e^x - log y$ for all real $x,y$; the EML operator recovers the exponential via $e^x - log 1 = e^x$ for all real $x$; the EML operator recovers the logarithm via the nested composition $e^1 - log(e^1 - log(e^1 - log x)) = log x$ for all real $x$; the EML operator recovers subtraction via $e^{log x} - log(e^y) = x - y$ for $x > 0$; and the log-domain cost satisfies $J(u) = J(-u)$ for all real $u$.
background
The module formalizes the honest RS/EML bridge. The EML operator is defined as the map sending a pair of reals to their difference after exponentiation and logarithm, serving as an oriented exp-log compiler gate. The oriented compiler gate is constructed via oriented subtraction on the ratio maps that lift additive log coordinates to positive ratios. Upstream, the log-domain cost is defined as the cost function composed with the exponential and equals $(e^t + e^{-t})/2 - 1$; the PrimitiveDistinction.from theorem reduces seven axioms to four structural conditions plus three definitional facts.
proof idea
This declaration is a structure definition, a one-line wrapper that assembles five lemmas: the equality of the oriented compiler gate with the EML operator, the exponential recovery lemma, the logarithmic recovery lemma, the subtraction recovery lemma, and the reciprocity lemma for the log-domain cost.
why it matters
This certificate feeds directly into the definition emlFromRecognitionCert and the theorem eml_from_recognition_cert_holds asserting the certificate is nonempty. It realizes the compiler-layer claim that the oriented recognition ledger induces the EML gate $e^x - log y$ before reciprocal symmetrization. In the Recognition Science framework it connects the oriented exp/log data to the EML operator, consistent with the forcing chain where J-uniqueness and the phi fixed point precede the eight-tick octave and D=3; it leaves open whether a purely reciprocal derivation of EML is possible, which the module states is false.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.