Exact expanded PA statement
forall p a x. ((((((~(x = 0) /\ (exists esi_strict_gap_fixed_relation_left_bound. esi_strict_gap_fixed_relation_left_bound + S x = p))) /\ (((~(x = 0) /\ (exists esi_strict_gap_fixed_relation_right_bound. esi_strict_gap_fixed_relation_right_bound + S x = p))) /\ (exists esi_mod_left_fixed_relation_mod esi_mod_right_fixed_relation_mod. (x * x) + p * esi_mod_left_fixed_relation_mod = (a) + p * esi_mod_right_fixed_relation_mod)))) -> ((((~(x = 0) /\ (exists esi_strict_gap_fixed_square_unit_bound. esi_strict_gap_fixed_square_unit_bound + S x = p))) /\ (exists esi_mod_left_fixed_square_square esi_mod_right_fixed_square_square. (x * x) + p * esi_mod_left_fixed_square_square = (a) + p * esi_mod_right_fixed_square_square)))) /\ (((((~(x = 0) /\ (exists esi_strict_gap_fixed_square_unit_bound. esi_strict_gap_fixed_square_unit_bound + S x = p))) /\ (exists esi_mod_left_fixed_square_square esi_mod_right_fixed_square_square. (x * x) + p * esi_mod_left_fixed_square_square = (a) + p * esi_mod_right_fixed_square_square))) -> ((((~(x = 0) /\ (exists esi_strict_gap_fixed_relation_left_bound. esi_strict_gap_fixed_relation_left_bound + S x = p))) /\ (((~(x = 0) /\ (exists esi_strict_gap_fixed_relation_right_bound. esi_strict_gap_fixed_relation_right_bound + S x = p))) /\ (exists esi_mod_left_fixed_relation_mod esi_mod_right_fixed_relation_mod. (x * x) + p * esi_mod_left_fixed_relation_mod = (a) + p * esi_mod_right_fixed_relation_mod))))))Structural proof guide
Generated structural guide
On the bounded unit domain, fixed points are exactly square roots of a.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by case analysis (3).
Referenced ingredients
none
Proof neighborhood
Direct dependencies
none
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.