PA0088

pow_congruent_base_witness

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

A congruent base has a relational power congruent to the supplied power.

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 r h A. (exists wpp_mod_left_eca_power_base_mod wpp_mod_right_eca_power_base_mod. (a) + p * wpp_mod_left_eca_power_base_mod = (r) + p * wpp_mod_right_eca_power_base_mod) -> (exists ff_b_eca_power_a ff_c_eca_power_a. ((forall ff_i_eca_power_a_repeat. (exists ff_lt_eca_power_a_repeat_bound. ff_lt_eca_power_a_repeat_bound + S ff_i_eca_power_a_repeat = h) -> (((exists ff_h_eca_power_a_repeat_decoded. ff_h_eca_power_a_repeat_decoded + S (a) = S ((S (ff_i_eca_power_a_repeat)) * ff_c_eca_power_a)) /\ exists ff_q_eca_power_a_repeat_decoded. ff_b_eca_power_a = ff_q_eca_power_a_repeat_decoded * S ((S (ff_i_eca_power_a_repeat)) * ff_c_eca_power_a) + (a)))) /\ (exists ff_u_eca_power_a_product ff_v_eca_power_a_product. ((((exists ff_h_eca_power_a_product_start. ff_h_eca_power_a_product_start + S (1) = S ((S (0)) * ff_v_eca_power_a_product)) /\ exists ff_q_eca_power_a_product_start. ff_u_eca_power_a_product = ff_q_eca_power_a_product_start * S ((S (0)) * ff_v_eca_power_a_product) + (1))) /\ ((((exists ff_h_eca_power_a_product_terminal. ff_h_eca_power_a_product_terminal + S (A) = S ((S (h)) * ff_v_eca_power_a_product)) /\ exists ff_q_eca_power_a_product_terminal. ff_u_eca_power_a_product = ff_q_eca_power_a_product_terminal * S ((S (h)) * ff_v_eca_power_a_product) + (A))) /\ forall ff_i_eca_power_a_product. (exists ff_lt_eca_power_a_product_bound. ff_lt_eca_power_a_product_bound + S ff_i_eca_power_a_product = h) -> exists ff_p_eca_power_a_product ff_r_eca_power_a_product ff_s_eca_power_a_product. ((((exists ff_h_eca_power_a_product_factor. ff_h_eca_power_a_product_factor + S (ff_p_eca_power_a_product) = S ((S (ff_i_eca_power_a_product)) * ff_c_eca_power_a)) /\ exists ff_q_eca_power_a_product_factor. ff_b_eca_power_a = ff_q_eca_power_a_product_factor * S ((S (ff_i_eca_power_a_product)) * ff_c_eca_power_a) + (ff_p_eca_power_a_product))) /\ ((((exists ff_h_eca_power_a_product_partial. ff_h_eca_power_a_product_partial + S (ff_r_eca_power_a_product) = S ((S (ff_i_eca_power_a_product)) * ff_v_eca_power_a_product)) /\ exists ff_q_eca_power_a_product_partial. ff_u_eca_power_a_product = ff_q_eca_power_a_product_partial * S ((S (ff_i_eca_power_a_product)) * ff_v_eca_power_a_product) + (ff_r_eca_power_a_product))) /\ ((((exists ff_h_eca_power_a_product_successor. ff_h_eca_power_a_product_successor + S (ff_s_eca_power_a_product) = S ((S (S ff_i_eca_power_a_product)) * ff_v_eca_power_a_product)) /\ exists ff_q_eca_power_a_product_successor. ff_u_eca_power_a_product = ff_q_eca_power_a_product_successor * S ((S (S ff_i_eca_power_a_product)) * ff_v_eca_power_a_product) + (ff_s_eca_power_a_product))) /\ ff_s_eca_power_a_product = ff_r_eca_power_a_product * ff_p_eca_power_a_product)))))))) -> (exists R. (exists ff_b_eca_power_r ff_c_eca_power_r. ((forall ff_i_eca_power_r_repeat. (exists ff_lt_eca_power_r_repeat_bound. ff_lt_eca_power_r_repeat_bound + S ff_i_eca_power_r_repeat = h) -> (((exists ff_h_eca_power_r_repeat_decoded. ff_h_eca_power_r_repeat_decoded + S (r) = S ((S (ff_i_eca_power_r_repeat)) * ff_c_eca_power_r)) /\ exists ff_q_eca_power_r_repeat_decoded. ff_b_eca_power_r = ff_q_eca_power_r_repeat_decoded * S ((S (ff_i_eca_power_r_repeat)) * ff_c_eca_power_r) + (r)))) /\ (exists ff_u_eca_power_r_product ff_v_eca_power_r_product. ((((exists ff_h_eca_power_r_product_start. ff_h_eca_power_r_product_start + S (1) = S ((S (0)) * ff_v_eca_power_r_product)) /\ exists ff_q_eca_power_r_product_start. ff_u_eca_power_r_product = ff_q_eca_power_r_product_start * S ((S (0)) * ff_v_eca_power_r_product) + (1))) /\ ((((exists ff_h_eca_power_r_product_terminal. ff_h_eca_power_r_product_terminal + S (R) = S ((S (h)) * ff_v_eca_power_r_product)) /\ exists ff_q_eca_power_r_product_terminal. ff_u_eca_power_r_product = ff_q_eca_power_r_product_terminal * S ((S (h)) * ff_v_eca_power_r_product) + (R))) /\ forall ff_i_eca_power_r_product. (exists ff_lt_eca_power_r_product_bound. ff_lt_eca_power_r_product_bound + S ff_i_eca_power_r_product = h) -> exists ff_p_eca_power_r_product ff_r_eca_power_r_product ff_s_eca_power_r_product. ((((exists ff_h_eca_power_r_product_factor. ff_h_eca_power_r_product_factor + S (ff_p_eca_power_r_product) = S ((S (ff_i_eca_power_r_product)) * ff_c_eca_power_r)) /\ exists ff_q_eca_power_r_product_factor. ff_b_eca_power_r = ff_q_eca_power_r_product_factor * S ((S (ff_i_eca_power_r_product)) * ff_c_eca_power_r) + (ff_p_eca_power_r_product))) /\ ((((exists ff_h_eca_power_r_product_partial. ff_h_eca_power_r_product_partial + S (ff_r_eca_power_r_product) = S ((S (ff_i_eca_power_r_product)) * ff_v_eca_power_r_product)) /\ exists ff_q_eca_power_r_product_partial. ff_u_eca_power_r_product = ff_q_eca_power_r_product_partial * S ((S (ff_i_eca_power_r_product)) * ff_v_eca_power_r_product) + (ff_r_eca_power_r_product))) /\ ((((exists ff_h_eca_power_r_product_successor. ff_h_eca_power_r_product_successor + S (ff_s_eca_power_r_product) = S ((S (S ff_i_eca_power_r_product)) * ff_v_eca_power_r_product)) /\ exists ff_q_eca_power_r_product_successor. ff_u_eca_power_r_product = ff_q_eca_power_r_product_successor * S ((S (S ff_i_eca_power_r_product)) * ff_v_eca_power_r_product) + (ff_s_eca_power_r_product))) /\ ff_s_eca_power_r_product = ff_r_eca_power_r_product * ff_p_eca_power_r_product)))))))) /\ (exists wpp_mod_left_eca_power_result_mod wpp_mod_right_eca_power_result_mod. (A) + p * wpp_mod_left_eca_power_result_mod = (R) + p * wpp_mod_right_eca_power_result_mod))

