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.
Definition in prerequisite notation
∃ cfc_state_prioritylayer. ConvergentMatrixCode(s,u,U,v,V,cfc_state_prioritylayer) ∧ BetaAt(h,e,j,cfc_state_prioritylayer)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists cfc_state_prioritylayer. ((exists cfc_left_prioritylayercode cfc_right_prioritylayercode cfc_matrix_prioritylayercode. ((cfc_left_prioritylayercode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_prioritylayercode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_prioritylayercode = ((cfc_left_prioritylayercode) + (cfc_right_prioritylayercode)) * S ((cfc_left_prioritylayercode) + (cfc_right_prioritylayercode)) + ((cfc_right_prioritylayercode) + (cfc_right_prioritylayercode))) /\ ((cfc_state_prioritylayer) = ((s) + (cfc_matrix_prioritylayercode)) * S ((s) + (cfc_matrix_prioritylayercode)) + ((cfc_matrix_prioritylayercode) + (cfc_matrix_prioritylayercode))))))) /\ (((exists ff_h_prioritylayerentry. ff_h_prioritylayerentry + S (cfc_state_prioritylayer) = S ((S (j)) * e)) /\ exists ff_q_prioritylayerentry. h = ff_q_prioritylayerentry * S ((S (j)) * e) + (cfc_state_prioritylayer))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.