Foundation Ledger To Factorization

/-- Primitive ledger posting plus continuity forces the canonical RCL
combiner. -/
theorem primitiveLedgerPosting_forces_rcl
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
    (hcont : ∀ u, Continuous fun v => P u v) :
    ∀ u v, P u v = rclCombiner u v :=
  ledgerLinearResponse_forces_rcl P
    (ledgerLinearResponse_from_primitiveLedgerPosting P h hcont)

/-- Primitive ledger posting plus monotone response forces the canonical RCL
combiner.  No continuity or completeness is used: only additivity from the free
ledger and order regularity. -/
theorem primitiveLedgerPosting_monotone_forces_rcl
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
    (hmono : ∀ u, Monotone fun v => P u v) :
    ∀ u v, P u v = rclCombiner u v :=
  ledgerLinearResponse_forces_rcl P
    (ledgerLinearResponse_from_primitiveLedgerPosting_monotone P h hmono)

/-- Primitive ledger posting plus **ledger-native cost non-negativity** forces the
canonical RCL combiner.  This is the fully ledger-internal route to
right-affineness: additivity comes from `ledgerCost_add`, and the only order
input is that posting non-negative defect mass never lowers cost, which is the
order shadow of `ledgerCost_nonneg`. -/
theorem primitiveLedgerPosting_nonneg_forces_rcl
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
    (hnn : ∀ u v, 0 ≤ v → P u 0 ≤ P u v) :
    ∀ u v, P u v = rclCombiner u v :=
  ledgerLinearResponse_forces_rcl P
    (ledgerLinearResponse_from_primitiveLedgerPosting_nonneg P h hnn)

/-- 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

/-- 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

/-- Primitive ledger posting plus continuity forces completed real
ledger-linear response. -/
theorem ledgerLinearResponse_from_primitiveLedgerPosting
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
    (hcont : ∀ u, Continuous fun v => P u v) :
    LedgerLinearResponse P :=
  ledgerLinearResponse_from_free_ledger P
    (freeLedgerCombinerSemantics_from_primitiveLedgerPosting P h hcont)