intCast_ne_zero_of_ne_zero

formal source

 240
 241/-! ### Jlog-cost tightening: if a monotone nontrivial tick has Jlog-cost ≤ Jlog(1), it is a posting step. -/
 242
 243private lemma intCast_ne_zero_of_ne_zero {z : ℤ} (hz : z ≠ 0) : ((z : ℤ) : ℝ) ≠ 0 := by
 244  exact_mod_cast hz
 245
 246private lemma jlog_lt_jlog_of_one_lt {x : ℝ} (hx : 1 < x) :
 247    Cost.Jlog (1 : ℝ) < Cost.Jlog x := by
 248  -- strict monotone on `Ici 0`, and `1 < x` implies `0 ≤ 1` and `0 ≤ x`
 249  have hmono := Cost.Jlog_strictMonoOn_Ici0
 250  have hx0 : (0 : ℝ) ≤ x := le_trans (show (0 : ℝ) ≤ (1 : ℝ) by linarith) (le_of_lt hx)
 251  exact hmono (by simp) (by simpa [Set.mem_Ici] using hx0) hx
 252
 253theorem postingStep_of_monotone_and_ledgerJlogCost_le_Jlog1 {d : Nat} {L L' : LedgerState d}
 254    (hmono : MonotoneLedger (d := d) L L')
 255    (hneq : L ≠ L')
 256    (hle : ledgerJlogCost (d := d) L L' ≤ Cost.Jlog (1 : ℝ)) :
 257    PostingStep (d := d) L L' := by
 258  classical
 259  -- helper: deltas
 260  let dΔ : Fin d → ℤ := fun i => L'.debit i - L.debit i
 261  let cΔ : Fin d → ℤ := fun i => L'.credit i - L.credit i
 262  have hdNonneg : ∀ i : Fin d, 0 ≤ dΔ i := by
 263    intro i
 264    have : L.debit i ≤ L'.debit i := hmono.1 i
 265    dsimp [dΔ]
 266    linarith
 267  have hcNonneg : ∀ i : Fin d, 0 ≤ cΔ i := by
 268    intro i
 269    have : L.credit i ≤ L'.credit i := hmono.2 i
 270    dsimp [cΔ]
 271    linarith
 272
 273  -- show every delta is ≤ 1 (otherwise cost would exceed Jlog 1)