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
PD0041 Choose PD0014 Product PD0018 Range PD0015 Sum PD0019 Repeat CF0010 Digit PD0007 DivRem PD0040 DivisionPrefixAll transitive conservative prerequisites
none
Used by theorem statements or local proof propositions
LU0000 lucas_digit_carry_implies_prime_divides LU0001 lucas_prime_row_interior_divisible LU0003 lucas_digit_carry_iff_prime_divides LU0004 lucas_digit_no_carry_iff_not_divides LU0008 lucas_base_p_digit_of_small_value LU000C lucas_base_p_digit_prefix_point LU000I lucas_prime_row_sparse_complete LU000J lucas_positive_lower_quotient_exceeds_upper_digit LU000K lucas_positive_lower_quotient_digit_coefficient_zero LU000L lucas_zero_upper_quotient_high_column_vanishes LU000M lucas_prime_block_digit_congruence LU000N lucas_one_step_division_congruence LU000Q lucas_choose_zero_upper_positive_is_zero LU000S lucas_positive_digit_has_bounded_complement LU000T lucas_prime_row_interior_zero_mod LU000V lucas_predecessor_digit_below_base LU000W lucas_prime_shift_below_base LU000Y lucas_add_positive_index_strict LU000Z lucas_prime_shift_high_column LU0012 lucas_repeated_prime_shift_below_base LU0014 lucas_low_digit_product_congruence LU0016 lucas_digit_chain_empty LU0017 lucas_digit_chain_empty_exists LU0018 lucas_digit_chain_extend LU0019 lucas_digit_chain_exists LU001A lucas_prime_digit_chain_exists LU001B lucas_digit_chain_initial_value LU001C lucas_digit_chain_step_exists LU001D lucas_modular_backward_product_fold LU001E lucas_choose_prefix_empty LU001F lucas_choose_prefix_extend LU001G lucas_choose_prefix_exists LU001H lucas_choose_prefix_point LU001I lucas_multidigit_congruence_from_one_step LU001J lucas_terminating_multidigit_theorem_from_one_step LU001K lucas_prime_digit_nonzero_quotient_strict LU001L lucas_prime_digit_chain_nonzero_index_bound LU001M lucas_prime_digit_chain_terminal_zero LU001N lucas_terminating_prime_digit_chain_exists LU001O lucas_multidigit_congruence LU001P lucas_terminating_multidigit_theorem LU001Q lucas_theorem_for_length LU001R lucas_theoremGrand-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.