orientedSub
The declaration defines oriented subtraction on the reals as the difference of two coordinates. It supplies the combiner for oriented recognition ledgers in the RS-to-EML bridge before any reciprocal symmetrization. Researchers constructing the pre-symmetrized compiler gate would cite this step when mapping additive log coordinates through exp and log charts. The definition is a direct one-line alias for subtraction.
claimThe oriented ledger combiner is the map $(a,b)mapsto a-b$ on real numbers, acting on additive log coordinates prior to reciprocal symmetrization.
background
The EMLFromRecognition module formalizes the RS/EML bridge by separating the oriented ledger stage from later reciprocal quotienting. An oriented recognition ledger carries an additive log coordinate; the multiplicative-ratio charts are the exponential and logarithm maps. The oriented ledger combiner is subtraction, so the induced two-input compiler gate takes the form eml x y = exp x - log y. This precedes the step that recovers J(exp u) = cosh u - 1 after symmetrization. The upstream CirclePhaseLift.and result supplies an explicit log-derivative bound M that converts to a concrete angular Lipschitz constant on the circle of radius r.
proof idea
The definition is a direct one-line alias that sets orientedSub a b to a - b. No lemmas are applied; the body is the standard subtraction operation on the reals.
why it matters in Recognition Science
This definition supplies the combiner used by orientedCompilerGate to realize the oriented EML gate. It fills the compiler-layer claim that, before reciprocal quotienting, the oriented ledger possesses an additive log coordinate. In the Recognition framework it supports the transition from oriented coordinates to the J-cost function, consistent with the forcing chain that forces phi as the self-similar fixed point and yields the eight-tick octave. It underscores the documented limitation that J alone forgets orientation.
scope and limits
- Does not derive the EML gate from the reciprocal cost J alone.
- Does not perform reciprocal symmetrization of coordinates.
- Does not claim equivalence to full electromagnetic field equations.
- Does not extend to higher-dimensional or quantum structures.
Lean usage
orientedCompilerGate x y := orientedSub (orientedToRatio x) (orientedFromRatio y)formal statement (Lean)
46def orientedSub (a b : ℝ) : ℝ :=
proof body
Definition body.
47 a - b
48
49/-- The compiler gate induced by the oriented exp/log chart and subtraction. -/