IndisputableMonolith.Information.EMLFromRecognition

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# EML from Oriented Recognition Coordinates
   6
   7This module formalizes the honest RS/EML bridge.
   8
   9It does not claim that the reciprocal cost `J` alone derives the EML gate.
  10That would be false: `J x = J x⁻¹` forgets orientation.
  11
  12The claim proved here is compiler-layer:
  13
  14* before reciprocal quotienting, an oriented recognition ledger has an
  15  additive log coordinate;
  16* the multiplicative-ratio chart maps are `exp` and `log`;
  17* the oriented ledger combiner is subtraction;
  18* therefore the induced two-input compiler gate is
  19  `eml x y = exp x - log y`.
  20
  21The same exp/log data, after reciprocal symmetrization, gives
  22`J(exp u) = cosh u - 1`.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Information
  27namespace EMLFromRecognition
  28
  29open Cost
  30
  31noncomputable section
  32
  33/-- Odrzywolek's EML operator, read as an oriented exp-log compiler gate. -/
  34def eml (x y : ℝ) : ℝ :=
  35  Real.exp x - Real.log y
  36
  37/-- Oriented additive ledger coordinates lift to positive ratios by exponentiation. -/
  38def orientedToRatio (u : ℝ) : ℝ :=
  39  Real.exp u
  40
  41/-- Positive ratios project back to additive ledger coordinates by logarithm. -/
  42def orientedFromRatio (x : ℝ) : ℝ :=
  43  Real.log x
  44
  45/-- The oriented ledger combiner before reciprocal symmetrization. -/
  46def orientedSub (a b : ℝ) : ℝ :=
  47  a - b
  48
  49/-- The compiler gate induced by the oriented exp/log chart and subtraction. -/
  50def orientedCompilerGate (x y : ℝ) : ℝ :=
  51  orientedSub (orientedToRatio x) (orientedFromRatio y)
  52
  53/-- The induced oriented compiler gate is exactly EML. -/
  54theorem oriented_compiler_gate_eq_eml (x y : ℝ) :
  55    orientedCompilerGate x y = eml x y := by
  56  rfl
  57
  58/-- The identity terminal kills the logarithmic channel. -/
  59theorem identity_terminal_kills_log : Real.log 1 = 0 := by
  60  simp
  61
  62/-- EML recovers exponentiation by feeding the identity terminal to the
  63logarithmic channel. -/
  64theorem eml_recovers_exp (x : ℝ) :
  65    eml x 1 = Real.exp x := by
  66  simp [eml]
  67
  68/-- EML recovers the constant `e` from the terminal `1`. -/
  69theorem eml_recovers_e :
  70    eml 1 1 = Real.exp 1 := by
  71  simp [eml]
  72
  73/-- The cancellation loop that recovers logarithm from EML.  Over real Lean
  74this statement uses Lean's total `Real.log`; analytically it is the real
  75positive branch or the chosen complex branch in the paper. -/
  76theorem eml_recovers_log (x : ℝ) :
  77    eml 1 (eml (eml 1 x) 1) = Real.log x := by
  78  unfold eml
  79  simp only [Real.log_one, sub_zero]
  80  rw [Real.log_exp]
  81  ring
  82
  83/-- Once `exp` and `log` have been recovered, EML recovers subtraction on
  84positive ratios. -/
  85theorem eml_recovers_sub (x y : ℝ) (hx : 0 < x) :
  86    eml (Real.log x) (Real.exp y) = x - y := by
  87  unfold eml
  88  rw [Real.exp_log hx, Real.log_exp]
  89
  90/-- Reciprocal cost forgets the orientation of the log coordinate. -/
  91theorem reciprocal_cost_forgets_orientation (u : ℝ) :
  92    Jlog u = Jlog (-u) := by
  93  have h := Jcost_symm (Real.exp_pos u)
  94  simpa [Jlog, Real.exp_neg] using h
  95
  96/-- EML keeps oriented channel data: the same terminal can be used to expose
  97the forward exp channel, while the log channel remains separately addressable. -/
  98theorem eml_keeps_oriented_channels (x : ℝ) :
  99    eml x 1 = orientedToRatio x ∧
 100    orientedFromRatio x = Real.log x := by
 101  constructor
 102  · simp [eml, orientedToRatio]
 103  · rfl
 104
 105/-- A compact certificate for the theorem-grade RS/EML bridge. -/
 106structure EMLFromRecognitionCert where
 107  compiler_gate :
 108    ∀ x y : ℝ, orientedCompilerGate x y = eml x y
 109  exp_recovery :
 110    ∀ x : ℝ, eml x 1 = Real.exp x
 111  log_recovery :
 112    ∀ x : ℝ, eml 1 (eml (eml 1 x) 1) = Real.log x
 113  sub_recovery :
 114    ∀ x y : ℝ, 0 < x → eml (Real.log x) (Real.exp y) = x - y
 115  reciprocal_cost_quotient :
 116    ∀ u : ℝ, Jlog u = Jlog (-u)
 117
 118/-- The EML compiler gate follows from oriented exp/log recognition data. -/
 119def emlFromRecognitionCert : EMLFromRecognitionCert where
 120  compiler_gate := oriented_compiler_gate_eq_eml
 121  exp_recovery := eml_recovers_exp
 122  log_recovery := eml_recovers_log
 123  sub_recovery := eml_recovers_sub
 124  reciprocal_cost_quotient := reciprocal_cost_forgets_orientation
 125
 126theorem eml_from_recognition_cert_holds : Nonempty EMLFromRecognitionCert :=
 127  ⟨emlFromRecognitionCert⟩
 128
 129end
 130end EMLFromRecognition
 131end Information
 132end IndisputableMonolith
 133