orientedFromRatio
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not apply to non-positive inputs.
- Does not perform reciprocal symmetrization.
- Does not derive the full EML gate in isolation.
- Applies only before the reciprocal quotienting step.
formal statement (Lean)
42def orientedFromRatio (x : ℝ) : ℝ :=
proof body
Definition body.
43 Real.log x
44
45/-- The oriented ledger combiner before reciprocal symmetrization. -/