PA009S · theorem

adjacent_scaled_orbit_history_append

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

Append one adjacent pair while retaining its raw At(i,S j) scaled edge.

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

∀ u. ∀ v. ∀ b. ∀ c. ∀ z. ∀ d. ∀ m. ∀ i. ∀ j. (∀ x. Lt(x,m) → ∃ y. ∃ n. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),n) ∧ BetaAt(u,v,y,S n))) → BetaAt(z,d,m + m,i) ∧ (BetaAt(z,d,S (m + m),j) ∧ (∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))) → BetaAt(u,v,i,S j) → ∀ x. Lt(x,S m) → ∃ y. ∃ n. BetaAt(z,d,x + x,y) ∧ (BetaAt(z,d,S (x + x),n) ∧ BetaAt(u,v,y,S n))

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

14 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

6 occurrences

Exact expanded native-PA statement
forall u v b c z d m i j. (forall espi_pair_append_old_history. (exists wpo_gap_append_old_history_pair_bound. wpo_gap_append_old_history_pair_bound + S (espi_pair_append_old_history) = m) -> exists espi_left_append_old_history espi_right_append_old_history. (((((exists wpo_beta_height_append_old_history_left_entry. wpo_beta_height_append_old_history_left_entry + S (espi_left_append_old_history) = S ((S (espi_pair_append_old_history + espi_pair_append_old_history)) * c)) /\ exists wpo_beta_quotient_append_old_history_left_entry. b = wpo_beta_quotient_append_old_history_left_entry * S ((S (espi_pair_append_old_history + espi_pair_append_old_history)) * c) + (espi_left_append_old_history))) /\ (((((exists wpo_beta_height_append_old_history_right_entry. wpo_beta_height_append_old_history_right_entry + S (espi_right_append_old_history) = S ((S (S (espi_pair_append_old_history + espi_pair_append_old_history))) * c)) /\ exists wpo_beta_quotient_append_old_history_right_entry. b = wpo_beta_quotient_append_old_history_right_entry * S ((S (S (espi_pair_append_old_history + espi_pair_append_old_history))) * c) + (espi_right_append_old_history))) /\ (((exists wpo_beta_height_append_old_history_scaled_edge. wpo_beta_height_append_old_history_scaled_edge + S (S espi_right_append_old_history) = S ((S (espi_left_append_old_history)) * v)) /\ exists wpo_beta_quotient_append_old_history_scaled_edge. u = wpo_beta_quotient_append_old_history_scaled_edge * S ((S (espi_left_append_old_history)) * v) + (S espi_right_append_old_history)))))))) -> (((((exists wpo_beta_height_append_trace_first. wpo_beta_height_append_trace_first + S (i) = S ((S (m + m)) * d)) /\ exists wpo_beta_quotient_append_trace_first. z = wpo_beta_quotient_append_trace_first * S ((S (m + m)) * d) + (i))) /\ ((((exists wpo_beta_height_append_trace_second. wpo_beta_height_append_trace_second + S (j) = S ((S (S (m + m))) * d)) /\ exists wpo_beta_quotient_append_trace_second. z = wpo_beta_quotient_append_trace_second * S ((S (S (m + m))) * d) + (j))) /\ (forall wpo_old_index_append_trace wpo_old_value_append_trace. (exists wpo_gap_append_trace_old_bound. wpo_gap_append_trace_old_bound + S (wpo_old_index_append_trace) = m + m) -> (((exists wpo_beta_height_append_trace_old_entry. wpo_beta_height_append_trace_old_entry + S (wpo_old_value_append_trace) = S ((S (wpo_old_index_append_trace)) * c)) /\ exists wpo_beta_quotient_append_trace_old_entry. b = wpo_beta_quotient_append_trace_old_entry * S ((S (wpo_old_index_append_trace)) * c) + (wpo_old_value_append_trace))) -> (((exists wpo_beta_height_append_trace_new_entry. wpo_beta_height_append_trace_new_entry + S (wpo_old_value_append_trace) = S ((S (wpo_old_index_append_trace)) * d)) /\ exists wpo_beta_quotient_append_trace_new_entry. z = wpo_beta_quotient_append_trace_new_entry * S ((S (wpo_old_index_append_trace)) * d) + (wpo_old_value_append_trace))))))) -> (((exists wpo_beta_height_append_forward. wpo_beta_height_append_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_append_forward. u = wpo_beta_quotient_append_forward * S ((S (i)) * v) + (S j))) -> (forall espi_pair_append_new_history. (exists wpo_gap_append_new_history_pair_bound. wpo_gap_append_new_history_pair_bound + S (espi_pair_append_new_history) = S m) -> exists espi_left_append_new_history espi_right_append_new_history. (((((exists wpo_beta_height_append_new_history_left_entry. wpo_beta_height_append_new_history_left_entry + S (espi_left_append_new_history) = S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d)) /\ exists wpo_beta_quotient_append_new_history_left_entry. z = wpo_beta_quotient_append_new_history_left_entry * S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d) + (espi_left_append_new_history))) /\ (((((exists wpo_beta_height_append_new_history_right_entry. wpo_beta_height_append_new_history_right_entry + S (espi_right_append_new_history) = S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d)) /\ exists wpo_beta_quotient_append_new_history_right_entry. z = wpo_beta_quotient_append_new_history_right_entry * S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d) + (espi_right_append_new_history))) /\ (((exists wpo_beta_height_append_new_history_scaled_edge. wpo_beta_height_append_new_history_scaled_edge + S (S espi_right_append_new_history) = S ((S (espi_left_append_new_history)) * v)) /\ exists wpo_beta_quotient_append_new_history_scaled_edge. u = wpo_beta_quotient_append_new_history_scaled_edge * S ((S (espi_left_append_new_history)) * v) + (S espi_right_append_new_history))))))))

