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
InverseIndex(m,l,i,j)Exact expansion
((exists dp_left_gap. dp_left_gap + S i = l) /\ ((exists dp_right_gap. dp_right_gap + S j = l) /\ (exists dp_u dp_v. (S i) * S j + m * dp_u = 1 + m * dp_v)))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
Used by definitions
Used by theorem statements or local proof propositions
PA00A4 prime_inverse_index_exists PA00A5 prime_inverse_prefix_extend PA00AF inverse_prefix_entry_sound PA00AH prime_inverse_prefix_fixed_cases PA00AJ inverse_index_symmetric PA00AL bounded_inverse_index_unique PA00AM inverse_prefix_extensional PA00AN inverse_prefix_involutive PA00AO inverse_prefix_zero_fixed PA00AP inverse_prefix_last_fixed PA00AR prime_choose_unused_nonendpoint_orbit PA00B7 paired_successor_lift_adjacent_units