PD0012 · conservative definition

Mod4Three

n is three modulo four by an explicit quotient.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Readable signature

Mod4Three(n)

Exact expansion

exists h. n = 4 * h + 3

This node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.

Definition neighborhood

Expands using

none

Used by definitions

none

Used by theorem statements or local proof propositions

PA00FR odd_half_odd_iff_mod4_three PA00FU qres_opposite_status_from_mod_four_three PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts PA00FW quadratic_reciprocity_combined