BT00U1

pow_four_four_exact

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A relational fourth power of four is the fourfold product.

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. (exists pa_b_bpf4e_source pa_c_bpf4e_source. ((forall pa_i_bpf4e_source_repeat. (exists pa_lt_bpf4e_source_repeat_bound. pa_lt_bpf4e_source_repeat_bound + S pa_i_bpf4e_source_repeat = 4) -> (((exists pa_h_bpf4e_source_repeat_decoded. pa_h_bpf4e_source_repeat_decoded + S (4) = S ((S (pa_i_bpf4e_source_repeat)) * pa_c_bpf4e_source)) /\ exists pa_q_bpf4e_source_repeat_decoded. pa_b_bpf4e_source = pa_q_bpf4e_source_repeat_decoded * S ((S (pa_i_bpf4e_source_repeat)) * pa_c_bpf4e_source) + (4)))) /\ (exists pa_u_bpf4e_source_product pa_v_bpf4e_source_product. ((((exists pa_h_bpf4e_source_product_start. pa_h_bpf4e_source_product_start + S (1) = S ((S (0)) * pa_v_bpf4e_source_product)) /\ exists pa_q_bpf4e_source_product_start. pa_u_bpf4e_source_product = pa_q_bpf4e_source_product_start * S ((S (0)) * pa_v_bpf4e_source_product) + (1))) /\ ((((exists pa_h_bpf4e_source_product_terminal. pa_h_bpf4e_source_product_terminal + S (p) = S ((S (4)) * pa_v_bpf4e_source_product)) /\ exists pa_q_bpf4e_source_product_terminal. pa_u_bpf4e_source_product = pa_q_bpf4e_source_product_terminal * S ((S (4)) * pa_v_bpf4e_source_product) + (p))) /\ forall pa_i_bpf4e_source_product. (exists pa_lt_bpf4e_source_product_bound. pa_lt_bpf4e_source_product_bound + S pa_i_bpf4e_source_product = 4) -> exists pa_p_bpf4e_source_product pa_r_bpf4e_source_product pa_s_bpf4e_source_product. ((((exists pa_h_bpf4e_source_product_factor. pa_h_bpf4e_source_product_factor + S (pa_p_bpf4e_source_product) = S ((S (pa_i_bpf4e_source_product)) * pa_c_bpf4e_source)) /\ exists pa_q_bpf4e_source_product_factor. pa_b_bpf4e_source = pa_q_bpf4e_source_product_factor * S ((S (pa_i_bpf4e_source_product)) * pa_c_bpf4e_source) + (pa_p_bpf4e_source_product))) /\ ((((exists pa_h_bpf4e_source_product_partial. pa_h_bpf4e_source_product_partial + S (pa_r_bpf4e_source_product) = S ((S (pa_i_bpf4e_source_product)) * pa_v_bpf4e_source_product)) /\ exists pa_q_bpf4e_source_product_partial. pa_u_bpf4e_source_product = pa_q_bpf4e_source_product_partial * S ((S (pa_i_bpf4e_source_product)) * pa_v_bpf4e_source_product) + (pa_r_bpf4e_source_product))) /\ ((((exists pa_h_bpf4e_source_product_successor. pa_h_bpf4e_source_product_successor + S (pa_s_bpf4e_source_product) = S ((S (S pa_i_bpf4e_source_product)) * pa_v_bpf4e_source_product)) /\ exists pa_q_bpf4e_source_product_successor. pa_u_bpf4e_source_product = pa_q_bpf4e_source_product_successor * S ((S (S pa_i_bpf4e_source_product)) * pa_v_bpf4e_source_product) + (pa_s_bpf4e_source_product))) /\ pa_s_bpf4e_source_product = pa_r_bpf4e_source_product * pa_p_bpf4e_source_product)))))))) -> p = ((4 * 4) * 4) * 4

Structural proof guide

A relational fourth power of four is the fourfold product.

Direct prerequisites: pow_successor_decompose, pow_two. The authored body proceeds by case analysis (4), intermediate claims (3), equality transport (3).

Proof neighborhood

Direct dependencies

BT0083 pow_successor_decompose BT009W pow_two

Direct dependents

BT00U3 four_pow_central_seed_package

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

22 script commands · 6 reading checkpoints · 3 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 successor decomposepow two

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–2

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

  1. L1
    intro p
  2. L2
    intro hpower
02Establish hthreeL3–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor decompose.

  1. L3
    have hthree : ∃ r. Pow(4,3,r) ∧ p = r · 4Definitions: Pow
  2. L4
    apply pow_successor_decompose
  3. L5
    refl
  4. L6
    exact hpower
