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
Lt(a, b)Exact expansion
exists h. h + S a = bThis 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
CF0015 FermatFourStrictDescent ND0070 EuclidParameters ND0074 EuclidParametrization ND0072 SmallerFermatFourCounterexampleAll transitive conservative prerequisites
none
Used by theorem statements or local proof propositions
PF000E fermat_four_bounded_descent PF0018 square_lt_strict PF001A square_lt_reflect PF001H pythagorean_positive_add_strict PF001I pythagorean_leg_strictly_below_hypotenuse PF001T pythagorean_positive_gap_orders_parameters PF0020 pythagorean_ordered_gap_positive PF0022 pythagorean_positive_primitive_from_parameters PF002A fermat_four_lt_add_positive PF002B fermat_four_root_lt_normGrand-campaign planning vocabulary
Locate Lt in the global campaign vocabulary →
Reviewed Lt corresponds to blueprint Lt with checked argument positions [0, 1].
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.