Foundation Ledger To Factorization Ledger Linear Response From Primitive Ledger

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

/-- Primitive ledger posting plus **per-slice directional regularity** forces the
completed real ledger-linear response.  For each fixed first cost `u`, the
combined cost responds to posted mass `v` in one consistent order direction
(monotone or antitone).  This is the genuine, non-vacuous order replacement for
the analytic continuity gate: unlike global monotonicity, the canonical RCL
combiner provably satisfies this (its response slope `2(u+1)` has a fixed sign
for each `u`), so the forcing hypothesis is consistent with its conclusion. -/
theorem ledgerLinearResponse_from_primitiveLedgerPosting_directional
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P)
    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v)) :
    LedgerLinearResponse P := by
  refine {
    symmetric := h.symmetric
    zeroBoundary := h.zeroBoundary
    unitDiagonal := h.unitDiagonal
    rightResponse := ?_
    free_ledger_additivity := h.free_ledger_additivity
  }
  intro u v
  let response : ℝ → ℝ := fun t => P u t - P u 0
  have hadd : ∀ x y, response (x + y) = response x + response y := by
    intro x y
    exact primitiveLedgerPosting_forces_rightPostedAdditive P h u x y
  have hlin : ∀ x, response x = response 1 * x := by
    rcases hdir u with hmono | hanti
    · have hrmono : Monotone response := by
        intro a b hab
        exact sub_le_sub_right (hmono hab) (P u 0)
      exact monotone_additive_isLinear hadd hrmono
    · have hranti : Antitone response := by
        intro a b hab
        exact sub_le_sub_right (hanti hab) (P u 0)
      exact antitone_additive_isLinear hadd hranti
  have hsub : P u v - P u 0 = (P u 1 - P u 0) * v := by
    simpa [response] using hlin v
  linarith

/-- 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 over arbitrary weighted defect ledgers gives the
additive response law for arbitrary real postings. -/
theorem primitiveLedgerPosting_forces_rightPostedAdditive
    (P : ℝ → ℝ → ℝ) (h : PrimitiveLedgerPostingSemantics P) :
    ∀ u v w,
      P u (v + w) - P u 0 =
        (P u v - P u 0) + (P u w - P u 0) := by
  intro u v w
  let weight : Bool → ℝ := fun b => if b then w else v
  let Γ : RecognitionLedgerFloor.DefectLedger Bool := Finsupp.single false 1
  let Δ : RecognitionLedgerFloor.DefectLedger Bool := Finsupp.single true 1
  have hpost := h.rightLedgerPostedAdditive u Bool weight Γ Δ
  have hΓ : RecognitionLedgerFloor.ledgerCost weight Γ = v := by
    simp [Γ, weight, RecognitionLedgerFloor.ledgerCost_single]
  have hΔ : RecognitionLedgerFloor.ledgerCost weight Δ = w := by
    simp [Δ, weight, RecognitionLedgerFloor.ledgerCost_single]
  have hsum : RecognitionLedgerFloor.ledgerCost weight (Γ + Δ) = v + w := by
    rw [RecognitionLedgerFloor.ledgerCost_add, hΓ, hΔ]
  simpa [hΓ, hΔ, hsum] using hpost

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