SK002E

perfect_power_profile_code_exists

Nine actual historical Pair constructors package the ten finite data fields without expanding a huge nested arithmetic numeral.

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

∀ pb. ∀ pc. ∀ eb. ∀ ec. ∀ vb. ∀ vc. ∀ l. ∀ g. ∀ rb. ∀ rc. ∃ w. PerfectPowerProfileCode(w,pb,pc,eb,ec,vb,vc,l,g,rb,rc)

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

Definition DAG

NaturalPair(z,a,b) · 9PerfectPowerProfileCode(w,pb,pc,eb,ec,vb,vc,l,g,rb,rc) · 1

Actual proof prerequisites

pair_code_constructor · checked external prerequisite
Original expanded first-order statement 
forall pb pc eb ec vb vc l g rb rc. exists w. (exists ppf_code_0_code_constructed ppf_code_1_code_constructed ppf_code_2_code_constructed ppf_code_3_code_constructed ppf_code_4_code_constructed ppf_code_5_code_constructed ppf_code_6_code_constructed ppf_code_7_code_constructed. ((((w) = ((pb) + (ppf_code_0_code_constructed)) * S ((pb) + (ppf_code_0_code_constructed)) + ((ppf_code_0_code_constructed) + (ppf_code_0_code_constructed))) /\ ((((ppf_code_0_code_constructed) = ((pc) + (ppf_code_1_code_constructed)) * S ((pc) + (ppf_code_1_code_constructed)) + ((ppf_code_1_code_constructed) + (ppf_code_1_code_constructed))) /\ ((((ppf_code_1_code_constructed) = ((eb) + (ppf_code_2_code_constructed)) * S ((eb) + (ppf_code_2_code_constructed)) + ((ppf_code_2_code_constructed) + (ppf_code_2_code_constructed))) /\ ((((ppf_code_2_code_constructed) = ((ec) + (ppf_code_3_code_constructed)) * S ((ec) + (ppf_code_3_code_constructed)) + ((ppf_code_3_code_constructed) + (ppf_code_3_code_constructed))) /\ ((((ppf_code_3_code_constructed) = ((vb) + (ppf_code_4_code_constructed)) * S ((vb) + (ppf_code_4_code_constructed)) + ((ppf_code_4_code_constructed) + (ppf_code_4_code_constructed))) /\ ((((ppf_code_4_code_constructed) = ((vc) + (ppf_code_5_code_constructed)) * S ((vc) + (ppf_code_5_code_constructed)) + ((ppf_code_5_code_constructed) + (ppf_code_5_code_constructed))) /\ ((((ppf_code_5_code_constructed) = ((l) + (ppf_code_6_code_constructed)) * S ((l) + (ppf_code_6_code_constructed)) + ((ppf_code_6_code_constructed) + (ppf_code_6_code_constructed))) /\ ((((ppf_code_6_code_constructed) = ((g) + (ppf_code_7_code_constructed)) * S ((g) + (ppf_code_7_code_constructed)) + ((ppf_code_7_code_constructed) + (ppf_code_7_code_constructed))) /\ ((ppf_code_7_code_constructed) = ((rb) + (rc)) * S ((rb) + (rc)) + ((rc) + (rc))))))))))))))))))))

Complete tactic proof in conservative notation

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

81 script commands · 36 reading checkpoints · 9 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–10

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

  1. L1
    intro pb
  2. L2
    intro pc
  3. L3
    intro eb
  4. L4
    intro ec
  5. L5
    intro vb
  6. L6
    intro vc
  7. L7
    intro l
  8. L8
    intro g
  9. L9
    intro rb
  10. L10
    intro rc
02Establish hpair8L11–14

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

  1. L11
    have hpair8 : ∃ z. NaturalPair(z,rb,rc)Definitions: NaturalPair(z,rb,rc)Original native command in the exact edition
  2. L12
    specialize pair_code_constructor (rb)
  3. L13
    specialize pair_code_constructor (rc)
  4. L14
    apply pair_code_constructor
03Separate the logical casesL15–15

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

  1. L15
    cases hpair8
