BT00U1 · Bertrand theorem

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.

Statement with defined notation

∀ p. Pow(4,4,p) → p = 4 · 4 · 4 · 4

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0020 Pow

1 occurrences

In local proof propositions

PD0020 Pow

2 occurrences

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

Proof neighborhood

Direct theorem prerequisites

BT0083 pow_successor_decompose BT009W pow_two

Direct theorem dependents

BT00U3 four_pow_central_seed_package

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

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.

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)
pow successor decomposepow two
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(4,3,r)Original native command in the exact edition
  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(4,2,r)Original native command in the exact edition
  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 defined command ledger · 22 lines
  1. 0001intro p
  2. 0002intro hpower
  3. 0003have hthree : ∃ r. Pow(4,3,r) ∧ p = r · 4
    Exact native replay linehave 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 : ∃ r. Pow(4,2,r) ∧ x = r · 4
    Exact native replay linehave 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