Reference · Signed rationals

rainbow.math.rational.signed.indexed-max-attains

Signed rationalssrc/rainbow/math/rational/signed/indexed_max_attains.clj0 definitions, 2 theorems

Attainment for the index-aware max -- the other half of argmax correctness (with dominance). signed/max-is-left-or-right : forall a b, (max a b = a) or (max a b = b) (Bool.rec on the decision) signed/indexed-max-from-attains : forall env init n, (indexed-max-from env init n = init) or (exists i, strict-below i n AND indexed-max-from env init n = env i). The aggregate is either the fallback init or an actual input at some index below n. By induction on n via max-is-left-or-right, the IH, and the nat weakening/self lemmas. Off the trusted base.

Depends onmath.rational.signed.indexed-maxmath.nat.strict-below-more

signed/max-is-left-or-right :
  (a b : ℚ)
  → proposition/disjunction (signed/max a b = a) (signed/max a b = b)

signed/indexed-max-from-attains :
  (env : ℕ → ℚ) (init : ℚ) (n : ℕ)
  → proposition/disjunction (signed/indexed-max-from env init n = init) (existence)
  where existence := proposition/existence ℕ (fun i => proposition/conjunction (nat/strict-below i n) (signed/indexed-max-from env init n = env i))