Proof neighborhood

Direct theorem prerequisites

PA003D finite_lt_succ_eq_or_lt PA009Q pair_index_left_below_double PA009R pair_index_right_below_double

Direct theorem dependents

PA009T scaled_inverse_pair_order_paired_state_step

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

73 script commands · 24 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)
finite lt succ eq or ltpair index left below doublepair index right below double
01Fix variables and assumptionsL1–10

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

  1. L1
    intro u
  2. L2
    intro v
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro z
  6. L6
    intro d
  7. L7
    intro m
  8. L8
    intro i
  9. L9
    intro j
  10. L10
    intro hold
02Fix variables and assumptionsL11–12

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

  1. L11
    intro htrace
  2. L12
    intro hforward
03Separate the logical casesL13–14

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

  1. L13
    cases htrace
  2. L14
    cases htrace_right
04Fix variables and assumptionsL15–16

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

  1. L15
    intro t
  2. L16
    intro ht
05Establish hsplitL17–21

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. L17
    have hsplit : t = m ∨ Lt(t,m)Definitions: Lt(t,m)Original native command in the exact edition
  2. L18
    specialize finite_lt_succ_eq_or_lt m
  3. L19
    specialize finite_lt_succ_eq_or_lt t
  4. L20
    apply finite_lt_succ_eq_or_lt
  5. L21
    exact ht
06Separate the logical casesL22–22

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

  1. L22
    cases hsplit
07Establish hleft_positionL23–26

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

  1. L23
    have hleft_position : t + t = m + m
  2. L24
    rewrite hsplit_left
  3. L25
    rewrite hsplit_left
  4. L26
    refl
08Establish hright_positionL27–29

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

  1. L27
    have hright_position : S (t + t) = S (m + m)
  2. L28
    congr
  3. L29
    exact hleft_position
09Construct an explicit witnessL30–31

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

  1. L30
    exists i
  2. L31
    exists j
10Separate the logical casesL32–32

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

  1. L32
    split
11Calculate and transport equalitiesL33–34

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

  1. L33
    rewrite hleft_position
  2. L34
    rewrite hleft_position
12Use earlier factsL35–35

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

  1. L35
    exact htrace_left
13Separate the logical casesL36–36

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

  1. L36
    split
14Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite hright_position
  2. L38
    rewrite hright_position
15Use earlier factsL39–40

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

  1. L39
    exact htrace_right_left
  2. L40
    exact hforward
16Establish hold_atL41–44

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

  1. L41
    have hold_at : ∃ oi. ∃ oj. BetaAt(b,c,t + t,oi) ∧ (BetaAt(b,c,S (t + t),oj) ∧ BetaAt(u,v,oi,S oj))Definitions: BetaAt(b,c,t + t,oi)BetaAt(b,c,S (t + t),oj)BetaAt(u,v,oi,S oj)Original native command in the exact edition
  2. L42
    specialize hold t
  3. L43
    apply hold
  4. L44
    exact hsplit_right
17Separate the logical casesL45–48

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

  1. L45
    cases hold_at
  2. L46
    cases hold_at_witness
  3. L47
    cases hold_at_witness_witness
  4. L48
    cases hold_at_witness_witness_right
18Establish hleft_boundL49–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair index left below double.

  1. L49
    have hleft_bound : Lt(t + t,m + m)Definitions: Lt(t + t,m + m)Original native command in the exact edition
  2. L50
    specialize pair_index_left_below_double t
  3. L51
    specialize pair_index_left_below_double m
  4. L52
    apply pair_index_left_below_double
  5. L53
    exact hsplit_right
19Establish hright_boundL54–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair index right below double.

  1. L54
    have hright_bound : Lt(S (t + t),m + m)Definitions: Lt(S (t + t),m + m)Original native command in the exact edition
  2. L55
    specialize pair_index_right_below_double t
  3. L56
    specialize pair_index_right_below_double m
  4. L57
    apply pair_index_right_below_double
  5. L58
    exact hsplit_right
