orientedToRatio
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 in Recognition Science
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.
scope and limits
- Does not claim that the reciprocal cost J alone derives the EML gate.
- Does not address the symmetrized case in which orientation is forgotten.
- Does not supply numerical values for physical constants or the alpha band.
Lean usage
example (u : ℝ) : orientedToRatio u = Real.exp u := rflformal statement (Lean)
38def orientedToRatio (u : ℝ) : ℝ :=
proof body
Definition body.
39 Real.exp u
40
41/-- Positive ratios project back to additive ledger coordinates by logarithm. -/