TS000V · theorem body

beta_affine_residue_grid_extend

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

Append the next canonical affine residue while preserving every decoded row, column, quotient, and earlier residue.

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

∀ p. ∀ w. ∀ r. ∀ b. ∀ c. ∀ l. (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. ∃ m. x = w · y + z ∧ (Lt(z,w) ∧ (r · y + z = p · n + m ∧ (Lt(m,p) ∧ BetaAt(b,c,x,m))))) → (∃ x. ∃ y. ∃ z. ∃ n. l = w · x + y ∧ (Lt(y,w) ∧ DivRem(r · x + y,p,z,n))) → ∃ x. ∃ y. ∀ z. Lt(z,S l) → ∃ n. ∃ m. ∃ k. ∃ i. z = w · n + m ∧ (Lt(m,w) ∧ (r · n + m = p · k + i ∧ (Lt(i,p) ∧ BetaAt(x,y,z,i))))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0007 DivRem PD0013 BetaAt

In local proof propositions

PD0002 Lt PD0013 BetaAt
Exact expanded first-order statement
forall p w r b c l. (forall ftrg_index_extend_previous. (exists ftrg_gap_extend_previous_index. ftrg_gap_extend_previous_index + S (ftrg_index_extend_previous) = (l)) -> exists ftrg_row_extend_previous ftrg_column_extend_previous ftrg_quotient_extend_previous ftrg_remainder_extend_previous. ((ftrg_index_extend_previous) = (w) * ftrg_row_extend_previous + ftrg_column_extend_previous /\ ((exists ftrg_gap_extend_previous_column. ftrg_gap_extend_previous_column + S (ftrg_column_extend_previous) = (w)) /\ ((r * ftrg_row_extend_previous + ftrg_column_extend_previous = (p) * ftrg_quotient_extend_previous + ftrg_remainder_extend_previous) /\ ((exists ftrg_gap_extend_previous_residue. ftrg_gap_extend_previous_residue + S (ftrg_remainder_extend_previous) = (p)) /\ (((exists ff_h_ftrg_extend_previous_entry. ff_h_ftrg_extend_previous_entry + S (ftrg_remainder_extend_previous) = S ((S (ftrg_index_extend_previous)) * c)) /\ exists ff_q_ftrg_extend_previous_entry. b = ff_q_ftrg_extend_previous_entry * S ((S (ftrg_index_extend_previous)) * c) + (ftrg_remainder_extend_previous)))))))) -> (exists ftrg_row_extend_last ftrg_column_extend_last ftrg_quotient_extend_last ftrg_remainder_extend_last. ((l) = (w) * ftrg_row_extend_last + ftrg_column_extend_last /\ ((exists ftrg_gap_extend_last_column. ftrg_gap_extend_last_column + S (ftrg_column_extend_last) = (w)) /\ ((r * ftrg_row_extend_last + ftrg_column_extend_last = (p) * ftrg_quotient_extend_last + ftrg_remainder_extend_last) /\ (exists ftrg_gap_extend_last_residue. ftrg_gap_extend_last_residue + S (ftrg_remainder_extend_last) = (p)))))) -> exists z d. (forall ftrg_index_extend_next. (exists ftrg_gap_extend_next_index. ftrg_gap_extend_next_index + S (ftrg_index_extend_next) = (S l)) -> exists ftrg_row_extend_next ftrg_column_extend_next ftrg_quotient_extend_next ftrg_remainder_extend_next. ((ftrg_index_extend_next) = (w) * ftrg_row_extend_next + ftrg_column_extend_next /\ ((exists ftrg_gap_extend_next_column. ftrg_gap_extend_next_column + S (ftrg_column_extend_next) = (w)) /\ ((r * ftrg_row_extend_next + ftrg_column_extend_next = (p) * ftrg_quotient_extend_next + ftrg_remainder_extend_next) /\ ((exists ftrg_gap_extend_next_residue. ftrg_gap_extend_next_residue + S (ftrg_remainder_extend_next) = (p)) /\ (((exists ff_h_ftrg_extend_next_entry. ff_h_ftrg_extend_next_entry + S (ftrg_remainder_extend_next) = S ((S (ftrg_index_extend_next)) * d)) /\ exists ff_q_ftrg_extend_next_entry. z = ff_q_ftrg_extend_next_entry * S ((S (ftrg_index_extend_next)) * d) + (ftrg_remainder_extend_next))))))))

Proof neighborhood

Direct theorem prerequisites

beta_prefix_extend · Stable closed finite_lt_succ_eq_or_lt · Stable closed

Direct theorem dependents

TS000W beta_affine_residue_grid_exists

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

79 script commands · 31 reading checkpoints · 3 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–8

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

  1. L1
    intro p
  2. L2
    intro w
  3. L3
    intro r
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro l
  7. L7
    intro hprevious
  8. L8
    intro hpoint
02Separate the logical casesL9–15

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

  1. L9
    cases hpoint
  2. L10
    cases hpoint_witness
  3. L11
    cases hpoint_witness_witness
  4. L12
    cases hpoint_witness_witness_witness
  5. L13
    cases hpoint_witness_witness_witness_witness
  6. L14
    cases hpoint_witness_witness_witness_witness_right
  7. L15
    cases hpoint_witness_witness_witness_witness_right_right
