PA008T · theorem

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.

Statement with defined notation

∀ p. ∀ a. ∀ n. p = S n → Prime(p) → ¬a = 0 → Lt(a,p) → ∃ x. ∃ y. ScaledInversePrefix(p,a,n,x,y,n)

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 PD0004 Prime PD0039 ScaledInversePrefix

3 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-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)))))))

Proof neighborhood

Direct theorem prerequisites

PA001A le_refl PA008S prime_scaled_inverse_prefix_exists_bounded

Direct theorem dependents

PA00BM quadratic_nonresidue_half_power_mod_predecessor

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

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.

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)
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 defined 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