Reference · Signed rationals

rainbow.math.rational.signed.max-three

Signed rationalssrc/rainbow/math/rational/signed/max_three.clj1 definitions, 5 theorems

Reusable optimality certificate for a fixed three-candidate maximum. Fixed-cardinality selection is the largest honest argmax slice expressible by the current scalar Expr/Form language without adding lists, computed indexing, or a polymorphic result carrier. `signed/max-three` is an unrolled fold and the four theorems prove its exact universal property: every candidate is below it, and it is below every common upper bound. Native and axiom-free on D63.

Depends onmath.rational.signed.order-transitivitymath.rational.signed.minmax

signed/max-three :
  (x₁ x₂ x₃ : ℚ)
  → ℚ

signed/max-three-upper-first :
  (first second third : ℚ)
  → first ≤ signed/max-three first second third

signed/max-three-upper-second :
  (first second third : ℚ)
  → second ≤ signed/max-three first second third

signed/max-three-upper-third :
  (first second third : ℚ)
  → third ≤ signed/max-three first second third

signed/max-three-least-upper :
  (first second third upper : ℚ)
  (first-upper : first ≤ upper)
  (second-upper : second ≤ upper)
  (third-upper : third ≤ upper)
  → signed/max-three first second third ≤ upper

signed/max-three-is-first-or-second-or-third :
  (first second third : ℚ)
  → proposition/disjunction (signed/max-three first second third = first) (disjunction)
  where disjunction := proposition/disjunction (signed/max-three first second third = second) (signed/max-three first second third = third)