Foundation Ledger To Factorization Factorization Gate Of Primitive Ledger Postin

/-- Primitive ledger posting plus **per-slice directional regularity** forces the
canonical RCL combiner.  Additivity is supplied by `ledgerCost_add`; the only
regularity input is that each fixed-cost response is monotone in one direction,
which the canonical combiner provably satisfies, so this forcing is
non-vacuous. -/
theorem primitiveLedgerPosting_directional_forces_rcl
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v)) :
    ∀ u v, P u v = rclCombiner u v :=
  ledgerLinearResponse_forces_rcl P
    (ledgerLinearResponse_from_primitiveLedgerPosting_directional P h hdir)

/-- Monotone additive real responses are linear.  This is the order-regularity
replacement for the continuity gate in the additive Cauchy step. -/
theorem monotone_additive_isLinear {f : ℝ → ℝ}
    (hadd : ∀ x y, f (x + y) = f x + f y) (hmono : Monotone f) :
    ∀ x, f x = f 1 * x := by
  have hf0 : f 0 = 0 := by
    have h := hadd 0 0
    rw [add_zero] at h
    linarith
  let F : ℝ →+ ℝ := AddMonoidHom.mk' f (fun a b => hadd a b)
  have hFcoe : ∀ y, F y = f y := fun _ => rfl
  have hFq : ∀ q : ℚ, f (q : ℝ) = f 1 * (q : ℝ) := by
    intro q
    have h := map_ratCast_smul F ℝ ℝ q (1 : ℝ)
    simp only [smul_eq_mul, mul_one, hFcoe] at h
    rw [h]
    ring
  intro x
  set c := f 1 with hc_def
  have hc : 0 ≤ c := by
    have hmle : f 0 ≤ f 1 := hmono (by norm_num)
    rw [hf0] at hmle
    exact hmle
  rcases eq_or_lt_of_le hc with hc0 | hcpos
  · have hub : f x ≤ 0 := by
      obtain ⟨r, hxr, -⟩ := exists_rat_btwn (lt_add_one x)
      have hmr := hmono hxr.le
      rw [hFq r, ← hc0, zero_mul] at hmr
      exact hmr
    have hlb : 0 ≤ f x := by
      obtain ⟨q, -, hqx⟩ := exists_rat_btwn (sub_one_lt x)
      have hmq := hmono hqx.le
      rw [hFq q, ← hc0, zero_mul] at hmq
      exact hmq
    rw [← hc0, zero_mul]
    linarith
  · refine le_antisymm ?_ ?_
    · by_contra hcon
      push_neg at hcon
      have hxlt : x < f x / c := by
        rw [lt_div_iff₀ hcpos]
        linarith [mul_comm c x]
      obtain ⟨r, hxr, hrlt⟩ := exists_rat_btwn hxlt
      have h1 : f x ≤ c * (r : ℝ) := by
        have hm := hmono hxr.le
        rwa [hFq r] at hm
      have h2 : c * (r : ℝ) < f x := by
        have := (lt_div_iff₀ hcpos).mp hrlt
        linarith [mul_comm (r : ℝ) c]
      linarith
    · by_contra hcon
      push_neg at hcon
      have hxlt : f x / c < x := by
        rw [div_lt_iff₀ hcpos]
        linarith [mul_comm c x]
      obtain ⟨q, hqlt, hqx⟩ := exists_rat_btwn hxlt
      have h1 : c * (q : ℝ) ≤ f x := by
        have hm := hmono hqx.le
        rwa [hFq q] at hm
      have h2 : f x < c * (q : ℝ) := by
        have := (div_lt_iff₀ hcpos).mp hqlt
        linarith [mul_comm (q : ℝ) c]
      linarith

/-- Antitone additive real responses are linear.  Apply the monotone lemma to
`-f`.  This is the second branch of the directional (order) regularity route:
the RCL response slope `2(u+1)` is negative for `u < -1`, so the response is
antitone there, not monotone. -/
theorem antitone_additive_isLinear {f : ℝ → ℝ}
    (hadd : ∀ x y, f (x + y) = f x + f y) (hanti : Antitone f) :
    ∀ x, f x = f 1 * x := by
  have hadd' : ∀ x y, (fun t => -f t) (x + y) =
      (fun t => -f t) x + (fun t => -f t) y := by
    intro x y
    simp only [hadd x y]
    ring
  have hmono' : Monotone (fun t => -f t) := by
    intro a b hab
    simp only [neg_le_neg_iff]
    exact hanti hab
  have h := monotone_additive_isLinear hadd' hmono'
  intro x
  have hx : -f x = -f 1 * x := h x
  have hx2 : -f x = -(f 1 * x) := by rw [hx]; ring
  linarith

/-- Ledger-linear response supplies the `rightAffine` field of the
factorization gate. -/
theorem rightAffine_of_ledgerLinearResponse
    (P : ℝ → ℝ → ℝ) (h : LedgerLinearResponse P) :
    ∀ u, ∃ α β, ∀ v, P u v = α * v + β := by
  intro u
  exact ⟨P u 1 - P u 0, P u 0, h.rightResponse u⟩

/-- Ledger-linear response forces the RCL polynomial through the existing gate
theorem. -/
theorem ledgerLinearResponse_forces_rcl
    (P : ℝ → ℝ → ℝ) (h : LedgerLinearResponse P) :
    ∀ u v, P u v = rclCombiner u v := by
  intro u v
  rw [gate_forces_rcl P (factorizationGate_of_ledgerLinearResponse P h) u v]
  rfl