PA009G

scaled_inverse_no_fixed_of_not_qres

Alpha v16 checked-use theorem · independently closed; not Stable

A negative QRes witness makes the scaled involution fixed-point-free.

Exact expanded PA statement

forall p a x. ~(exists qr_x_euler_scaled_inverse. exists qr_u_euler_scaled_inverse qr_v_euler_scaled_inverse. qr_x_euler_scaled_inverse * qr_x_euler_scaled_inverse + p * qr_u_euler_scaled_inverse = a + p * qr_v_euler_scaled_inverse) -> ~((((~(x = 0) /\ (exists esi_strict_gap_no_fixed_relation_left_bound. esi_strict_gap_no_fixed_relation_left_bound + S x = p))) /\ (((~(x = 0) /\ (exists esi_strict_gap_no_fixed_relation_right_bound. esi_strict_gap_no_fixed_relation_right_bound + S x = p))) /\ (exists esi_mod_left_no_fixed_relation_mod esi_mod_right_no_fixed_relation_mod. (x * x) + p * esi_mod_left_no_fixed_relation_mod = (a) + p * esi_mod_right_no_fixed_relation_mod))))

Structural proof guide

Generated structural guide

A negative QRes witness makes the scaled involution fixed-point-free.

Use the direct prerequisites scaled_inverse_fixed_point_iff as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (1).

Referenced ingredients

PA009F scaled_inverse_fixed_point_iff

Proof neighborhood

Direct dependencies

PA009F scaled_inverse_fixed_point_iff

Direct dependents

PA009H scaled_inverse_prefix_no_fixed_of_not_qres

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.

  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro hnq
  5. 0005intro hrel
  6. 0006have hfixed : (((~(x = 0) /\ (exists esi_strict_gap_no_fixed_square_unit_bound. esi_strict_gap_no_fixed_square_unit_bound + S x = p))) /\ (exists esi_mod_left_no_fixed_square_square esi_mod_right_no_fixed_square_square. (x * x) + p * esi_mod_left_no_fixed_square_square = (a) + p * esi_mod_right_no_fixed_square_square))
  7. 0007specialize scaled_inverse_fixed_point_iff p
  8. 0008specialize scaled_inverse_fixed_point_iff a
  9. 0009specialize scaled_inverse_fixed_point_iff x
  10. 0010cases scaled_inverse_fixed_point_iff
  11. 0011apply scaled_inverse_fixed_point_iff_left
  12. 0012exact hrel
  13. 0013cases hfixed
  14. 0014apply hnq
  15. 0015exists x
  16. 0016exact hfixed_right