AF000D

factor_permutation_empty_matching

The actual literal zero beta code is a bounded/injective/surjective matching permutation between any two empty factor prefixes.

Alpha v34 checked-use · first admitted v28 · 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.

The original division, gcd, cancellation, and factor-existence foundations are exposed through checked wrappers. Unordered uniqueness adds an actual bounded, injective, surjective index map matching repeated prime occurrences. The empty factor list represents one, not zero.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ d. ∀ e. PermutationPrefix(0,0,0) ∧ FactorListMatching(b,c,d,e,0,0,0)

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

Definition DAG

PermutationPrefix(b,c,l) · 1FactorListMatching(b,c,d,e,u,v,l) · 1

Actual proof prerequisites

factor_permutation_below_zero_impossible
Original expanded first-order statement 
forall b c d e. (((((forall pfp_i_emptypermutationbounded. (exists pfp_gap_emptypermutationboundedindex. pfp_gap_emptypermutationboundedindex + S (pfp_i_emptypermutationbounded) = (0)) -> exists pfp_a_emptypermutationbounded. (((exists ff_h_pfp_emptypermutationboundedentry. ff_h_pfp_emptypermutationboundedentry + S (pfp_a_emptypermutationbounded) = S ((S (pfp_i_emptypermutationbounded)) * 0)) /\ exists ff_q_pfp_emptypermutationboundedentry. 0 = ff_q_pfp_emptypermutationboundedentry * S ((S (pfp_i_emptypermutationbounded)) * 0) + (pfp_a_emptypermutationbounded))) /\ (exists pfp_gap_emptypermutationboundedvalue. pfp_gap_emptypermutationboundedvalue + S (pfp_a_emptypermutationbounded) = (0))) /\ (((forall pfp_i_emptypermutationinjective pfp_j_emptypermutationinjective pfp_a_emptypermutationinjective. (exists pfp_gap_emptypermutationinjectivefirst. pfp_gap_emptypermutationinjectivefirst + S (pfp_i_emptypermutationinjective) = (0)) -> (exists pfp_gap_emptypermutationinjectivesecond. pfp_gap_emptypermutationinjectivesecond + S (pfp_j_emptypermutationinjective) = (0)) -> (((exists ff_h_pfp_emptypermutationinjectiveleft. ff_h_pfp_emptypermutationinjectiveleft + S (pfp_a_emptypermutationinjective) = S ((S (pfp_i_emptypermutationinjective)) * 0)) /\ exists ff_q_pfp_emptypermutationinjectiveleft. 0 = ff_q_pfp_emptypermutationinjectiveleft * S ((S (pfp_i_emptypermutationinjective)) * 0) + (pfp_a_emptypermutationinjective))) -> (((exists ff_h_pfp_emptypermutationinjectiveright. ff_h_pfp_emptypermutationinjectiveright + S (pfp_a_emptypermutationinjective) = S ((S (pfp_j_emptypermutationinjective)) * 0)) /\ exists ff_q_pfp_emptypermutationinjectiveright. 0 = ff_q_pfp_emptypermutationinjectiveright * S ((S (pfp_j_emptypermutationinjective)) * 0) + (pfp_a_emptypermutationinjective))) -> pfp_i_emptypermutationinjective = pfp_j_emptypermutationinjective) /\ (forall pfp_a_emptypermutationsurjective. (exists pfp_gap_emptypermutationsurjectivevalue. pfp_gap_emptypermutationsurjectivevalue + S (pfp_a_emptypermutationsurjective) = (0)) -> exists pfp_i_emptypermutationsurjective. (exists pfp_gap_emptypermutationsurjectiveindex. pfp_gap_emptypermutationsurjectiveindex + S (pfp_i_emptypermutationsurjective) = (0)) /\ (((exists ff_h_pfp_emptypermutationsurjectiveentry. ff_h_pfp_emptypermutationsurjectiveentry + S (pfp_a_emptypermutationsurjective) = S ((S (pfp_i_emptypermutationsurjective)) * 0)) /\ exists ff_q_pfp_emptypermutationsurjectiveentry. 0 = ff_q_pfp_emptypermutationsurjectiveentry * S ((S (pfp_i_emptypermutationsurjective)) * 0) + (pfp_a_emptypermutationsurjective)))))))) /\ (forall pfp_i_emptymatching pfp_j_emptymatching pfp_a_emptymatching. (exists pfp_gap_emptymatchingbound. pfp_gap_emptymatchingbound + S (pfp_i_emptymatching) = (0)) -> (((exists ff_h_pfp_emptymatchingmap. ff_h_pfp_emptymatchingmap + S (pfp_j_emptymatching) = S ((S (pfp_i_emptymatching)) * 0)) /\ exists ff_q_pfp_emptymatchingmap. 0 = ff_q_pfp_emptymatchingmap * S ((S (pfp_i_emptymatching)) * 0) + (pfp_j_emptymatching))) -> (((exists ff_h_pfp_emptymatchingsource. ff_h_pfp_emptymatchingsource + S (pfp_a_emptymatching) = S ((S (pfp_i_emptymatching)) * c)) /\ exists ff_q_pfp_emptymatchingsource. b = ff_q_pfp_emptymatchingsource * S ((S (pfp_i_emptymatching)) * c) + (pfp_a_emptymatching))) -> (((exists ff_h_pfp_emptymatchingtarget. ff_h_pfp_emptymatchingtarget + S (pfp_a_emptymatching) = S ((S (pfp_j_emptymatching)) * e)) /\ exists ff_q_pfp_emptymatchingtarget. d = ff_q_pfp_emptymatchingtarget * S ((S (pfp_j_emptymatching)) * e) + (pfp_a_emptymatching))))))