20Construct an explicit witnessL59–60

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

  1. L59
    exists x
  2. L60
    exists x1
21Separate the logical casesL61–61

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

  1. L61
    split
22Use earlier factsL62–66

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

  1. L62
    specialize htrace_right_right (t + t)
  2. L63
    specialize htrace_right_right x
  3. L64
    apply htrace_right_right
  4. L65
    exact hleft_bound
  5. L66
    exact hold_at_witness_witness_left
23Separate the logical casesL67–67

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

  1. L67
    split
24Use earlier factsL68–73

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

  1. L68
    specialize htrace_right_right (S (t + t))
  2. L69
    specialize htrace_right_right x1
  3. L70
    apply htrace_right_right
  4. L71
    exact hright_bound
  5. L72
    exact hold_at_witness_witness_right_left
  6. L73
    exact hold_at_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 73 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro m
  8. 0008intro i
  9. 0009intro j
  10. 0010intro hold
  11. 0011intro htrace
  12. 0012intro hforward
  13. 0013cases htrace
  14. 0014cases htrace_right
  15. 0015intro t
  16. 0016intro ht
  17. 0017have hsplit : t = m ∨ Lt(t,m)
    Exact native replay linehave hsplit : t = m \/ exists h. h + S t = m
  18. 0018specialize finite_lt_succ_eq_or_lt m
  19. 0019specialize finite_lt_succ_eq_or_lt t
  20. 0020apply finite_lt_succ_eq_or_lt
  21. 0021exact ht
  22. 0022cases hsplit
  23. 0023have hleft_position : t + t = m + m
  24. 0024rewrite hsplit_left
  25. 0025rewrite hsplit_left
  26. 0026refl
  27. 0027have hright_position : S (t + t) = S (m + m)
  28. 0028congr
  29. 0029exact hleft_position
  30. 0030exists i
  31. 0031exists j
  32. 0032split
  33. 0033rewrite hleft_position
  34. 0034rewrite hleft_position
  35. 0035exact htrace_left
  36. 0036split
  37. 0037rewrite hright_position
  38. 0038rewrite hright_position
  39. 0039exact htrace_right_left
  40. 0040exact hforward
  41. 0041have hold_at : ∃ oi. ∃ oj. BetaAt(b,c,t + t,oi) ∧ (BetaAt(b,c,S (t + t),oj) ∧ BetaAt(u,v,oi,S oj))
    Exact native replay linehave hold_at : exists oi oj. ((((exists wpo_beta_height_old_history_left. wpo_beta_height_old_history_left + S (oi) = S ((S (t + t)) * c)) /\ exists wpo_beta_quotient_old_history_left. b = wpo_beta_quotient_old_history_left * S ((S (t + t)) * c) + (oi))) /\ (((((exists wpo_beta_height_old_history_right. wpo_beta_height_old_history_right + S (oj) = S ((S (S (t + t))) * c)) /\ exists wpo_beta_quotient_old_history_right. b = wpo_beta_quotient_old_history_right * S ((S (S (t + t))) * c) + (oj))) /\ (((exists wpo_beta_height_old_history_edge. wpo_beta_height_old_history_edge + S (S oj) = S ((S (oi)) * v)) /\ exists wpo_beta_quotient_old_history_edge. u = wpo_beta_quotient_old_history_edge * S ((S (oi)) * v) + (S oj))))))
  42. 0042specialize hold t
  43. 0043apply hold
  44. 0044exact hsplit_right
  45. 0045cases hold_at
  46. 0046cases hold_at_witness
  47. 0047cases hold_at_witness_witness
  48. 0048cases hold_at_witness_witness_right
  49. 0049have hleft_bound : Lt(t + t,m + m)
    Exact native replay linehave hleft_bound : exists h. h + S (t + t) = m + m
  50. 0050specialize pair_index_left_below_double t
  51. 0051specialize pair_index_left_below_double m
  52. 0052apply pair_index_left_below_double
  53. 0053exact hsplit_right
  54. 0054have hright_bound : Lt(S (t + t),m + m)
    Exact native replay linehave hright_bound : exists h. h + S (S (t + t)) = m + m
  55. 0055specialize pair_index_right_below_double t
  56. 0056specialize pair_index_right_below_double m
  57. 0057apply pair_index_right_below_double
  58. 0058exact hsplit_right
  59. 0059exists x
  60. 0060exists x1
  61. 0061split
  62. 0062specialize htrace_right_right (t + t)
  63. 0063specialize htrace_right_right x
  64. 0064apply htrace_right_right
  65. 0065exact hleft_bound
  66. 0066exact hold_at_witness_witness_left
  67. 0067split
  68. 0068specialize htrace_right_right (S (t + t))
  69. 0069specialize htrace_right_right x1
  70. 0070apply htrace_right_right
  71. 0071exact hright_bound
  72. 0072exact hold_at_witness_witness_right_left
  73. 0073exact hold_at_witness_witness_right_right