orientedToRatio
plain-language theorem explainer
orientedToRatio lifts an oriented additive ledger coordinate u in the reals to a positive ratio via the exponential map. Researchers constructing the RS-EML bridge cite it when assembling the two-input compiler gate from oriented recognition data before reciprocal symmetrization. The definition is a direct one-line abbreviation to the standard real exponential.
Claim. $umapsto e^u$ for oriented additive ledger coordinate $u in mathbb{R}$.
background
The module formalizes the honest RS/EML bridge. An oriented recognition ledger has an additive log coordinate before reciprocal quotienting; the multiplicative-ratio chart maps are exp and log, while the oriented ledger combiner is subtraction. This induces the compiler gate eml x y = exp x - log y. The same data after reciprocal symmetrization recovers J(exp u) = cosh u - 1.
proof idea
The definition is a one-line wrapper that applies the real exponential function Real.exp to the input coordinate u.
why it matters
This definition supplies the forward exp map for the oriented compiler gate, which downstream results identify with EML. It fills the compiler-layer claim that oriented ledgers retain additive coordinates addressable by exp and log. It supports the framework step from T5 J-uniqueness to the eight-tick octave and D=3, and feeds eml_keeps_oriented_channels together with orientedCompilerGate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.