SK0012

power_one_base_value

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every nonnegative power of the unit has value one, proved by ordinary exponent induction.

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 first-order arithmetic statement

forall k z. (exists pa_b_pvs_one_base pa_c_pvs_one_base. ((forall pa_i_pvs_one_base_repeat. (exists pa_lt_pvs_one_base_repeat_bound. pa_lt_pvs_one_base_repeat_bound + S pa_i_pvs_one_base_repeat = k) -> (((exists pa_h_pvs_one_base_repeat_decoded. pa_h_pvs_one_base_repeat_decoded + S (1) = S ((S (pa_i_pvs_one_base_repeat)) * pa_c_pvs_one_base)) /\ exists pa_q_pvs_one_base_repeat_decoded. pa_b_pvs_one_base = pa_q_pvs_one_base_repeat_decoded * S ((S (pa_i_pvs_one_base_repeat)) * pa_c_pvs_one_base) + (1)))) /\ (exists pa_u_pvs_one_base_product pa_v_pvs_one_base_product. ((((exists pa_h_pvs_one_base_product_start. pa_h_pvs_one_base_product_start + S (1) = S ((S (0)) * pa_v_pvs_one_base_product)) /\ exists pa_q_pvs_one_base_product_start. pa_u_pvs_one_base_product = pa_q_pvs_one_base_product_start * S ((S (0)) * pa_v_pvs_one_base_product) + (1))) /\ ((((exists pa_h_pvs_one_base_product_terminal. pa_h_pvs_one_base_product_terminal + S (z) = S ((S (k)) * pa_v_pvs_one_base_product)) /\ exists pa_q_pvs_one_base_product_terminal. pa_u_pvs_one_base_product = pa_q_pvs_one_base_product_terminal * S ((S (k)) * pa_v_pvs_one_base_product) + (z))) /\ forall pa_i_pvs_one_base_product. (exists pa_lt_pvs_one_base_product_bound. pa_lt_pvs_one_base_product_bound + S pa_i_pvs_one_base_product = k) -> exists pa_p_pvs_one_base_product pa_r_pvs_one_base_product pa_s_pvs_one_base_product. ((((exists pa_h_pvs_one_base_product_factor. pa_h_pvs_one_base_product_factor + S (pa_p_pvs_one_base_product) = S ((S (pa_i_pvs_one_base_product)) * pa_c_pvs_one_base)) /\ exists pa_q_pvs_one_base_product_factor. pa_b_pvs_one_base = pa_q_pvs_one_base_product_factor * S ((S (pa_i_pvs_one_base_product)) * pa_c_pvs_one_base) + (pa_p_pvs_one_base_product))) /\ ((((exists pa_h_pvs_one_base_product_partial. pa_h_pvs_one_base_product_partial + S (pa_r_pvs_one_base_product) = S ((S (pa_i_pvs_one_base_product)) * pa_v_pvs_one_base_product)) /\ exists pa_q_pvs_one_base_product_partial. pa_u_pvs_one_base_product = pa_q_pvs_one_base_product_partial * S ((S (pa_i_pvs_one_base_product)) * pa_v_pvs_one_base_product) + (pa_r_pvs_one_base_product))) /\ ((((exists pa_h_pvs_one_base_product_successor. pa_h_pvs_one_base_product_successor + S (pa_s_pvs_one_base_product) = S ((S (S pa_i_pvs_one_base_product)) * pa_v_pvs_one_base_product)) /\ exists pa_q_pvs_one_base_product_successor. pa_u_pvs_one_base_product = pa_q_pvs_one_base_product_successor * S ((S (S pa_i_pvs_one_base_product)) * pa_v_pvs_one_base_product) + (pa_s_pvs_one_base_product))) /\ pa_s_pvs_one_base_product = pa_r_pvs_one_base_product * pa_p_pvs_one_base_product)))))))) -> z = 1

Constructive proof overview

Generated structural guide

Every nonnegative power of the unit has value one, proved by ordinary exponent induction.

The unchanged tactic script uses 3 declared prerequisites and contains 31 exact native proof lines.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

pow_zero Stable theorem; checked-use authorized pow_successor_decompose Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized

Direct dependents

SK0013 power_one_base_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

31 script commands · 6 reading checkpoints · 2 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.

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

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

  1. L1
    intro k
02Induction on kL2–11

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction k
  2. L3
    intro z
  3. L4
    intro hpow
  4. L5
    specialize pow_zero (1)
  5. L6
    specialize pow_zero (0)
  6. L7
    specialize pow_zero (z)
  7. L8
    apply pow_zero
  8. L9
    refl
  9. L10
    exact hpow
  10. L11
    intro z
03Fix variables and assumptionsL12–12

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

  1. L12
    intro hpow
04Establish hprevL13–20

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

  1. L13
    have hprev : ∃ r. Pow(1,k,r) ∧ z = r · 1Definitions: Pow
  2. L14
    specialize pow_successor_decompose (1)
  3. L15
    specialize pow_successor_decompose (k)
  4. L16
    specialize pow_successor_decompose (S k)
  5. L17
    specialize pow_successor_decompose (z)
  6. L18
    apply pow_successor_decompose
  7. L19
    refl
  8. L20
    exact hpow
05Separate the logical casesL21–22

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

  1. L21
    cases hprev
  2. L22
    cases hprev_witness
