Reference · Signed rationals

rainbow.math.rational.signed.decide-completeness

Signed rationalssrc/rainbow/math/rational/signed/decide_completeness.clj0 definitions, 13 theorems

Completeness of Rainbow's exact-rational decision procedures. The existing decision bridge is sound: a computation returning true yields the corresponding order or signed-equivalence proof. This module proves the converse for EVERY value, and then proves that a false result refutes the corresponding proposition. Consequently `signed/decide-equivalent` is a complete two-outcome proof-producing test for the Grothendieck equivalence of signed rationals, not merely a sound filter observed on concrete numerals. The proof follows the implementation boundary exactly. Nat completeness uses total Boolean case analysis, order antisymmetry, and the already-proved true-on-reflexive comparison. Nnrat completeness transports an order proof to the two natural cross products. Signed completeness applies the nnrat result to the signed cross sums. Equivalence completeness proves both signed orders and combines the two true decisions. Native and axiom-free on D63.

Depends onmath.rational.signed.decide-reflexivemath.rational.nnrat.order-equivalencemath.rational.signed.decide-equivalencemath.logic.boolean-and

boolean/and-true-complete :
  (left right : data/Bool)
  (left-true : left = data/true)
  (right-true : right = data/true)
  → boolean/and left right = data/true

nat/decide-at-most-true-complete :
  (left right : ℕ)
  (ordered : left ≤ right)
  → nat/decide-at-most left right = data/true

nnrat/decide-at-most-true-complete :
  (left right : ℚ≥0)
  (ordered : left ≤ right)
  → audit/decide-nnrat-at-most left right = data/true

signed/decide-at-most-true-complete :
  (left right : ℚ)
  (ordered : left ≤ right)
  → signed/decide-at-most left right = data/true

signed/decide-equivalent-true-complete :
  (left right : ℚ)
  (same : left = right)
  → signed/decide-equivalent left right = data/true

nat/decide-at-most-false-sound :
  (left right : ℕ)
  (decided-false : nat/decide-at-most left right = data/false)
  (h₁ : left ≤ right)
  → proposition/falsity

nnrat/decide-at-most-false-sound :
  (left right : ℚ≥0)
  (decided-false : audit/decide-nnrat-at-most left right = data/false)
  (h₁ : left ≤ right)
  → proposition/falsity

signed/decide-at-most-false-sound :
  (left right : ℚ)
  (decided-false : signed/decide-at-most left right = data/false)
  (h₁ : left ≤ right)
  → proposition/falsity

signed/decide-equivalent-false-sound :
  (left right : ℚ)
  (decided-false : signed/decide-equivalent left right = data/false)
  (h₁ : left = right)
  → proposition/falsity

nat/decide-at-most-false-complete :
  (left right : ℕ) (not-ordered : left ≤ right → proposition/falsity)
  → nat/decide-at-most left right = data/false

nnrat/decide-at-most-false-complete :
  (left right : ℚ≥0) (not-ordered : left ≤ right → proposition/falsity)
  → audit/decide-nnrat-at-most left right = data/false

signed/decide-at-most-false-complete :
  (left right : ℚ) (not-ordered : left ≤ right → proposition/falsity)
  → signed/decide-at-most left right = data/false

signed/decide-equivalent-false-complete :
  (left right : ℚ) (not-same : left = right → proposition/falsity)
  → signed/decide-equivalent left right = data/false