Structural proof guide

Generated structural guide

A congruent base has a relational power congruent to the supplied power.

Use the direct prerequisites pow_exists, pow_mod_congruent as previously established PA formulas.

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

Referenced ingredients

PA0046 pow_exists PA005I pow_mod_congruent

Proof neighborhood

Direct dependencies

PA0046 pow_exists PA005I pow_mod_congruent

Direct dependents

PA00BR arbitrary_euler_criterion_residue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff

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

25 script commands · 7 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 (2)
pow existspow mod congruent

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 r
  4. L4
    intro h
  5. L5
    intro A
  6. L6
    intro har
  7. L7
    intro hpower
02Establish hrpowerL8–11

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

  1. L8
    have hrpower : ∃ R. Pow(r,h,R)Definitions: Pow
  2. L9
    specialize pow_exists r
  3. L10
    specialize pow_exists h
  4. L11
    exact pow_exists
03Separate the logical casesL12–12

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

  1. L12
    cases hrpower
04Construct an explicit witnessL13–13

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

  1. L13
    exists x
05Separate the logical casesL14–14

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

  1. L14
    split
06Use earlier factsL15–24

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

  1. L15
    exact hrpower_witness
  2. L16
    specialize pow_mod_congruent p
  3. L17
    specialize pow_mod_congruent a
  4. L18
    specialize pow_mod_congruent r
  5. L19
    specialize pow_mod_congruent h
  6. L20
    specialize pow_mod_congruent A
  7. L21
    specialize pow_mod_congruent x
  8. L22
    apply pow_mod_congruent
  9. L23
    exact har
  10. L24
    exact hpower
07Use earlier factsL25–25

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

  1. L25
    exact hrpower_witness

Library-wide reading audit