04Establish hpair7L16–19

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

  1. L16
    have hpair7 : ∃ z. NaturalPair(z,g,x)Definitions: NaturalPair(z,g,x)Original native command in the exact edition
  2. L17
    specialize pair_code_constructor (g)
  3. L18
    specialize pair_code_constructor (x)
  4. L19
    apply pair_code_constructor
05Separate the logical casesL20–20

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

  1. L20
    cases hpair7
06Establish hpair6L21–24

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

  1. L21
    have hpair6 : ∃ z. NaturalPair(z,l,x1)Definitions: NaturalPair(z,l,x1)Original native command in the exact edition
  2. L22
    specialize pair_code_constructor (l)
  3. L23
    specialize pair_code_constructor (x1)
  4. L24
    apply pair_code_constructor
07Separate the logical casesL25–25

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

  1. L25
    cases hpair6
08Establish hpair5L26–29

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

  1. L26
    have hpair5 : ∃ z. NaturalPair(z,vc,x2)Definitions: NaturalPair(z,vc,x2)Original native command in the exact edition
  2. L27
    specialize pair_code_constructor (vc)
  3. L28
    specialize pair_code_constructor (x2)
  4. L29
    apply pair_code_constructor
09Separate the logical casesL30–30

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

  1. L30
    cases hpair5
10Establish hpair4L31–34

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

  1. L31
    have hpair4 : ∃ z. NaturalPair(z,vb,x3)Definitions: NaturalPair(z,vb,x3)Original native command in the exact edition
  2. L32
    specialize pair_code_constructor (vb)
  3. L33
    specialize pair_code_constructor (x3)
  4. L34
    apply pair_code_constructor
11Separate the logical casesL35–35

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

  1. L35
    cases hpair4
12Establish hpair3L36–39

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

  1. L36
    have hpair3 : ∃ z. NaturalPair(z,ec,x4)Definitions: NaturalPair(z,ec,x4)Original native command in the exact edition
  2. L37
    specialize pair_code_constructor (ec)
  3. L38
    specialize pair_code_constructor (x4)
  4. L39
    apply pair_code_constructor
13Separate the logical casesL40–40

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

  1. L40
    cases hpair3
14Establish hpair2L41–44

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

  1. L41
    have hpair2 : ∃ z. NaturalPair(z,eb,x5)Definitions: NaturalPair(z,eb,x5)Original native command in the exact edition
  2. L42
    specialize pair_code_constructor (eb)
  3. L43
    specialize pair_code_constructor (x5)
  4. L44
    apply pair_code_constructor
15Separate the logical casesL45–45

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

  1. L45
    cases hpair2
16Establish hpair1L46–49

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

  1. L46
    have hpair1 : ∃ z. NaturalPair(z,pc,x6)Definitions: NaturalPair(z,pc,x6)Original native command in the exact edition
  2. L47
    specialize pair_code_constructor (pc)
  3. L48
    specialize pair_code_constructor (x6)
  4. L49
    apply pair_code_constructor
17Separate the logical casesL50–50

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

  1. L50
    cases hpair1
18Establish hpair0L51–54

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

  1. L51
    have hpair0 : ∃ z. NaturalPair(z,pb,x7)Definitions: NaturalPair(z,pb,x7)Original native command in the exact edition
  2. L52
    specialize pair_code_constructor (pb)
  3. L53
    specialize pair_code_constructor (x7)
  4. L54
    apply pair_code_constructor
19Separate the logical casesL55–55

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

  1. L55
    cases hpair0
20Construct an explicit witnessL56–64

Supply the displayed value, then prove that it has the required property.

  1. L56
    exists x8
  2. L57
    exists x7
  3. L58
    exists x6
  4. L59
    exists x5
  5. L60
    exists x4
  6. L61
    exists x3
  7. L62
    exists x2
  8. L63
    exists x1
  9. L64
    exists x
21Separate the logical casesL65–65

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

  1. L65
    split
22Use earlier factsL66–66

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

  1. L66
    exact hpair0_witness
23Separate the logical casesL67–67

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

  1. L67
    split
24Use earlier factsL68–68

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

  1. L68
    exact hpair1_witness
25Separate the logical casesL69–69

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

  1. L69
    split
26Use earlier factsL70–70

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

  1. L70
    exact hpair2_witness
