PA009H · theorem

scaled_inverse_prefix_no_fixed_of_not_qres

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

A nonresidue scaled-inverse prefix has no decoded fixed point.

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.

Statement with defined notation

∀ p. ∀ a. ∀ n. ∀ b. ∀ c. ∀ l. ∀ i. ¬QRes(p,a) → ScaledInversePrefix(p,a,n,b,c,l) → Lt(i,l) → ¬BetaAt(b,c,i,S i)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0021 QRes PD0039 ScaledInversePrefix

4 occurrences

In local proof propositions

PD0038 ScaledInverseIndex

1 occurrences

Exact expanded native-PA statement
forall p a n b c l i. ~(exists qr_x_esipe_fixed_nonresidue. exists qr_u_esipe_fixed_nonresidue qr_v_esipe_fixed_nonresidue. qr_x_esipe_fixed_nonresidue * qr_x_esipe_fixed_nonresidue + p * qr_u_esipe_fixed_nonresidue = a + p * qr_v_esipe_fixed_nonresidue) -> (forall esip_index_fixed_prefix. (exists esip_gap_fixed_prefix_prefix_bound. esip_gap_fixed_prefix_prefix_bound + S (esip_index_fixed_prefix) = l) -> exists esip_mate_fixed_prefix. ((((exists ff_h_esip_fixed_prefix_entry. ff_h_esip_fixed_prefix_entry + S (esip_mate_fixed_prefix) = S ((S (esip_index_fixed_prefix)) * c)) /\ exists ff_q_esip_fixed_prefix_entry. b = ff_q_esip_fixed_prefix_entry * S ((S (esip_index_fixed_prefix)) * c) + (esip_mate_fixed_prefix))) /\ ((exists esip_gap_fixed_prefix_relation_index_bound. esip_gap_fixed_prefix_relation_index_bound + S (esip_index_fixed_prefix) = n) /\ ((((~((S esip_index_fixed_prefix) = 0) /\ (exists esip_gap_fixed_prefix_relation_scaled_left_bound. esip_gap_fixed_prefix_relation_scaled_left_bound + S (S esip_index_fixed_prefix) = p))) /\ (((~(esip_mate_fixed_prefix = 0) /\ (exists esip_gap_fixed_prefix_relation_scaled_right_bound. esip_gap_fixed_prefix_relation_scaled_right_bound + S (esip_mate_fixed_prefix) = p))) /\ (exists esi_mod_left_fixed_prefix_relation_scaled_mod esi_mod_right_fixed_prefix_relation_scaled_mod. ((S esip_index_fixed_prefix) * esip_mate_fixed_prefix) + p * esi_mod_left_fixed_prefix_relation_scaled_mod = (a) + p * esi_mod_right_fixed_prefix_relation_scaled_mod))))))) -> (exists esip_gap_fixed_bound. esip_gap_fixed_bound + S (i) = l) -> ~(((exists ff_h_esipe_fixed_at. ff_h_esipe_fixed_at + S (S i) = S ((S (i)) * c)) /\ exists ff_q_esipe_fixed_at. b = ff_q_esipe_fixed_at * S ((S (i)) * c) + (S i)))

Proof neighborhood

Direct theorem prerequisites

PA0099 scaled_inverse_prefix_entry_sound PA009G scaled_inverse_no_fixed_of_not_qres

Direct theorem dependents

PA009I scaled_inverse_prefix_choose_omitted_orbit

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

31 script commands · 6 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
scaled inverse prefix entry soundscaled inverse no fixed of not qres
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro l
  7. L7
    intro i
  8. L8
    intro hnotqres
  9. L9
    intro hprefix
  10. L10
    intro hi
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hfixed
03Establish hrelationL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled inverse prefix entry sound.

  1. L12
    have hrelation : ScaledInverseIndex(p,a,n,i,S i)Definitions: ScaledInverseIndex(p,a,n,i,S i)Original native command in the exact edition
  2. L13
    specialize scaled_inverse_prefix_entry_sound p
  3. L14
    specialize scaled_inverse_prefix_entry_sound a
  4. L15
    specialize scaled_inverse_prefix_entry_sound n
  5. L16
    specialize scaled_inverse_prefix_entry_sound b
  6. L17
    specialize scaled_inverse_prefix_entry_sound c
  7. L18
    specialize scaled_inverse_prefix_entry_sound l
  8. L19
    specialize scaled_inverse_prefix_entry_sound i
  9. L20
    specialize scaled_inverse_prefix_entry_sound (S i)
  10. L21
    apply scaled_inverse_prefix_entry_sound
04Use earlier factsL22–24

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

  1. L22
    exact hprefix
  2. L23
    exact hi
  3. L24
    exact hfixed
05Separate the logical casesL25–25

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

  1. L25
    cases hrelation
06Use earlier factsL26–31

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

  1. L26
    specialize scaled_inverse_no_fixed_of_not_qres p
  2. L27
    specialize scaled_inverse_no_fixed_of_not_qres a
  3. L28
    specialize scaled_inverse_no_fixed_of_not_qres (S i)
  4. L29
    apply scaled_inverse_no_fixed_of_not_qres
  5. L30
    exact hnotqres
  6. L31
    exact hrelation_right

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro l
  7. 0007intro i
  8. 0008intro hnotqres
  9. 0009intro hprefix
  10. 0010intro hi
  11. 0011intro hfixed
  12. 0012have hrelation : ScaledInverseIndex(p,a,n,i,S i)
    Exact native replay linehave hrelation : (exists esip_gap_fixed_relation_index_bound. esip_gap_fixed_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_fixed_relation_scaled_left_bound. esip_gap_fixed_relation_scaled_left_bound + S (S i) = p))) /\ (((~(S i = 0) /\ (exists esip_gap_fixed_relation_scaled_right_bound. esip_gap_fixed_relation_scaled_right_bound + S (S i) = p))) /\ (exists esi_mod_left_fixed_relation_scaled_mod esi_mod_right_fixed_relation_scaled_mod. ((S i) * S i) + p * esi_mod_left_fixed_relation_scaled_mod = (a) + p * esi_mod_right_fixed_relation_scaled_mod))))
  13. 0013specialize scaled_inverse_prefix_entry_sound p
  14. 0014specialize scaled_inverse_prefix_entry_sound a
  15. 0015specialize scaled_inverse_prefix_entry_sound n
  16. 0016specialize scaled_inverse_prefix_entry_sound b
  17. 0017specialize scaled_inverse_prefix_entry_sound c
  18. 0018specialize scaled_inverse_prefix_entry_sound l
  19. 0019specialize scaled_inverse_prefix_entry_sound i
  20. 0020specialize scaled_inverse_prefix_entry_sound (S i)
  21. 0021apply scaled_inverse_prefix_entry_sound
  22. 0022exact hprefix
  23. 0023exact hi
  24. 0024exact hfixed
  25. 0025cases hrelation
  26. 0026specialize scaled_inverse_no_fixed_of_not_qres p
  27. 0027specialize scaled_inverse_no_fixed_of_not_qres a
  28. 0028specialize scaled_inverse_no_fixed_of_not_qres (S i)
  29. 0029apply scaled_inverse_no_fixed_of_not_qres
  30. 0030exact hnotqres
  31. 0031exact hrelation_right