orientedFromRatio
plain-language theorem explainer
The orientedFromRatio definition converts a positive ratio to its additive ledger coordinate by applying the natural logarithm. Researchers formalizing the oriented EML compiler gate before reciprocal symmetrization cite it when separating forward and inverse channels in Recognition Science. The implementation is a direct one-line assignment to the real logarithm.
Claim. The map sending a positive ratio $x$ to its additive ledger coordinate is the natural logarithm: $f(x) = log x$ for $x > 0$.
background
The EMLFromRecognition module isolates the oriented ledger stage before reciprocal symmetrization. In this stage an additive log coordinate exists on the recognition ledger, with multiplicative ratios mapped by exp and log and combination performed by subtraction. The reciprocal automorphism from CostAlgebra and LedgerForcing sends each event to its inverse ratio and erases orientation, while the before relation from TimeEmergence orders snapshots by tick index.
proof idea
This is a one-line definition that directly applies the real logarithm function.
why it matters
It supplies the log map required by orientedCompilerGate and is invoked in eml_keeps_oriented_channels to confirm that EML preserves separate oriented channels. The definition completes the compiler-layer claim stated in the module documentation, keeping the oriented log distinct from the J-cost that later produces cosh(u) - 1 after symmetrization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.