SK0012

power_one_base_value

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

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

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.

For n>1 the exponent gcd and a real beta table classify and witness all positive root degrees. The unit n=1 has a separate uniform certificate for every positive degree. Zero is excluded. NaturalSquarefreeDecomposition is deliberately distinct from the unrelated polynomial definition.

Exact theorem in conservative defined notation

∀ k. ∀ z. Pow(1,k,z) → z = 1

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Pow(a,e,z) · 2

Actual proof prerequisites

pow_zero · checked external prerequisitepow_successor_decompose · checked external prerequisitemul_one · checked external prerequisite
Original expanded first-order 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

Complete tactic proof in conservative notation

All 31 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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(1,k,r)Original native command in the exact edition
  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 defined 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 : ∃ r. Pow(1,k,r) ∧ 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