Reference · Non-negative rationals

rainbow.math.rational.nnrat.quadratic-zero

Non-negative rationalssrc/rainbow/math/rational/nnrat/quadratic_zero.clj0 definitions, 3 theorems

Zero reflection and the equality case of the nnrat square inequality. nat/multiply-self-zero nnrat/square-zero-reflects nnrat/quadratic-equality-reflects The quadratic theorem proves p*p + n*n ~ p*n + n*p -> p ~ n. Decidable total order chooses the smaller component. Difference existence writes the larger as smaller+gap; verified ring normalization reduces the hypothesis to core+gap^2 ~ core, additive cancellation forces gap^2~0, and square-zero reflection forces gap~0. Native and axiom-free.

Depends onmath.rational.nnrat.order-difference

nat/multiply-self-zero :
  (value : ℕ)
  (zero-product : nat/multiply value value = 0)
  → value = 0

nnrat/square-zero-reflects :
  (value : ℚ≥0)
  (zero-square : value · value = 0)
  → value = 0

nnrat/quadratic-equality-reflects :
  (positive negative : ℚ≥0)
  (balanced : positive · positive + negative · negative = positive · negative + negative · positive)
  → positive = negative