proof

Hidden-rate accumulation

Lean spine source

formal/AlignmentProofSpine/Capability.lean

Declarations: positive_hidden_rate_eventually_crosses

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem positive_hidden_rate_eventually_crosses
    (rate threshold : Nat)
    (hr : 0 < rate) :
    ∃ n : Nat, threshold < n * rate := by
  refine ⟨threshold + 1, ?_⟩
  cases rate with
  | zero => cases hr
  | succ r =>
      have hbase : threshold < threshold + 1 := Nat.lt_succ_self threshold
      have hmul : threshold + 1 ≤ (threshold + 1) * (r + 1) :=
        Nat.le_mul_of_pos_right (threshold + 1) (Nat.succ_pos r)
      exact Nat.lt_of_lt_of_le hbase hmul