PA009G

scaled_inverse_no_fixed_of_not_qres

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

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

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.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

16 script commands · 8 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
scaled inverse fixed point iff
01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro hnq
  5. L5
    intro hrel
02Establish hfixedL6–9

Establish this local claim before using it. It is not an additional assumption.

  1. L6
    have 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))
  2. L7
    specialize scaled_inverse_fixed_point_iff p
  3. L8
    specialize scaled_inverse_fixed_point_iff a
  4. L9
    specialize scaled_inverse_fixed_point_iff x
03Separate the logical casesL10–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L10
    cases scaled_inverse_fixed_point_iff
04Use earlier factsL11–12

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L11
    apply scaled_inverse_fixed_point_iff_left
  2. L12
    exact hrel
05Separate the logical casesL13–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    cases hfixed
06Use earlier factsL14–14

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L14
    apply hnq
07Construct an explicit witnessL15–15

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists x
08Use earlier factsL16–16

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L16
    exact hfixed_right

Library-wide reading audit

Original exact command ledger · 16 lines
  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