PA007F · theorem

beta_sign_factor_prefix_extend

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

Append the selected 1/r factor while preserving every earlier decoded factor.

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.

Statement with defined notation

∀ sb. ∀ sc. ∀ fb. ∀ fc. ∀ r. ∀ l. ∀ a. ∀ f. (∀ x. ∀ y. Lt(x,l) → BetaAt(sb,sc,x,y) → y = 0 ∧ BetaAt(fb,fc,x,1) ∨ y = 1 ∧ BetaAt(fb,fc,x,r)) → BetaAt(sb,sc,l,a) → a = 0 ∧ f = 1 ∨ a = 1 ∧ f = r → ∃ x. ∃ y. ∀ z. ∀ n. Lt(z,S l) → BetaAt(sb,sc,z,n) → n = 0 ∧ BetaAt(x,y,z,1) ∨ n = 1 ∧ BetaAt(x,y,z,r)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

9 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

6 occurrences

Exact expanded native-PA statement
forall sb sc fb fc r l a f. (forall gspf_index_recode_before gspf_bit_recode_before. (exists gsp_lt_gap_recode_before_bound. gsp_lt_gap_recode_before_bound + S gspf_index_recode_before = l) -> (((exists ff_h_gspf_recode_before_bit. ff_h_gspf_recode_before_bit + S (gspf_bit_recode_before) = S ((S (gspf_index_recode_before)) * sc)) /\ exists ff_q_gspf_recode_before_bit. sb = ff_q_gspf_recode_before_bit * S ((S (gspf_index_recode_before)) * sc) + (gspf_bit_recode_before))) -> (((gspf_bit_recode_before = 0) /\ (((exists gsp_beta_height_gspf_recode_before_one. gsp_beta_height_gspf_recode_before_one + S (1) = S ((S (gspf_index_recode_before)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_before_one. fb = gsp_beta_quotient_gspf_recode_before_one * S ((S (gspf_index_recode_before)) * fc) + (1)))) \/ ((gspf_bit_recode_before = 1) /\ (((exists ff_h_gspf_recode_before_predecessor. ff_h_gspf_recode_before_predecessor + S (r) = S ((S (gspf_index_recode_before)) * fc)) /\ exists ff_q_gspf_recode_before_predecessor. fb = ff_q_gspf_recode_before_predecessor * S ((S (gspf_index_recode_before)) * fc) + (r)))))) -> (((exists ff_h_recode_source_last. ff_h_recode_source_last + S (a) = S ((S (l)) * sc)) /\ exists ff_q_recode_source_last. sb = ff_q_recode_source_last * S ((S (l)) * sc) + (a))) -> ((a = 0 /\ f = 1) \/ (a = 1 /\ f = r)) -> exists z d. (forall gspf_index_recode_after gspf_bit_recode_after. (exists gsp_lt_gap_recode_after_bound. gsp_lt_gap_recode_after_bound + S gspf_index_recode_after = S l) -> (((exists ff_h_gspf_recode_after_bit. ff_h_gspf_recode_after_bit + S (gspf_bit_recode_after) = S ((S (gspf_index_recode_after)) * sc)) /\ exists ff_q_gspf_recode_after_bit. sb = ff_q_gspf_recode_after_bit * S ((S (gspf_index_recode_after)) * sc) + (gspf_bit_recode_after))) -> (((gspf_bit_recode_after = 0) /\ (((exists gsp_beta_height_gspf_recode_after_one. gsp_beta_height_gspf_recode_after_one + S (1) = S ((S (gspf_index_recode_after)) * d)) /\ exists gsp_beta_quotient_gspf_recode_after_one. z = gsp_beta_quotient_gspf_recode_after_one * S ((S (gspf_index_recode_after)) * d) + (1)))) \/ ((gspf_bit_recode_after = 1) /\ (((exists ff_h_gspf_recode_after_predecessor. ff_h_gspf_recode_after_predecessor + S (r) = S ((S (gspf_index_recode_after)) * d)) /\ exists ff_q_gspf_recode_after_predecessor. z = ff_q_gspf_recode_after_predecessor * S ((S (gspf_index_recode_after)) * d) + (r))))))

Proof neighborhood

Direct theorem prerequisites

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt PA002F beta_at_unique

Direct theorem dependents

PA007G beta_sign_factor_prefix_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

95 script commands · 23 reading checkpoints · 6 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 (3)
beta prefix extendfinite lt succ eq or ltbeta at unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro sb
  2. L2
    intro sc
  3. L3
    intro fb
  4. L4
    intro fc
  5. L5
    intro r
  6. L6
    intro l
  7. L7
    intro a
  8. L8
    intro f
  9. L9
    intro hsigns
  10. L10
    intro hlast
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hchosen
03Use earlier factsL12–15

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

  1. L12
    specialize beta_prefix_extend l
  2. L13
    specialize beta_prefix_extend fb
  3. L14
    specialize beta_prefix_extend fc
  4. L15
    specialize beta_prefix_extend f
04Separate the logical casesL16–18

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

  1. L16
    cases beta_prefix_extend
  2. L17
    cases beta_prefix_extend_witness
  3. L18
    cases beta_prefix_extend_witness_witness
05Construct an explicit witnessL19–20

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

  1. L19
    exists x
  2. L20
    exists x1
06Fix variables and assumptionsL21–24

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

  1. L21
    intro i
  2. L22
    intro v
  3. L23
    intro hi
  4. L24
    intro hv
07Establish hsplitL25–29

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. L25
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L26
    specialize finite_lt_succ_eq_or_lt l
  3. L27
    specialize finite_lt_succ_eq_or_lt i
  4. L28
    apply finite_lt_succ_eq_or_lt
  5. L29
    exact hi
08Separate the logical casesL30–30

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

  1. L30
    cases hsplit
09Establish hvlastL31–34

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hvlast : BetaAt(sb,sc,l,v)Definitions: BetaAt(sb,sc,l,v)Original native command in the exact edition
  2. L32
    rewrite hsplit_left at hv
  3. L33
    rewrite hsplit_left at hv
  4. L34
    exact hv
10Establish hvaL35–43

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

  1. L35
    have hva : v = a
  2. L36
    specialize beta_at_unique sb
  3. L37
    specialize beta_at_unique sc
  4. L38
    specialize beta_at_unique l
  5. L39
    specialize beta_at_unique v
  6. L40
    specialize beta_at_unique a
  7. L41
    apply beta_at_unique
  8. L42
    exact hvlast
  9. L43
    exact hlast
11Separate the logical casesL44–47

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

  1. L44
    cases hchosen
  2. L45
    cases hchosen_left
  3. L46
    left
  4. L47
    split
12Calculate and transport equalitiesL48–48

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

  1. L48
    trans a
13Use earlier factsL49–50

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

  1. L49
    exact hva
  2. L50
    exact hchosen_left_left
14Establish hnew_oneL51–57

Establish this local claim before using it. It is not an additional assumption.

  1. L51
    have hnew_one : BetaAt(x,x1,l,1)Definitions: BetaAt(x,x1,l,1)Original native command in the exact edition
  2. L52
    rewrite hchosen_left_right at beta_prefix_extend_witness_witness_left
  3. L53
    rewrite hchosen_left_right at beta_prefix_extend_witness_witness_left
  4. L54
    exact beta_prefix_extend_witness_witness_left
  5. L55
    rewrite hsplit_left
  6. L56
    rewrite hsplit_left
  7. L57
    exact hnew_one
15Separate the logical casesL58–60

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

  1. L58
    cases hchosen_right
  2. L59
    right
  3. L60
    split
16Calculate and transport equalitiesL61–61

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

  1. L61
    trans a
17Use earlier factsL62–63

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

  1. L62
    exact hva
  2. L63
    exact hchosen_right_left
18Establish hnew_predecessorL64–70

Establish this local claim before using it. It is not an additional assumption.

  1. L64
    have hnew_predecessor : BetaAt(x,x1,l,r)Definitions: BetaAt(x,x1,l,r)Original native command in the exact edition
  2. L65
    rewrite hchosen_right_right at beta_prefix_extend_witness_witness_left
  3. L66
    rewrite hchosen_right_right at beta_prefix_extend_witness_witness_left
  4. L67
    exact beta_prefix_extend_witness_witness_left
  5. L68
    rewrite hsplit_left
  6. L69
    rewrite hsplit_left
  7. L70
    exact hnew_predecessor
19Establish holdL71–76

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

  1. L71
    have hold : v = 0 ∧ BetaAt(fb,fc,i,1) ∨ v = 1 ∧ BetaAt(fb,fc,i,r)Definitions: BetaAt(fb,fc,i,1)BetaAt(fb,fc,i,r)Original native command in the exact edition
  2. L72
    specialize hsigns i
  3. L73
    specialize hsigns v
  4. L74
    apply hsigns
  5. L75
    exact hsplit_right
  6. L76
    exact hv
20Separate the logical casesL77–80

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

  1. L77
    cases hold
  2. L78
    cases hold_left
  3. L79
    left
  4. L80
    split
21Use earlier factsL81–86

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

  1. L81
    exact hold_left_left
  2. L82
    specialize beta_prefix_extend_witness_witness_right i
  3. L83
    specialize beta_prefix_extend_witness_witness_right 1
  4. L84
    apply beta_prefix_extend_witness_witness_right
  5. L85
    exact hsplit_right
  6. L86
    exact hold_left_right
22Separate the logical casesL87–89

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

  1. L87
    cases hold_right
  2. L88
    right
  3. L89
    split
23Use earlier factsL90–95

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

  1. L90
    exact hold_right_left
  2. L91
    specialize beta_prefix_extend_witness_witness_right i
  3. L92
    specialize beta_prefix_extend_witness_witness_right r
  4. L93
    apply beta_prefix_extend_witness_witness_right
  5. L94
    exact hsplit_right
  6. L95
    exact hold_right_right

Library-wide reading audit

Original defined command ledger · 95 lines
  1. 0001intro sb
  2. 0002intro sc
  3. 0003intro fb
  4. 0004intro fc
  5. 0005intro r
  6. 0006intro l
  7. 0007intro a
  8. 0008intro f
  9. 0009intro hsigns
  10. 0010intro hlast
  11. 0011intro hchosen
  12. 0012specialize beta_prefix_extend l
  13. 0013specialize beta_prefix_extend fb
  14. 0014specialize beta_prefix_extend fc
  15. 0015specialize beta_prefix_extend f
  16. 0016cases beta_prefix_extend
  17. 0017cases beta_prefix_extend_witness
  18. 0018cases beta_prefix_extend_witness_witness
  19. 0019exists x
  20. 0020exists x1
  21. 0021intro i
  22. 0022intro v
  23. 0023intro hi
  24. 0024intro hv
  25. 0025have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists gap. gap + S i = l
  26. 0026specialize finite_lt_succ_eq_or_lt l
  27. 0027specialize finite_lt_succ_eq_or_lt i
  28. 0028apply finite_lt_succ_eq_or_lt
  29. 0029exact hi
  30. 0030cases hsplit
  31. 0031have hvlast : BetaAt(sb,sc,l,v)
    Exact native replay linehave hvlast : ((exists ff_h_recode_top_source. ff_h_recode_top_source + S (v) = S ((S (l)) * sc)) /\ exists ff_q_recode_top_source. sb = ff_q_recode_top_source * S ((S (l)) * sc) + (v))
  32. 0032rewrite hsplit_left at hv
  33. 0033rewrite hsplit_left at hv
  34. 0034exact hv
  35. 0035have hva : v = a
  36. 0036specialize beta_at_unique sb
  37. 0037specialize beta_at_unique sc
  38. 0038specialize beta_at_unique l
  39. 0039specialize beta_at_unique v
  40. 0040specialize beta_at_unique a
  41. 0041apply beta_at_unique
  42. 0042exact hvlast
  43. 0043exact hlast
  44. 0044cases hchosen
  45. 0045cases hchosen_left
  46. 0046left
  47. 0047split
  48. 0048trans a
  49. 0049exact hva
  50. 0050exact hchosen_left_left
  51. 0051have hnew_one : BetaAt(x,x1,l,1)
    Exact native replay linehave hnew_one : ((exists gsp_beta_height_recode_new_one. gsp_beta_height_recode_new_one + S (1) = S ((S (l)) * x1)) /\ exists gsp_beta_quotient_recode_new_one. x = gsp_beta_quotient_recode_new_one * S ((S (l)) * x1) + (1))
  52. 0052rewrite hchosen_left_right at beta_prefix_extend_witness_witness_left
  53. 0053rewrite hchosen_left_right at beta_prefix_extend_witness_witness_left
  54. 0054exact beta_prefix_extend_witness_witness_left
  55. 0055rewrite hsplit_left
  56. 0056rewrite hsplit_left
  57. 0057exact hnew_one
  58. 0058cases hchosen_right
  59. 0059right
  60. 0060split
  61. 0061trans a
  62. 0062exact hva
  63. 0063exact hchosen_right_left
  64. 0064have hnew_predecessor : BetaAt(x,x1,l,r)
    Exact native replay linehave hnew_predecessor : ((exists ff_h_recode_new_predecessor. ff_h_recode_new_predecessor + S (r) = S ((S (l)) * x1)) /\ exists ff_q_recode_new_predecessor. x = ff_q_recode_new_predecessor * S ((S (l)) * x1) + (r))
  65. 0065rewrite hchosen_right_right at beta_prefix_extend_witness_witness_left
  66. 0066rewrite hchosen_right_right at beta_prefix_extend_witness_witness_left
  67. 0067exact beta_prefix_extend_witness_witness_left
  68. 0068rewrite hsplit_left
  69. 0069rewrite hsplit_left
  70. 0070exact hnew_predecessor
  71. 0071have hold : v = 0 ∧ BetaAt(fb,fc,i,1) ∨ v = 1 ∧ BetaAt(fb,fc,i,r)
    Exact native replay linehave hold : ((v = 0 /\ (((exists gsp_beta_height_recode_old_one. gsp_beta_height_recode_old_one + S (1) = S ((S (i)) * fc)) /\ exists gsp_beta_quotient_recode_old_one. fb = gsp_beta_quotient_recode_old_one * S ((S (i)) * fc) + (1)))) \/ (v = 1 /\ (((exists ff_h_recode_old_predecessor. ff_h_recode_old_predecessor + S (r) = S ((S (i)) * fc)) /\ exists ff_q_recode_old_predecessor. fb = ff_q_recode_old_predecessor * S ((S (i)) * fc) + (r)))))
  72. 0072specialize hsigns i
  73. 0073specialize hsigns v
  74. 0074apply hsigns
  75. 0075exact hsplit_right
  76. 0076exact hv
  77. 0077cases hold
  78. 0078cases hold_left
  79. 0079left
  80. 0080split
  81. 0081exact hold_left_left
  82. 0082specialize beta_prefix_extend_witness_witness_right i
  83. 0083specialize beta_prefix_extend_witness_witness_right 1
  84. 0084apply beta_prefix_extend_witness_witness_right
  85. 0085exact hsplit_right
  86. 0086exact hold_left_right
  87. 0087cases hold_right
  88. 0088right
  89. 0089split
  90. 0090exact hold_right_left
  91. 0091specialize beta_prefix_extend_witness_witness_right i
  92. 0092specialize beta_prefix_extend_witness_witness_right r
  93. 0093apply beta_prefix_extend_witness_witness_right
  94. 0094exact hsplit_right
  95. 0095exact hold_right_right