27Separate the logical casesL71–71

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

  1. L71
    split
28Use earlier factsL72–72

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

  1. L72
    exact hpair3_witness
29Separate the logical casesL73–73

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

  1. L73
    split
30Use earlier factsL74–74

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

  1. L74
    exact hpair4_witness
31Separate the logical casesL75–75

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

  1. L75
    split
32Use earlier factsL76–76

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

  1. L76
    exact hpair5_witness
33Separate the logical casesL77–77

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

  1. L77
    split
34Use earlier factsL78–78

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

  1. L78
    exact hpair6_witness
35Separate the logical casesL79–79

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

  1. L79
    split
36Use earlier factsL80–81

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

  1. L80
    exact hpair7_witness
  2. L81
    exact hpair8_witness

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro eb
  4. 0004intro ec
  5. 0005intro vb
  6. 0006intro vc
  7. 0007intro l
  8. 0008intro g
  9. 0009intro rb
  10. 0010intro rc
  11. 0011have hpair8 : ∃ z. NaturalPair(z,rb,rc)
  12. 0012specialize pair_code_constructor (rb)
  13. 0013specialize pair_code_constructor (rc)
  14. 0014apply pair_code_constructor
  15. 0015cases hpair8
  16. 0016have hpair7 : ∃ z. NaturalPair(z,g,x)
  17. 0017specialize pair_code_constructor (g)
  18. 0018specialize pair_code_constructor (x)
  19. 0019apply pair_code_constructor
  20. 0020cases hpair7
  21. 0021have hpair6 : ∃ z. NaturalPair(z,l,x1)
  22. 0022specialize pair_code_constructor (l)
  23. 0023specialize pair_code_constructor (x1)
  24. 0024apply pair_code_constructor
  25. 0025cases hpair6
  26. 0026have hpair5 : ∃ z. NaturalPair(z,vc,x2)
  27. 0027specialize pair_code_constructor (vc)
  28. 0028specialize pair_code_constructor (x2)
  29. 0029apply pair_code_constructor
  30. 0030cases hpair5
  31. 0031have hpair4 : ∃ z. NaturalPair(z,vb,x3)
  32. 0032specialize pair_code_constructor (vb)
  33. 0033specialize pair_code_constructor (x3)
  34. 0034apply pair_code_constructor
  35. 0035cases hpair4
  36. 0036have hpair3 : ∃ z. NaturalPair(z,ec,x4)
  37. 0037specialize pair_code_constructor (ec)
  38. 0038specialize pair_code_constructor (x4)
  39. 0039apply pair_code_constructor
  40. 0040cases hpair3
  41. 0041have hpair2 : ∃ z. NaturalPair(z,eb,x5)
  42. 0042specialize pair_code_constructor (eb)
  43. 0043specialize pair_code_constructor (x5)
  44. 0044apply pair_code_constructor
  45. 0045cases hpair2
  46. 0046have hpair1 : ∃ z. NaturalPair(z,pc,x6)
  47. 0047specialize pair_code_constructor (pc)
  48. 0048specialize pair_code_constructor (x6)
  49. 0049apply pair_code_constructor
  50. 0050cases hpair1
  51. 0051have hpair0 : ∃ z. NaturalPair(z,pb,x7)
  52. 0052specialize pair_code_constructor (pb)
  53. 0053specialize pair_code_constructor (x7)
  54. 0054apply pair_code_constructor
  55. 0055cases hpair0
  56. 0056exists x8
  57. 0057exists x7
  58. 0058exists x6
  59. 0059exists x5
  60. 0060exists x4
  61. 0061exists x3
  62. 0062exists x2
  63. 0063exists x1
  64. 0064exists x
  65. 0065split
  66. 0066exact hpair0_witness
  67. 0067split
  68. 0068exact hpair1_witness
  69. 0069split
  70. 0070exact hpair2_witness
  71. 0071split
  72. 0072exact hpair3_witness
  73. 0073split
  74. 0074exact hpair4_witness
  75. 0075split
  76. 0076exact hpair5_witness
  77. 0077split
  78. 0078exact hpair6_witness
  79. 0079split
  80. 0080exact hpair7_witness
  81. 0081exact hpair8_witness