Complete tactic proof in conservative notation

All 40 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

40 script commands · 15 reading checkpoints · 0 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 (1)
factor permutation below zero impossible
01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
02Separate the logical casesL5–6

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

  1. L5
    split
  2. L6
    split
03Fix variables and assumptionsL7–8

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

  1. L7
    intro i
  2. L8
    intro hi
04Separate the logical casesL9–9

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

  1. L9
    exfalso
05Use earlier factsL10–12

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

  1. L10
    specialize factor_permutation_below_zero_impossible (i)
  2. L11
    apply factor_permutation_below_zero_impossible
  3. L12
    exact hi
06Separate the logical casesL13–13

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

  1. L13
    split
07Fix variables and assumptionsL14–20

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

  1. L14
    intro i
  2. L15
    intro j
  3. L16
    intro a
  4. L17
    intro hi
  5. L18
    intro hj
  6. L19
    intro hfirst
  7. L20
    intro hsecond
08Separate the logical casesL21–21

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

  1. L21
    exfalso
09Use earlier factsL22–24

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

  1. L22
    specialize factor_permutation_below_zero_impossible (i)
  2. L23
    apply factor_permutation_below_zero_impossible
  3. L24
    exact hi
10Fix variables and assumptionsL25–26

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

  1. L25
    intro a
  2. L26
    intro ha
11Separate the logical casesL27–27

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

  1. L27
    exfalso
12Use earlier factsL28–30

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

  1. L28
    specialize factor_permutation_below_zero_impossible (a)
  2. L29
    apply factor_permutation_below_zero_impossible
  3. L30
    exact ha
13Fix variables and assumptionsL31–36

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

  1. L31
    intro i
  2. L32
    intro j
  3. L33
    intro a
  4. L34
    intro hi
  5. L35
    intro hmap
  6. L36
    intro hsource
14Separate the logical casesL37–37

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

  1. L37
    exfalso
15Use earlier factsL38–40

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

  1. L38
    specialize factor_permutation_below_zero_impossible (i)
  2. L39
    apply factor_permutation_below_zero_impossible
  3. L40
    exact hi

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005split
  6. 0006split
  7. 0007intro i
  8. 0008intro hi
  9. 0009exfalso
  10. 0010specialize factor_permutation_below_zero_impossible (i)
  11. 0011apply factor_permutation_below_zero_impossible
  12. 0012exact hi
  13. 0013split
  14. 0014intro i
  15. 0015intro j
  16. 0016intro a
  17. 0017intro hi
  18. 0018intro hj
  19. 0019intro hfirst
  20. 0020intro hsecond
  21. 0021exfalso
  22. 0022specialize factor_permutation_below_zero_impossible (i)
  23. 0023apply factor_permutation_below_zero_impossible
  24. 0024exact hi
  25. 0025intro a
  26. 0026intro ha
  27. 0027exfalso
  28. 0028specialize factor_permutation_below_zero_impossible (a)
  29. 0029apply factor_permutation_below_zero_impossible
  30. 0030exact ha
  31. 0031intro i
  32. 0032intro j
  33. 0033intro a
  34. 0034intro hi
  35. 0035intro hmap
  36. 0036intro hsource
  37. 0037exfalso
  38. 0038specialize factor_permutation_below_zero_impossible (i)
  39. 0039apply factor_permutation_below_zero_impossible
  40. 0040exact hi