03Establish hextensionL16–21

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

  1. L16
    have hextension : ∃ z. ∃ d. BetaAt(z,d,l,x3) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))Definitions: BetaAt(z,d,l,x3)Lt(x,l)BetaAt(b,c,x,y)BetaAt(z,d,x,y)Original native command in the exact edition
  2. L17
    specialize beta_prefix_extend l
  3. L18
    specialize beta_prefix_extend b
  4. L19
    specialize beta_prefix_extend c
  5. L20
    specialize beta_prefix_extend x3
  6. L21
    exact beta_prefix_extend
04Separate the logical casesL22–24

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

  1. L22
    cases hextension
  2. L23
    cases hextension_witness
  3. L24
    cases hextension_witness_witness
05Construct an explicit witnessL25–26

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

  1. L25
    exists x4
  2. L26
    exists x5
06Fix variables and assumptionsL27–28

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

  1. L27
    intro k
  2. L28
    intro hk
07Establish hsplitL29–33

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. L29
    have hsplit : k = l ∨ Lt(k,l)Definitions: Lt(k,l)Original native command in the exact edition
  2. L30
    specialize finite_lt_succ_eq_or_lt l
  3. L31
    specialize finite_lt_succ_eq_or_lt k
  4. L32
    apply finite_lt_succ_eq_or_lt
  5. L33
    exact hk
08Separate the logical casesL34–34

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

  1. L34
    cases hsplit
09Construct an explicit witnessL35–38

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

  1. L35
    exists x
  2. L36
    exists x1
  3. L37
    exists x2
  4. L38
    exists x3
10Separate the logical casesL39–39

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

  1. L39
    split
11Calculate and transport equalitiesL40–40

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

  1. L40
    rewrite hsplit_left
12Use earlier factsL41–41

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

  1. L41
    exact hpoint_witness_witness_witness_witness_left
13Separate the logical casesL42–42

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

  1. L42
    split
14Use earlier factsL43–43

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

  1. L43
    exact hpoint_witness_witness_witness_witness_right_left
15Separate the logical casesL44–44

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

  1. L44
    split
16Use earlier factsL45–45

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

  1. L45
    exact hpoint_witness_witness_witness_witness_right_right_left
17Separate the logical casesL46–46

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

  1. L46
    split
18Use earlier factsL47–47

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

  1. L47
    exact hpoint_witness_witness_witness_witness_right_right_right
19Calculate and transport equalitiesL48–49

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

  1. L48
    rewrite hsplit_left
  2. L49
    rewrite hsplit_left
20Use earlier factsL50–51

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

  1. L50
    exact hextension_witness_witness_left
  2. L51
    specialize hprevious k
21Establish holdL52–54

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

  1. L52
    have hold : ∃ i. ∃ j. ∃ q. ∃ t. k = w · i + j ∧ (Lt(j,w) ∧ (r · i + j = p · q + t ∧ (Lt(t,p) ∧ BetaAt(b,c,k,t))))Definitions: Lt(j,w)Lt(t,p)BetaAt(b,c,k,t)Original native command in the exact edition
  2. L53
    apply hprevious
  3. L54
    exact hsplit_right
22Separate the logical casesL55–62

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

  1. L55
    cases hold
  2. L56
    cases hold_witness
  3. L57
    cases hold_witness_witness
  4. L58
    cases hold_witness_witness_witness
  5. L59
    cases hold_witness_witness_witness_witness
  6. L60
    cases hold_witness_witness_witness_witness_right
  7. L61
    cases hold_witness_witness_witness_witness_right_right
  8. L62
    cases hold_witness_witness_witness_witness_right_right_right
23Construct an explicit witnessL63–66

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

  1. L63
    exists x6
  2. L64
    exists x7
  3. L65
    exists x8
  4. L66
    exists x9
24Separate the logical casesL67–67

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

  1. L67
    split
25Use earlier factsL68–68

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

  1. L68
    exact hold_witness_witness_witness_witness_left
26Separate the logical casesL69–69

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

  1. L69
    split
27Use earlier factsL70–70

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

  1. L70
    exact hold_witness_witness_witness_witness_right_left
28Separate the logical casesL71–71

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

  1. L71
    split
29Use earlier factsL72–72

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

  1. L72
    exact hold_witness_witness_witness_witness_right_right_left
30Separate the logical casesL73–73

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

  1. L73
    split
