Reference · Signed rationals

rainbow.math.rational.signed.indexed-max

Signed rationalssrc/rainbow/math/rational/signed/indexed_max.clj0 definitions, 3 theorems

Index-aware MAX aggregation -- the argmax semantic core, continuing the non-invasive Level-6 line (indexed-sum -> indexed-max). Reads env at each index and folds signed/max from a fallback init. signed/indexed-max-from env init n := max(init, env 0, ..., env (n-1)) (Nat.rec) signed/indexed-max-from-dominates-init : forall env init n, init <= indexed-max-from env init n signed/indexed-max-from-upper-of-last : forall env init m, env m <= indexed-max-from env init (succ m) The dominance-of-init is proved by induction (max-upper-left + at-most-transitive); the last-element bound is direct (max-upper-right). The full 'dominates every index below n' is a follow-on needing strict-below case analysis. This is the semantic target a future index-aware fold CONSTRUCTOR would let a verified program compute -- see the design notes.

Depends onmath.rational.signed.minmaxmath.rational.signed.order-transitivity

signed/indexed-max-from :
  (x₁ : ℕ → ℚ) (x₂ : ℚ) (x₃ : ℕ)
  → ℚ

signed/indexed-max-from-dominates-init :
  (env : ℕ → ℚ) (init : ℚ) (n : ℕ)
  → init ≤ signed/indexed-max-from env init n

signed/indexed-max-from-upper-of-last :
  (env : ℕ → ℚ) (init : ℚ) (m : ℕ)
  → env m ≤ signed/indexed-max-from env init (data/succ m)