03Separate the logical casesL7–8

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

  1. L7
    cases hthree
  2. L8
    cases hthree_witness
04Establish htwoL9–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor decompose.

  1. L9
    have htwo : ∃ r. Pow(4,2,r) ∧ x = r · 4Definitions: Pow
  2. L10
    apply pow_successor_decompose
  3. L11
    refl
  4. L12
    exact hthree_witness_left
05Separate the logical casesL13–14

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

  1. L13
    cases htwo
  2. L14
    cases htwo_witness
06Establish htwo_valueL15–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow two.

  1. L15
    have htwo_value : x1 = 4 * 4
  2. L16
    apply pow_two
  3. L17
    refl
  4. L18
    exact htwo_witness_left
  5. L19
    rewrite hthree_witness_right
  6. L20
    rewrite htwo_witness_right
  7. L21
    rewrite htwo_value
  8. L22
    refl

Library-wide reading audit

Original exact command ledger · 22 lines
  1. 0001intro p
  2. 0002intro hpower
  3. 0003have hthree : exists r. (exists pa_b_bpf4e_three pa_c_bpf4e_three. ((forall pa_i_bpf4e_three_repeat. (exists pa_lt_bpf4e_three_repeat_bound. pa_lt_bpf4e_three_repeat_bound + S pa_i_bpf4e_three_repeat = 3) -> (((exists pa_h_bpf4e_three_repeat_decoded. pa_h_bpf4e_three_repeat_decoded + S (4) = S ((S (pa_i_bpf4e_three_repeat)) * pa_c_bpf4e_three)) /\ exists pa_q_bpf4e_three_repeat_decoded. pa_b_bpf4e_three = pa_q_bpf4e_three_repeat_decoded * S ((S (pa_i_bpf4e_three_repeat)) * pa_c_bpf4e_three) + (4)))) /\ (exists pa_u_bpf4e_three_product pa_v_bpf4e_three_product. ((((exists pa_h_bpf4e_three_product_start. pa_h_bpf4e_three_product_start + S (1) = S ((S (0)) * pa_v_bpf4e_three_product)) /\ exists pa_q_bpf4e_three_product_start. pa_u_bpf4e_three_product = pa_q_bpf4e_three_product_start * S ((S (0)) * pa_v_bpf4e_three_product) + (1))) /\ ((((exists pa_h_bpf4e_three_product_terminal. pa_h_bpf4e_three_product_terminal + S (r) = S ((S (3)) * pa_v_bpf4e_three_product)) /\ exists pa_q_bpf4e_three_product_terminal. pa_u_bpf4e_three_product = pa_q_bpf4e_three_product_terminal * S ((S (3)) * pa_v_bpf4e_three_product) + (r))) /\ forall pa_i_bpf4e_three_product. (exists pa_lt_bpf4e_three_product_bound. pa_lt_bpf4e_three_product_bound + S pa_i_bpf4e_three_product = 3) -> exists pa_p_bpf4e_three_product pa_r_bpf4e_three_product pa_s_bpf4e_three_product. ((((exists pa_h_bpf4e_three_product_factor. pa_h_bpf4e_three_product_factor + S (pa_p_bpf4e_three_product) = S ((S (pa_i_bpf4e_three_product)) * pa_c_bpf4e_three)) /\ exists pa_q_bpf4e_three_product_factor. pa_b_bpf4e_three = pa_q_bpf4e_three_product_factor * S ((S (pa_i_bpf4e_three_product)) * pa_c_bpf4e_three) + (pa_p_bpf4e_three_product))) /\ ((((exists pa_h_bpf4e_three_product_partial. pa_h_bpf4e_three_product_partial + S (pa_r_bpf4e_three_product) = S ((S (pa_i_bpf4e_three_product)) * pa_v_bpf4e_three_product)) /\ exists pa_q_bpf4e_three_product_partial. pa_u_bpf4e_three_product = pa_q_bpf4e_three_product_partial * S ((S (pa_i_bpf4e_three_product)) * pa_v_bpf4e_three_product) + (pa_r_bpf4e_three_product))) /\ ((((exists pa_h_bpf4e_three_product_successor. pa_h_bpf4e_three_product_successor + S (pa_s_bpf4e_three_product) = S ((S (S pa_i_bpf4e_three_product)) * pa_v_bpf4e_three_product)) /\ exists pa_q_bpf4e_three_product_successor. pa_u_bpf4e_three_product = pa_q_bpf4e_three_product_successor * S ((S (S pa_i_bpf4e_three_product)) * pa_v_bpf4e_three_product) + (pa_s_bpf4e_three_product))) /\ pa_s_bpf4e_three_product = pa_r_bpf4e_three_product * pa_p_bpf4e_three_product)))))))) /\ p = r * 4
  4. 0004apply pow_successor_decompose
  5. 0005refl
  6. 0006exact hpower
  7. 0007cases hthree
  8. 0008cases hthree_witness
  9. 0009have htwo : exists r. (exists pa_b_bpf4e_two pa_c_bpf4e_two. ((forall pa_i_bpf4e_two_repeat. (exists pa_lt_bpf4e_two_repeat_bound. pa_lt_bpf4e_two_repeat_bound + S pa_i_bpf4e_two_repeat = 2) -> (((exists pa_h_bpf4e_two_repeat_decoded. pa_h_bpf4e_two_repeat_decoded + S (4) = S ((S (pa_i_bpf4e_two_repeat)) * pa_c_bpf4e_two)) /\ exists pa_q_bpf4e_two_repeat_decoded. pa_b_bpf4e_two = pa_q_bpf4e_two_repeat_decoded * S ((S (pa_i_bpf4e_two_repeat)) * pa_c_bpf4e_two) + (4)))) /\ (exists pa_u_bpf4e_two_product pa_v_bpf4e_two_product. ((((exists pa_h_bpf4e_two_product_start. pa_h_bpf4e_two_product_start + S (1) = S ((S (0)) * pa_v_bpf4e_two_product)) /\ exists pa_q_bpf4e_two_product_start. pa_u_bpf4e_two_product = pa_q_bpf4e_two_product_start * S ((S (0)) * pa_v_bpf4e_two_product) + (1))) /\ ((((exists pa_h_bpf4e_two_product_terminal. pa_h_bpf4e_two_product_terminal + S (r) = S ((S (2)) * pa_v_bpf4e_two_product)) /\ exists pa_q_bpf4e_two_product_terminal. pa_u_bpf4e_two_product = pa_q_bpf4e_two_product_terminal * S ((S (2)) * pa_v_bpf4e_two_product) + (r))) /\ forall pa_i_bpf4e_two_product. (exists pa_lt_bpf4e_two_product_bound. pa_lt_bpf4e_two_product_bound + S pa_i_bpf4e_two_product = 2) -> exists pa_p_bpf4e_two_product pa_r_bpf4e_two_product pa_s_bpf4e_two_product. ((((exists pa_h_bpf4e_two_product_factor. pa_h_bpf4e_two_product_factor + S (pa_p_bpf4e_two_product) = S ((S (pa_i_bpf4e_two_product)) * pa_c_bpf4e_two)) /\ exists pa_q_bpf4e_two_product_factor. pa_b_bpf4e_two = pa_q_bpf4e_two_product_factor * S ((S (pa_i_bpf4e_two_product)) * pa_c_bpf4e_two) + (pa_p_bpf4e_two_product))) /\ ((((exists pa_h_bpf4e_two_product_partial. pa_h_bpf4e_two_product_partial + S (pa_r_bpf4e_two_product) = S ((S (pa_i_bpf4e_two_product)) * pa_v_bpf4e_two_product)) /\ exists pa_q_bpf4e_two_product_partial. pa_u_bpf4e_two_product = pa_q_bpf4e_two_product_partial * S ((S (pa_i_bpf4e_two_product)) * pa_v_bpf4e_two_product) + (pa_r_bpf4e_two_product))) /\ ((((exists pa_h_bpf4e_two_product_successor. pa_h_bpf4e_two_product_successor + S (pa_s_bpf4e_two_product) = S ((S (S pa_i_bpf4e_two_product)) * pa_v_bpf4e_two_product)) /\ exists pa_q_bpf4e_two_product_successor. pa_u_bpf4e_two_product = pa_q_bpf4e_two_product_successor * S ((S (S pa_i_bpf4e_two_product)) * pa_v_bpf4e_two_product) + (pa_s_bpf4e_two_product))) /\ pa_s_bpf4e_two_product = pa_r_bpf4e_two_product * pa_p_bpf4e_two_product)))))))) /\ x = r * 4
  10. 0010apply pow_successor_decompose
  11. 0011refl
  12. 0012exact hthree_witness_left
  13. 0013cases htwo
  14. 0014cases htwo_witness
  15. 0015have htwo_value : x1 = 4 * 4
  16. 0016apply pow_two
  17. 0017refl
  18. 0018exact htwo_witness_left
  19. 0019rewrite hthree_witness_right
  20. 0020rewrite htwo_witness_right
  21. 0021rewrite htwo_value
  22. 0022refl