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
∃ cfba_error_prioritylayer. ∃ cfba_previous_error_prioritylayer. AlternatingConvergentIdentity(a,b,u,U,v,V,cfba_error_prioritylayer,cfba_previous_error_prioritylayer) ∧ (Lt(cfba_error_prioritylayer,cfba_previous_error_prioritylayer) ∧ Le(cfba_previous_error_prioritylayer,b))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists cfba_error_prioritylayer cfba_previous_error_prioritylayer. (((((u * V + 1 = U * v) /\ ((a * v = b * u + cfba_error_prioritylayer) /\ (b * U = a * V + cfba_previous_error_prioritylayer)))) \/ (((U * v + 1 = u * V) /\ ((b * u = a * v + cfba_error_prioritylayer) /\ (a * V = b * U + cfba_previous_error_prioritylayer))))) /\ ((exists cfba_gap_prioritylayerdecrease. cfba_gap_prioritylayerdecrease + S (cfba_error_prioritylayer) = (cfba_previous_error_prioritylayer)) /\ (exists cfba_bound_prioritylayerprevious_bound. cfba_bound_prioritylayerprevious_bound + (cfba_previous_error_prioritylayer) = (b))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none
Checked theorems using this definition
BA000B · cf_approximation_first_recurrence_error_invariantBA000C · cf_approximation_prepend_recurrence_error_invariantBA000D · cf_approximation_derived_invariant_denominator_positiveBA000E · cf_approximation_derived_invariant_determinantBA0026 · cf_approximation_derived_invariant_best_signedBA003E · cf_convergent_actual_prefix_error_invariant