31Use earlier factsL74–79

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

  1. L74
    exact hold_witness_witness_witness_witness_right_right_right_left
  2. L75
    specialize hextension_witness_witness_right k
  3. L76
    specialize hextension_witness_witness_right x9
  4. L77
    apply hextension_witness_witness_right
  5. L78
    exact hsplit_right
  6. L79
    exact hold_witness_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original defined command ledger · 79 lines
  1. 0001intro p
  2. 0002intro w
  3. 0003intro r
  4. 0004intro b
  5. 0005intro c
  6. 0006intro l
  7. 0007intro hprevious
  8. 0008intro hpoint
  9. 0009cases hpoint
  10. 0010cases hpoint_witness
  11. 0011cases hpoint_witness_witness
  12. 0012cases hpoint_witness_witness_witness
  13. 0013cases hpoint_witness_witness_witness_witness
  14. 0014cases hpoint_witness_witness_witness_witness_right
  15. 0015cases hpoint_witness_witness_witness_witness_right_right
  16. 0016have hextension : ∃ z. ∃ d. BetaAt(z,d,l,x3) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))
    Exact native replay linehave hextension : exists z d. ((((exists ff_h_ftrg_extension_last. ff_h_ftrg_extension_last + S (x3) = S ((S (l)) * d)) /\ exists ff_q_ftrg_extension_last. z = ff_q_ftrg_extension_last * S ((S (l)) * d) + (x3))) /\ forall k value. (exists ftrg_gap_extension_old_bound. ftrg_gap_extension_old_bound + S (k) = (l)) -> (((exists ff_h_ftrg_extension_old. ff_h_ftrg_extension_old + S (value) = S ((S (k)) * c)) /\ exists ff_q_ftrg_extension_old. b = ff_q_ftrg_extension_old * S ((S (k)) * c) + (value))) -> (((exists ff_h_ftrg_extension_new. ff_h_ftrg_extension_new + S (value) = S ((S (k)) * d)) /\ exists ff_q_ftrg_extension_new. z = ff_q_ftrg_extension_new * S ((S (k)) * d) + (value))))
  17. 0017specialize beta_prefix_extend l
  18. 0018specialize beta_prefix_extend b
  19. 0019specialize beta_prefix_extend c
  20. 0020specialize beta_prefix_extend x3
  21. 0021exact beta_prefix_extend
  22. 0022cases hextension
  23. 0023cases hextension_witness
  24. 0024cases hextension_witness_witness
  25. 0025exists x4
  26. 0026exists x5
  27. 0027intro k
  28. 0028intro hk
  29. 0029have hsplit : k = l ∨ Lt(k,l)
    Exact native replay linehave hsplit : k = l \/ exists gap. gap + S k = l
  30. 0030specialize finite_lt_succ_eq_or_lt l
  31. 0031specialize finite_lt_succ_eq_or_lt k
  32. 0032apply finite_lt_succ_eq_or_lt
  33. 0033exact hk
  34. 0034cases hsplit
  35. 0035exists x
  36. 0036exists x1
  37. 0037exists x2
  38. 0038exists x3
  39. 0039split
  40. 0040rewrite hsplit_left
  41. 0041exact hpoint_witness_witness_witness_witness_left
  42. 0042split
  43. 0043exact hpoint_witness_witness_witness_witness_right_left
  44. 0044split
  45. 0045exact hpoint_witness_witness_witness_witness_right_right_left
  46. 0046split
  47. 0047exact hpoint_witness_witness_witness_witness_right_right_right
  48. 0048rewrite hsplit_left
  49. 0049rewrite hsplit_left
  50. 0050exact hextension_witness_witness_left
  51. 0051specialize hprevious k
  52. 0052have hold : ∃ i. ∃ j. ∃ q. ∃ t. k = w · i + j ∧ (Lt(j,w) ∧ (r · i + j = p · q + t ∧ (Lt(t,p) ∧ BetaAt(b,c,k,t))))
    Exact native replay linehave hold : exists i j q t. (k = w * i + j /\ ((exists gap. gap + S j = w) /\ ((r * i + j = p * q + t) /\ ((exists gap. gap + S t = p) /\ (((exists ff_h_ftrg_extend_old_entry. ff_h_ftrg_extend_old_entry + S (t) = S ((S (k)) * c)) /\ exists ff_q_ftrg_extend_old_entry. b = ff_q_ftrg_extend_old_entry * S ((S (k)) * c) + (t)))))))
  53. 0053apply hprevious
  54. 0054exact hsplit_right
  55. 0055cases hold
  56. 0056cases hold_witness
  57. 0057cases hold_witness_witness
  58. 0058cases hold_witness_witness_witness
  59. 0059cases hold_witness_witness_witness_witness
  60. 0060cases hold_witness_witness_witness_witness_right
  61. 0061cases hold_witness_witness_witness_witness_right_right
  62. 0062cases hold_witness_witness_witness_witness_right_right_right
  63. 0063exists x6
  64. 0064exists x7
  65. 0065exists x8
  66. 0066exists x9
  67. 0067split
  68. 0068exact hold_witness_witness_witness_witness_left
  69. 0069split
  70. 0070exact hold_witness_witness_witness_witness_right_left
  71. 0071split
  72. 0072exact hold_witness_witness_witness_witness_right_right_left
  73. 0073split
  74. 0074exact hold_witness_witness_witness_witness_right_right_right_left
  75. 0075specialize hextension_witness_witness_right k
  76. 0076specialize hextension_witness_witness_right x9
  77. 0077apply hextension_witness_witness_right
  78. 0078exact hsplit_right
  79. 0079exact hold_witness_witness_witness_witness_right_right_right_right