06Establish honeL23–31

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

  1. L23
    have hone : x = 1
  2. L24
    specialize IH (x)
  3. L25
    apply IH
  4. L26
    exact hprev_witness_left
  5. L27
    trans x * 1
  6. L28
    exact hprev_witness_right
  7. L29
    trans x
  8. L30
    apply mul_one
  9. L31
    exact hone

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro k
  2. 0002induction k
  3. 0003intro z
  4. 0004intro hpow
  5. 0005specialize pow_zero (1)
  6. 0006specialize pow_zero (0)
  7. 0007specialize pow_zero (z)
  8. 0008apply pow_zero
  9. 0009refl
  10. 0010exact hpow
  11. 0011intro z
  12. 0012intro hpow
  13. 0013have hprev : exists r. (exists pa_b_pvs_one_previous pa_c_pvs_one_previous. ((forall pa_i_pvs_one_previous_repeat. (exists pa_lt_pvs_one_previous_repeat_bound. pa_lt_pvs_one_previous_repeat_bound + S pa_i_pvs_one_previous_repeat = k) -> (((exists pa_h_pvs_one_previous_repeat_decoded. pa_h_pvs_one_previous_repeat_decoded + S (1) = S ((S (pa_i_pvs_one_previous_repeat)) * pa_c_pvs_one_previous)) /\ exists pa_q_pvs_one_previous_repeat_decoded. pa_b_pvs_one_previous = pa_q_pvs_one_previous_repeat_decoded * S ((S (pa_i_pvs_one_previous_repeat)) * pa_c_pvs_one_previous) + (1)))) /\ (exists pa_u_pvs_one_previous_product pa_v_pvs_one_previous_product. ((((exists pa_h_pvs_one_previous_product_start. pa_h_pvs_one_previous_product_start + S (1) = S ((S (0)) * pa_v_pvs_one_previous_product)) /\ exists pa_q_pvs_one_previous_product_start. pa_u_pvs_one_previous_product = pa_q_pvs_one_previous_product_start * S ((S (0)) * pa_v_pvs_one_previous_product) + (1))) /\ ((((exists pa_h_pvs_one_previous_product_terminal. pa_h_pvs_one_previous_product_terminal + S (r) = S ((S (k)) * pa_v_pvs_one_previous_product)) /\ exists pa_q_pvs_one_previous_product_terminal. pa_u_pvs_one_previous_product = pa_q_pvs_one_previous_product_terminal * S ((S (k)) * pa_v_pvs_one_previous_product) + (r))) /\ forall pa_i_pvs_one_previous_product. (exists pa_lt_pvs_one_previous_product_bound. pa_lt_pvs_one_previous_product_bound + S pa_i_pvs_one_previous_product = k) -> exists pa_p_pvs_one_previous_product pa_r_pvs_one_previous_product pa_s_pvs_one_previous_product. ((((exists pa_h_pvs_one_previous_product_factor. pa_h_pvs_one_previous_product_factor + S (pa_p_pvs_one_previous_product) = S ((S (pa_i_pvs_one_previous_product)) * pa_c_pvs_one_previous)) /\ exists pa_q_pvs_one_previous_product_factor. pa_b_pvs_one_previous = pa_q_pvs_one_previous_product_factor * S ((S (pa_i_pvs_one_previous_product)) * pa_c_pvs_one_previous) + (pa_p_pvs_one_previous_product))) /\ ((((exists pa_h_pvs_one_previous_product_partial. pa_h_pvs_one_previous_product_partial + S (pa_r_pvs_one_previous_product) = S ((S (pa_i_pvs_one_previous_product)) * pa_v_pvs_one_previous_product)) /\ exists pa_q_pvs_one_previous_product_partial. pa_u_pvs_one_previous_product = pa_q_pvs_one_previous_product_partial * S ((S (pa_i_pvs_one_previous_product)) * pa_v_pvs_one_previous_product) + (pa_r_pvs_one_previous_product))) /\ ((((exists pa_h_pvs_one_previous_product_successor. pa_h_pvs_one_previous_product_successor + S (pa_s_pvs_one_previous_product) = S ((S (S pa_i_pvs_one_previous_product)) * pa_v_pvs_one_previous_product)) /\ exists pa_q_pvs_one_previous_product_successor. pa_u_pvs_one_previous_product = pa_q_pvs_one_previous_product_successor * S ((S (S pa_i_pvs_one_previous_product)) * pa_v_pvs_one_previous_product) + (pa_s_pvs_one_previous_product))) /\ pa_s_pvs_one_previous_product = pa_r_pvs_one_previous_product * pa_p_pvs_one_previous_product)))))))) /\ z = r * 1
  14. 0014specialize pow_successor_decompose (1)
  15. 0015specialize pow_successor_decompose (k)
  16. 0016specialize pow_successor_decompose (S k)
  17. 0017specialize pow_successor_decompose (z)
  18. 0018apply pow_successor_decompose
  19. 0019refl
  20. 0020exact hpow
  21. 0021cases hprev
  22. 0022cases hprev_witness
  23. 0023have hone : x = 1
  24. 0024specialize IH (x)
  25. 0025apply IH
  26. 0026exact hprev_witness_left
  27. 0027trans x * 1
  28. 0028exact hprev_witness_right
  29. 0029trans x
  30. 0030apply mul_one
  31. 0031exact hone