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 conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.

Definition neighborhood

Depends on conservative definitions

none

Used by conservative definitions

none

All transitive conservative prerequisites

none

Used by theorem statements or local proof propositions

SL0005 quadratic_supplement_minus_one_nonresidue_iff_mod_four_three SL0006 quadratic_supplement_minus_one_complete

Grand-campaign planning vocabulary

Locate Mod4Three in the global campaign vocabulary →

Reviewed Mod4Three corresponds to blueprint Mod4Three with checked argument positions [0].

The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.