Original exact command ledger · 25 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro r
  4. 0004intro h
  5. 0005intro A
  6. 0006intro har
  7. 0007intro hpower
  8. 0008have hrpower : exists R. (exists ff_b_eca_power_proof_exists ff_c_eca_power_proof_exists. ((forall ff_i_eca_power_proof_exists_repeat. (exists ff_lt_eca_power_proof_exists_repeat_bound. ff_lt_eca_power_proof_exists_repeat_bound + S ff_i_eca_power_proof_exists_repeat = h) -> (((exists ff_h_eca_power_proof_exists_repeat_decoded. ff_h_eca_power_proof_exists_repeat_decoded + S (r) = S ((S (ff_i_eca_power_proof_exists_repeat)) * ff_c_eca_power_proof_exists)) /\ exists ff_q_eca_power_proof_exists_repeat_decoded. ff_b_eca_power_proof_exists = ff_q_eca_power_proof_exists_repeat_decoded * S ((S (ff_i_eca_power_proof_exists_repeat)) * ff_c_eca_power_proof_exists) + (r)))) /\ (exists ff_u_eca_power_proof_exists_product ff_v_eca_power_proof_exists_product. ((((exists ff_h_eca_power_proof_exists_product_start. ff_h_eca_power_proof_exists_product_start + S (1) = S ((S (0)) * ff_v_eca_power_proof_exists_product)) /\ exists ff_q_eca_power_proof_exists_product_start. ff_u_eca_power_proof_exists_product = ff_q_eca_power_proof_exists_product_start * S ((S (0)) * ff_v_eca_power_proof_exists_product) + (1))) /\ ((((exists ff_h_eca_power_proof_exists_product_terminal. ff_h_eca_power_proof_exists_product_terminal + S (R) = S ((S (h)) * ff_v_eca_power_proof_exists_product)) /\ exists ff_q_eca_power_proof_exists_product_terminal. ff_u_eca_power_proof_exists_product = ff_q_eca_power_proof_exists_product_terminal * S ((S (h)) * ff_v_eca_power_proof_exists_product) + (R))) /\ forall ff_i_eca_power_proof_exists_product. (exists ff_lt_eca_power_proof_exists_product_bound. ff_lt_eca_power_proof_exists_product_bound + S ff_i_eca_power_proof_exists_product = h) -> exists ff_p_eca_power_proof_exists_product ff_r_eca_power_proof_exists_product ff_s_eca_power_proof_exists_product. ((((exists ff_h_eca_power_proof_exists_product_factor. ff_h_eca_power_proof_exists_product_factor + S (ff_p_eca_power_proof_exists_product) = S ((S (ff_i_eca_power_proof_exists_product)) * ff_c_eca_power_proof_exists)) /\ exists ff_q_eca_power_proof_exists_product_factor. ff_b_eca_power_proof_exists = ff_q_eca_power_proof_exists_product_factor * S ((S (ff_i_eca_power_proof_exists_product)) * ff_c_eca_power_proof_exists) + (ff_p_eca_power_proof_exists_product))) /\ ((((exists ff_h_eca_power_proof_exists_product_partial. ff_h_eca_power_proof_exists_product_partial + S (ff_r_eca_power_proof_exists_product) = S ((S (ff_i_eca_power_proof_exists_product)) * ff_v_eca_power_proof_exists_product)) /\ exists ff_q_eca_power_proof_exists_product_partial. ff_u_eca_power_proof_exists_product = ff_q_eca_power_proof_exists_product_partial * S ((S (ff_i_eca_power_proof_exists_product)) * ff_v_eca_power_proof_exists_product) + (ff_r_eca_power_proof_exists_product))) /\ ((((exists ff_h_eca_power_proof_exists_product_successor. ff_h_eca_power_proof_exists_product_successor + S (ff_s_eca_power_proof_exists_product) = S ((S (S ff_i_eca_power_proof_exists_product)) * ff_v_eca_power_proof_exists_product)) /\ exists ff_q_eca_power_proof_exists_product_successor. ff_u_eca_power_proof_exists_product = ff_q_eca_power_proof_exists_product_successor * S ((S (S ff_i_eca_power_proof_exists_product)) * ff_v_eca_power_proof_exists_product) + (ff_s_eca_power_proof_exists_product))) /\ ff_s_eca_power_proof_exists_product = ff_r_eca_power_proof_exists_product * ff_p_eca_power_proof_exists_product))))))))
  9. 0009specialize pow_exists r
  10. 0010specialize pow_exists h
  11. 0011exact pow_exists
  12. 0012cases hrpower
  13. 0013exists x
  14. 0014split
  15. 0015exact hrpower_witness
  16. 0016specialize pow_mod_congruent p
  17. 0017specialize pow_mod_congruent a
  18. 0018specialize pow_mod_congruent r
  19. 0019specialize pow_mod_congruent h
  20. 0020specialize pow_mod_congruent A
  21. 0021specialize pow_mod_congruent x
  22. 0022apply pow_mod_congruent
  23. 0023exact har
  24. 0024exact hpower
  25. 0025exact hrpower_witness