PA008T

prime_scaled_inverse_prefix_exists

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

A prime predecessor interval has a full beta-coded scaled-inverse map.

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 n. p = S n -> ((~(p = 1) /\ forall esi_prime_left_esip_full_prime esi_prime_right_esip_full_prime. p = esi_prime_left_esip_full_prime * esi_prime_right_esip_full_prime -> esi_prime_left_esip_full_prime = 1 \/ esi_prime_right_esip_full_prime = 1)) -> ~(a = 0) -> (exists esip_gap_full_target_bound. esip_gap_full_target_bound + S (a) = p) -> exists b c. (forall esip_index_full_result. (exists esip_gap_full_result_prefix_bound. esip_gap_full_result_prefix_bound + S (esip_index_full_result) = n) -> exists esip_mate_full_result. ((((exists ff_h_esip_full_result_entry. ff_h_esip_full_result_entry + S (esip_mate_full_result) = S ((S (esip_index_full_result)) * c)) /\ exists ff_q_esip_full_result_entry. b = ff_q_esip_full_result_entry * S ((S (esip_index_full_result)) * c) + (esip_mate_full_result))) /\ ((exists esip_gap_full_result_relation_index_bound. esip_gap_full_result_relation_index_bound + S (esip_index_full_result) = n) /\ ((((~((S esip_index_full_result) = 0) /\ (exists esip_gap_full_result_relation_scaled_left_bound. esip_gap_full_result_relation_scaled_left_bound + S (S esip_index_full_result) = p))) /\ (((~(esip_mate_full_result = 0) /\ (exists esip_gap_full_result_relation_scaled_right_bound. esip_gap_full_result_relation_scaled_right_bound + S (esip_mate_full_result) = p))) /\ (exists esi_mod_left_full_result_relation_scaled_mod esi_mod_right_full_result_relation_scaled_mod. ((S esip_index_full_result) * esip_mate_full_result) + p * esi_mod_left_full_result_relation_scaled_mod = (a) + p * esi_mod_right_full_result_relation_scaled_mod)))))))

Structural proof guide

Generated structural guide

A prime predecessor interval has a full beta-coded scaled-inverse map.

Use the direct prerequisites le_refl, prime_scaled_inverse_prefix_exists_bounded as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA001A le_refl PA008S prime_scaled_inverse_prefix_exists_bounded

Proof neighborhood

Direct dependencies

PA001A le_refl PA008S prime_scaled_inverse_prefix_exists_bounded

Direct dependents

PA00BM quadratic_nonresidue_half_power_mod_predecessor

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

18 script commands · 3 reading checkpoints · 0 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 (2)
le reflprime scaled inverse prefix exists bounded
01Fix variables and assumptionsL1–7

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 hpn
  5. L5
    intro hp
  6. L6
    intro ha0
  7. L7
    intro hap
02Use earlier factsL8–17

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

  1. L8
    specialize prime_scaled_inverse_prefix_exists_bounded p
  2. L9
    specialize prime_scaled_inverse_prefix_exists_bounded a
  3. L10
    specialize prime_scaled_inverse_prefix_exists_bounded n
  4. L11
    specialize prime_scaled_inverse_prefix_exists_bounded n
  5. L12
    apply prime_scaled_inverse_prefix_exists_bounded
  6. L13
    exact hpn
  7. L14
    exact hp
  8. L15
    exact ha0
  9. L16
    exact hap
  10. L17
    specialize le_refl n
03Use earlier factsL18–18

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

  1. L18
    exact le_refl

Library-wide reading audit

Original exact command ledger · 18 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro hpn
  5. 0005intro hp
  6. 0006intro ha0
  7. 0007intro hap
  8. 0008specialize prime_scaled_inverse_prefix_exists_bounded p
  9. 0009specialize prime_scaled_inverse_prefix_exists_bounded a
  10. 0010specialize prime_scaled_inverse_prefix_exists_bounded n
  11. 0011specialize prime_scaled_inverse_prefix_exists_bounded n
  12. 0012apply prime_scaled_inverse_prefix_exists_bounded
  13. 0013exact hpn
  14. 0014exact hp
  15. 0015exact ha0
  16. 0016exact hap
  17. 0017specialize le_refl n
  18. 0018exact le_refl