PA007D

beta_magnitude_predecessor_recode_exists

Alpha v34 checked-use theorem · independently closed; not Stable

Every positive bounded beta prefix can be recoded pointwise by removing one successor from each value.

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 PA statement

forall mb mc H l. (forall gmp_index_predecessor_recode_range. (exists gsp_lt_gap_predecessor_recode_range_index_bound. gsp_lt_gap_predecessor_recode_range_index_bound + S gmp_index_predecessor_recode_range = l) -> exists gmp_magnitude_predecessor_recode_range. ((((exists ff_h_gmp_predecessor_recode_range_decoded. ff_h_gmp_predecessor_recode_range_decoded + S (gmp_magnitude_predecessor_recode_range) = S ((S (gmp_index_predecessor_recode_range)) * mc)) /\ exists ff_q_gmp_predecessor_recode_range_decoded. mb = ff_q_gmp_predecessor_recode_range_decoded * S ((S (gmp_index_predecessor_recode_range)) * mc) + (gmp_magnitude_predecessor_recode_range))) /\ ((exists gsp_lt_gap_predecessor_recode_range_positive. gsp_lt_gap_predecessor_recode_range_positive + S 0 = gmp_magnitude_predecessor_recode_range) /\ (exists gsp_le_gap_predecessor_recode_range_bounded. gsp_le_gap_predecessor_recode_range_bounded + gmp_magnitude_predecessor_recode_range = H)))) -> (exists rb rc. (forall gmp_index_predecessor_recode_result gmp_predecessor_predecessor_recode_result. (exists gsp_lt_gap_predecessor_recode_result_index_bound. gsp_lt_gap_predecessor_recode_result_index_bound + S gmp_index_predecessor_recode_result = l) -> (((exists gsp_beta_height_gmp_predecessor_recode_result_source. gsp_beta_height_gmp_predecessor_recode_result_source + S (S gmp_predecessor_predecessor_recode_result) = S ((S (gmp_index_predecessor_recode_result)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_recode_result_source. mb = gsp_beta_quotient_gmp_predecessor_recode_result_source * S ((S (gmp_index_predecessor_recode_result)) * mc) + (S gmp_predecessor_predecessor_recode_result))) -> (((exists ff_h_gmp_predecessor_recode_result_target. ff_h_gmp_predecessor_recode_result_target + S (gmp_predecessor_predecessor_recode_result) = S ((S (gmp_index_predecessor_recode_result)) * rc)) /\ exists ff_q_gmp_predecessor_recode_result_target. rb = ff_q_gmp_predecessor_recode_result_target * S ((S (gmp_index_predecessor_recode_result)) * rc) + (gmp_predecessor_predecessor_recode_result)))))

Structural proof guide

Generated structural guide

Every positive bounded beta prefix can be recoded pointwise by removing one successor from each value.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, le_succ, le_refl, ne_zero_of_one_le, nonzero_is_succ, finite_lt_succ_eq_or_lt, beta_at_unique, succ_injective, beta_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (11), intermediate claims (9), equality transport (6).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA003D finite_lt_succ_eq_or_lt PA002F beta_at_unique PA003V succ_injective PA002X beta_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA003D finite_lt_succ_eq_or_lt PA002F beta_at_unique PA003V succ_injective PA002X beta_prefix_extend

Direct dependents

PA007E gauss_signed_half_predecessor_recode_exists PA00B4 finite_bounded_nonendpoint_injective_coverage PA00BE prime_wilson_terminal_product_package_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

106 script commands · 25 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.

Named ingredients (10)
add eq zero rightsucc ne zerole succle reflne zero of one lenonzero is succfinite lt succ eq or ltbeta at uniquesucc injectivebeta prefix extend

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

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

  1. L1
    intro mb
  2. L2
    intro mc
  3. L3
    intro H
02Induction on lL4–5

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

  1. L4
    induction l
  2. L5
    intro hrange
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–11

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

  1. L8
    intro i
  2. L9
    intro r
  3. L10
    intro hi
  4. L11
    intro hsource
05Separate the logical casesL12–13

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

  1. L12
    exfalso
  2. L13
    cases hi
06Establish hsiL14–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L14
    have hsi : S i = 0
  2. L15
    specialize add_eq_zero_right x
  3. L16
    specialize add_eq_zero_right (S i)
  4. L17
    apply add_eq_zero_right
  5. L18
    exact hi_witness
  6. L19
    specialize succ_ne_zero i
  7. L20
    apply succ_ne_zero
  8. L21
    exact hsi
  9. L22
    intro hrange
07Establish hprevious_rangeL23–31

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

  1. L23
    have hprevious_range : ∀ gmp_index_predecessor_recode_previous_range. Lt(gmp_index_predecessor_recode_previous_range,l) → ∃ x. BetaAt(mb,mc,gmp_index_predecessor_recode_previous_range,x) ∧ (Lt(0,x) ∧ Le(x,H))Definitions: LeLtBetaAt
  2. L24
    intro i
  3. L25
    intro hi
  4. L26
    specialize hrange i
  5. L27
    apply hrange
  6. L28
    specialize le_succ (S i)
  7. L29
    specialize le_succ l
  8. L30
    apply le_succ
  9. L31
    exact hi
08Establish hpreviousL32–34

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

  1. L32
    have hprevious : ∃ rb. ∃ rc. ∀ x. ∀ y. Lt(x,l) → BetaAt(mb,mc,x,S y) → BetaAt(rb,rc,x,y)Definitions: LtBetaAt
  2. L33
    apply IH
  3. L34
    exact hprevious_range
09Separate the logical casesL35–36

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

  1. L35
    cases hprevious
  2. L36
    cases hprevious_witness
10Establish hlastL37–41

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

  1. L37
    have hlast : exists m. (((exists ff_h_gmp_predecessor_recode_last_entry. ff_h_gmp_predecessor_recode_last_entry + S (m) = S ((S (l)) * mc)) /\ exists ff_q_gmp_predecessor_recode_last_entry. mb = ff_q_gmp_predecessor_recode_last_entry * S ((S (l)) * mc) + (m))) /\ ((exists gsp_lt_gap_predecessor_recode_last_positive. gsp_lt_gap_predecessor_recode_last_positive + S 0 = m) /\ (exists gsp_le_gap_predecessor_recode_last_bounded. gsp_le_gap_predecessor_recode_last_bounded + m = H))
  2. L38
    specialize hrange l
  3. L39
    apply hrange
  4. L40
    specialize le_refl (S l)
  5. L41
    exact le_refl
11Separate the logical casesL42–44

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

  1. L42
    cases hlast
  2. L43
    cases hlast_witness
  3. L44
    cases hlast_witness_right
12Establish hlast0L45–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ne zero of one le.

  1. L45
    have hlast0 : ~(x2 = 0)
  2. L46
    intro hlastzero
  3. L47
    specialize ne_zero_of_one_le x2
  4. L48
    apply ne_zero_of_one_le
  5. L49
    exact hlast_witness_right_left
  6. L50
    exact hlastzero
13Establish hlast_predecessorL51–54

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

  1. L51
    have hlast_predecessor : exists r. x2 = S r
  2. L52
    specialize nonzero_is_succ x2
  3. L53
    apply nonzero_is_succ
  4. L54
    exact hlast0
14Separate the logical casesL55–55

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

  1. L55
    cases hlast_predecessor
15Use earlier factsL56–59

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

  1. L56
    specialize beta_prefix_extend l
  2. L57
    specialize beta_prefix_extend x
  3. L58
    specialize beta_prefix_extend x1
  4. L59
    specialize beta_prefix_extend x3
16Separate the logical casesL60–62

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

  1. L60
    cases beta_prefix_extend
  2. L61
    cases beta_prefix_extend_witness
  3. L62
    cases beta_prefix_extend_witness_witness
17Construct an explicit witnessL63–64

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

  1. L63
    exists x4
  2. L64
    exists x5
18Fix variables and assumptionsL65–68

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

  1. L65
    intro i
  2. L66
    intro r
  3. L67
    intro hi
  4. L68
    intro hsource
19Establish hsplitL69–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L69
    have hsplit : i = l \/ exists gap. gap + S i = l
  2. L70
    specialize finite_lt_succ_eq_or_lt l
  3. L71
    specialize finite_lt_succ_eq_or_lt i
  4. L72
    apply finite_lt_succ_eq_or_lt
  5. L73
    exact hi
20Separate the logical casesL74–74

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

  1. L74
    cases hsplit
21Establish hsource_valueL75–84

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

  1. L75
    have hsource_value : S r = x2
  2. L76
    specialize beta_at_unique mb
  3. L77
    specialize beta_at_unique mc
  4. L78
    specialize beta_at_unique l
  5. L79
    specialize beta_at_unique (S r)
  6. L80
    specialize beta_at_unique x2
  7. L81
    apply beta_at_unique
  8. L82
    rewrite hsplit_left at hsource
  9. L83
    rewrite hsplit_left at hsource
  10. L84
    exact hsource
22Use earlier factsL85–85

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

  1. L85
    exact hlast_witness_left
23Establish hrvalueL86–95

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

  1. L86
    have hrvalue : r = x3
  2. L87
    specialize succ_injective r
  3. L88
    specialize succ_injective x3
  4. L89
    apply succ_injective
  5. L90
    trans x2
  6. L91
    exact hsource_value
  7. L92
    exact hlast_predecessor_witness
  8. L93
    rewrite hsplit_left
  9. L94
    rewrite hsplit_left
  10. L95
    rewrite hrvalue
24Calculate and transport equalitiesL96–96

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L96
    rewrite hrvalue
25Use earlier factsL97–106

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

  1. L97
    exact beta_prefix_extend_witness_witness_left
  2. L98
    specialize beta_prefix_extend_witness_witness_right i
  3. L99
    specialize beta_prefix_extend_witness_witness_right r
  4. L100
    apply beta_prefix_extend_witness_witness_right
  5. L101
    exact hsplit_right
  6. L102
    specialize hprevious_witness_witness i
  7. L103
    specialize hprevious_witness_witness r
  8. L104
    apply hprevious_witness_witness
  9. L105
    exact hsplit_right
  10. L106
    exact hsource

Library-wide reading audit

Original exact command ledger · 106 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro H
  4. 0004induction l
  5. 0005intro hrange
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro r
  10. 0010intro hi
  11. 0011intro hsource
  12. 0012exfalso
  13. 0013cases hi
  14. 0014have hsi : S i = 0
  15. 0015specialize add_eq_zero_right x
  16. 0016specialize add_eq_zero_right (S i)
  17. 0017apply add_eq_zero_right
  18. 0018exact hi_witness
  19. 0019specialize succ_ne_zero i
  20. 0020apply succ_ne_zero
  21. 0021exact hsi
  22. 0022intro hrange
  23. 0023have hprevious_range : forall gmp_index_predecessor_recode_previous_range. (exists gsp_lt_gap_predecessor_recode_previous_range_index_bound. gsp_lt_gap_predecessor_recode_previous_range_index_bound + S gmp_index_predecessor_recode_previous_range = l) -> exists gmp_magnitude_predecessor_recode_previous_range. ((((exists ff_h_gmp_predecessor_recode_previous_range_decoded. ff_h_gmp_predecessor_recode_previous_range_decoded + S (gmp_magnitude_predecessor_recode_previous_range) = S ((S (gmp_index_predecessor_recode_previous_range)) * mc)) /\ exists ff_q_gmp_predecessor_recode_previous_range_decoded. mb = ff_q_gmp_predecessor_recode_previous_range_decoded * S ((S (gmp_index_predecessor_recode_previous_range)) * mc) + (gmp_magnitude_predecessor_recode_previous_range))) /\ ((exists gsp_lt_gap_predecessor_recode_previous_range_positive. gsp_lt_gap_predecessor_recode_previous_range_positive + S 0 = gmp_magnitude_predecessor_recode_previous_range) /\ (exists gsp_le_gap_predecessor_recode_previous_range_bounded. gsp_le_gap_predecessor_recode_previous_range_bounded + gmp_magnitude_predecessor_recode_previous_range = H)))
  24. 0024intro i
  25. 0025intro hi
  26. 0026specialize hrange i
  27. 0027apply hrange
  28. 0028specialize le_succ (S i)
  29. 0029specialize le_succ l
  30. 0030apply le_succ
  31. 0031exact hi
  32. 0032have hprevious : exists rb rc. (forall gmp_index_predecessor_recode_previous_result gmp_predecessor_predecessor_recode_previous_result. (exists gsp_lt_gap_predecessor_recode_previous_result_index_bound. gsp_lt_gap_predecessor_recode_previous_result_index_bound + S gmp_index_predecessor_recode_previous_result = l) -> (((exists gsp_beta_height_gmp_predecessor_recode_previous_result_source. gsp_beta_height_gmp_predecessor_recode_previous_result_source + S (S gmp_predecessor_predecessor_recode_previous_result) = S ((S (gmp_index_predecessor_recode_previous_result)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_recode_previous_result_source. mb = gsp_beta_quotient_gmp_predecessor_recode_previous_result_source * S ((S (gmp_index_predecessor_recode_previous_result)) * mc) + (S gmp_predecessor_predecessor_recode_previous_result))) -> (((exists ff_h_gmp_predecessor_recode_previous_result_target. ff_h_gmp_predecessor_recode_previous_result_target + S (gmp_predecessor_predecessor_recode_previous_result) = S ((S (gmp_index_predecessor_recode_previous_result)) * rc)) /\ exists ff_q_gmp_predecessor_recode_previous_result_target. rb = ff_q_gmp_predecessor_recode_previous_result_target * S ((S (gmp_index_predecessor_recode_previous_result)) * rc) + (gmp_predecessor_predecessor_recode_previous_result))))
  33. 0033apply IH
  34. 0034exact hprevious_range
  35. 0035cases hprevious
  36. 0036cases hprevious_witness
  37. 0037have hlast : exists m. (((exists ff_h_gmp_predecessor_recode_last_entry. ff_h_gmp_predecessor_recode_last_entry + S (m) = S ((S (l)) * mc)) /\ exists ff_q_gmp_predecessor_recode_last_entry. mb = ff_q_gmp_predecessor_recode_last_entry * S ((S (l)) * mc) + (m))) /\ ((exists gsp_lt_gap_predecessor_recode_last_positive. gsp_lt_gap_predecessor_recode_last_positive + S 0 = m) /\ (exists gsp_le_gap_predecessor_recode_last_bounded. gsp_le_gap_predecessor_recode_last_bounded + m = H))
  38. 0038specialize hrange l
  39. 0039apply hrange
  40. 0040specialize le_refl (S l)
  41. 0041exact le_refl
  42. 0042cases hlast
  43. 0043cases hlast_witness
  44. 0044cases hlast_witness_right
  45. 0045have hlast0 : ~(x2 = 0)
  46. 0046intro hlastzero
  47. 0047specialize ne_zero_of_one_le x2
  48. 0048apply ne_zero_of_one_le
  49. 0049exact hlast_witness_right_left
  50. 0050exact hlastzero
  51. 0051have hlast_predecessor : exists r. x2 = S r
  52. 0052specialize nonzero_is_succ x2
  53. 0053apply nonzero_is_succ
  54. 0054exact hlast0
  55. 0055cases hlast_predecessor
  56. 0056specialize beta_prefix_extend l
  57. 0057specialize beta_prefix_extend x
  58. 0058specialize beta_prefix_extend x1
  59. 0059specialize beta_prefix_extend x3
  60. 0060cases beta_prefix_extend
  61. 0061cases beta_prefix_extend_witness
  62. 0062cases beta_prefix_extend_witness_witness
  63. 0063exists x4
  64. 0064exists x5
  65. 0065intro i
  66. 0066intro r
  67. 0067intro hi
  68. 0068intro hsource
  69. 0069have hsplit : i = l \/ exists gap. gap + S i = l
  70. 0070specialize finite_lt_succ_eq_or_lt l
  71. 0071specialize finite_lt_succ_eq_or_lt i
  72. 0072apply finite_lt_succ_eq_or_lt
  73. 0073exact hi
  74. 0074cases hsplit
  75. 0075have hsource_value : S r = x2
  76. 0076specialize beta_at_unique mb
  77. 0077specialize beta_at_unique mc
  78. 0078specialize beta_at_unique l
  79. 0079specialize beta_at_unique (S r)
  80. 0080specialize beta_at_unique x2
  81. 0081apply beta_at_unique
  82. 0082rewrite hsplit_left at hsource
  83. 0083rewrite hsplit_left at hsource
  84. 0084exact hsource
  85. 0085exact hlast_witness_left
  86. 0086have hrvalue : r = x3
  87. 0087specialize succ_injective r
  88. 0088specialize succ_injective x3
  89. 0089apply succ_injective
  90. 0090trans x2
  91. 0091exact hsource_value
  92. 0092exact hlast_predecessor_witness
  93. 0093rewrite hsplit_left
  94. 0094rewrite hsplit_left
  95. 0095rewrite hrvalue
  96. 0096rewrite hrvalue
  97. 0097exact beta_prefix_extend_witness_witness_left
  98. 0098specialize beta_prefix_extend_witness_witness_right i
  99. 0099specialize beta_prefix_extend_witness_witness_right r
  100. 0100apply beta_prefix_extend_witness_witness_right
  101. 0101exact hsplit_right
  102. 0102specialize hprevious_witness_witness i
  103. 0103specialize hprevious_witness_witness r
  104. 0104apply hprevious_witness_witness
  105. 0105exact hsplit_right
  106. 0106exact hsource