PA00BB · theorem

pair_order_terminal_state_magnitude_range

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

A terminal PairOrder state decodes exactly positive values bounded by its length.

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. ∀ l. ∀ n. n = S S l → (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,y,z) → ContainsPrefix(b,c,l,z)) ∧ ((∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ ((∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → ¬y = 0 ∧ ¬S y = n) ∧ InjectivePrefix(b,c,l))) → ∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ (Lt(0,y) ∧ Le(y,l))

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

PD0001 Le PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

14 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall u v b c l n. n = S (S l) -> (((forall wpo_position_wtp_terminal_state_closed wpo_source_wtp_terminal_state_closed wpo_mate_wtp_terminal_state_closed. (exists wpo_gap_wtp_terminal_state_closed_position_bound. wpo_gap_wtp_terminal_state_closed_position_bound + S (wpo_position_wtp_terminal_state_closed) = l) -> (((exists wpo_beta_height_wtp_terminal_state_closed_source_entry. wpo_beta_height_wtp_terminal_state_closed_source_entry + S (wpo_source_wtp_terminal_state_closed) = S ((S (wpo_position_wtp_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_closed_source_entry. b = wpo_beta_quotient_wtp_terminal_state_closed_source_entry * S ((S (wpo_position_wtp_terminal_state_closed)) * c) + (wpo_source_wtp_terminal_state_closed))) -> (((exists wpo_beta_height_wtp_terminal_state_closed_inverse_entry. wpo_beta_height_wtp_terminal_state_closed_inverse_entry + S (wpo_mate_wtp_terminal_state_closed) = S ((S (wpo_source_wtp_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_wtp_terminal_state_closed_inverse_entry. u = wpo_beta_quotient_wtp_terminal_state_closed_inverse_entry * S ((S (wpo_source_wtp_terminal_state_closed)) * v) + (wpo_mate_wtp_terminal_state_closed))) -> exists wpo_mate_position_wtp_terminal_state_closed. ((exists wpo_gap_wtp_terminal_state_closed_mate_bound. wpo_gap_wtp_terminal_state_closed_mate_bound + S (wpo_mate_position_wtp_terminal_state_closed) = l) /\ (((exists wpo_beta_height_wtp_terminal_state_closed_mate_entry. wpo_beta_height_wtp_terminal_state_closed_mate_entry + S (wpo_mate_wtp_terminal_state_closed) = S ((S (wpo_mate_position_wtp_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_closed_mate_entry. b = wpo_beta_quotient_wtp_terminal_state_closed_mate_entry * S ((S (wpo_mate_position_wtp_terminal_state_closed)) * c) + (wpo_mate_wtp_terminal_state_closed))))) /\ ((forall fom_index_wtp_terminal_state_bounded. (exists fom_gap_wtp_terminal_state_bounded_index_bound. fom_gap_wtp_terminal_state_bounded_index_bound + S (fom_index_wtp_terminal_state_bounded) = l) -> exists fom_value_wtp_terminal_state_bounded. ((((exists fom_beta_height_wtp_terminal_state_bounded_entry. fom_beta_height_wtp_terminal_state_bounded_entry + S (fom_value_wtp_terminal_state_bounded) = S ((S (fom_index_wtp_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_wtp_terminal_state_bounded_entry. b = fom_beta_quotient_wtp_terminal_state_bounded_entry * S ((S (fom_index_wtp_terminal_state_bounded)) * c) + (fom_value_wtp_terminal_state_bounded))) /\ (exists fom_gap_wtp_terminal_state_bounded_value_bound. fom_gap_wtp_terminal_state_bounded_value_bound + S (fom_value_wtp_terminal_state_bounded) = n))) /\ ((forall wpo_position_wtp_terminal_state_nonendpoint wpo_value_wtp_terminal_state_nonendpoint. (exists wpo_gap_wtp_terminal_state_nonendpoint_position_bound. wpo_gap_wtp_terminal_state_nonendpoint_position_bound + S (wpo_position_wtp_terminal_state_nonendpoint) = l) -> (((exists wpo_beta_height_wtp_terminal_state_nonendpoint_entry. wpo_beta_height_wtp_terminal_state_nonendpoint_entry + S (wpo_value_wtp_terminal_state_nonendpoint) = S ((S (wpo_position_wtp_terminal_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_nonendpoint_entry. b = wpo_beta_quotient_wtp_terminal_state_nonendpoint_entry * S ((S (wpo_position_wtp_terminal_state_nonendpoint)) * c) + (wpo_value_wtp_terminal_state_nonendpoint))) -> (~(wpo_value_wtp_terminal_state_nonendpoint = 0) /\ ~((S wpo_value_wtp_terminal_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_terminal_state_injective wpo_injective_right_wtp_terminal_state_injective wpo_injective_value_wtp_terminal_state_injective. (exists wpo_gap_wtp_terminal_state_injective_left_bound. wpo_gap_wtp_terminal_state_injective_left_bound + S (wpo_injective_left_wtp_terminal_state_injective) = l) -> (exists wpo_gap_wtp_terminal_state_injective_right_bound. wpo_gap_wtp_terminal_state_injective_right_bound + S (wpo_injective_right_wtp_terminal_state_injective) = l) -> (((exists wpo_beta_height_wtp_terminal_state_injective_left_entry. wpo_beta_height_wtp_terminal_state_injective_left_entry + S (wpo_injective_value_wtp_terminal_state_injective) = S ((S (wpo_injective_left_wtp_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_injective_left_entry. b = wpo_beta_quotient_wtp_terminal_state_injective_left_entry * S ((S (wpo_injective_left_wtp_terminal_state_injective)) * c) + (wpo_injective_value_wtp_terminal_state_injective))) -> (((exists wpo_beta_height_wtp_terminal_state_injective_right_entry. wpo_beta_height_wtp_terminal_state_injective_right_entry + S (wpo_injective_value_wtp_terminal_state_injective) = S ((S (wpo_injective_right_wtp_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_injective_right_entry. b = wpo_beta_quotient_wtp_terminal_state_injective_right_entry * S ((S (wpo_injective_right_wtp_terminal_state_injective)) * c) + (wpo_injective_value_wtp_terminal_state_injective))) -> wpo_injective_left_wtp_terminal_state_injective = wpo_injective_right_wtp_terminal_state_injective))))) -> (forall gmp_index_wtp_terminal_range. (exists gsp_lt_gap_wtp_terminal_range_index_bound. gsp_lt_gap_wtp_terminal_range_index_bound + S gmp_index_wtp_terminal_range = l) -> exists gmp_magnitude_wtp_terminal_range. ((((exists ff_h_gmp_wtp_terminal_range_decoded. ff_h_gmp_wtp_terminal_range_decoded + S (gmp_magnitude_wtp_terminal_range) = S ((S (gmp_index_wtp_terminal_range)) * c)) /\ exists ff_q_gmp_wtp_terminal_range_decoded. b = ff_q_gmp_wtp_terminal_range_decoded * S ((S (gmp_index_wtp_terminal_range)) * c) + (gmp_magnitude_wtp_terminal_range))) /\ ((exists gsp_lt_gap_wtp_terminal_range_positive. gsp_lt_gap_wtp_terminal_range_positive + S 0 = gmp_magnitude_wtp_terminal_range) /\ (exists gsp_le_gap_wtp_terminal_range_bounded. gsp_le_gap_wtp_terminal_range_bounded + gmp_magnitude_wtp_terminal_range = l))))

Proof neighborhood

Direct theorem prerequisites

PA002L one_le_of_ne_zero PA000V le_of_succ_le_succ PA000W le_eq_or_lt

Direct theorem dependents

PA00BE prime_wilson_terminal_product_package_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

54 script commands · 19 reading checkpoints · 4 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)
one le of ne zerole of succ le succle eq or lt
01Fix variables and assumptionsL1–8

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 l
  6. L6
    intro n
  7. L7
    intro hterminal
  8. L8
    intro hstate
02Separate the logical casesL9–11

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

  1. L9
    cases hstate
  2. L10
    cases hstate_right
  3. L11
    cases hstate_right_right
03Calculate and transport equalitiesL12–13

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

  1. L12
    rewrite hterminal at hstate_right_left
  2. L13
    rewrite hterminal at hstate_right_right_left
04Fix variables and assumptionsL14–15

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

  1. L14
    intro q
  2. L15
    intro hq
05Establish hentryL16–19

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

  1. L16
    have hentry : ∃ x. BetaAt(b,c,q,x) ∧ Lt(x,S S l)Definitions: BetaAt(b,c,q,x)Lt(x,S S l)Original native command in the exact edition
  2. L17
    specialize hstate_right_left q
  3. L18
    apply hstate_right_left
  4. L19
    exact hq
06Separate the logical casesL20–21

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

  1. L20
    cases hentry
  2. L21
    cases hentry_witness
07Establish hnonendpointL22–27

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

  1. L22
    have hnonendpoint : ~(x = 0) /\ ~((S x) = S (S l))
  2. L23
    specialize hstate_right_right_left q
  3. L24
    specialize hstate_right_right_left x
  4. L25
    apply hstate_right_right_left
  5. L26
    exact hq
  6. L27
    exact hentry_witness_left
08Separate the logical casesL28–28

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

  1. L28
    cases hnonendpoint
09Construct an explicit witnessL29–29

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

  1. L29
    exists x
10Separate the logical casesL30–30

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

  1. L30
    split
11Use earlier factsL31–31

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

  1. L31
    exact hentry_witness_left
12Separate the logical casesL32–32

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

  1. L32
    split
13Use earlier factsL33–35

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

  1. L33
    specialize one_le_of_ne_zero x
  2. L34
    apply one_le_of_ne_zero
  3. L35
    exact hnonendpoint_left
14Establish hxle_succL36–40

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

  1. L36
    have hxle_succ : Le(x,S l)Definitions: Le(x,S l)Original native command in the exact edition
  2. L37
    specialize le_of_succ_le_succ x
  3. L38
    specialize le_of_succ_le_succ (S l)
  4. L39
    apply le_of_succ_le_succ
  5. L40
    exact hentry_witness_right
15Establish hxsplitL41–45

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

  1. L41
    have hxsplit : x = S l ∨ Lt(x,S l)Definitions: Lt(x,S l)Original native command in the exact edition
  2. L42
    specialize le_eq_or_lt x
  3. L43
    specialize le_eq_or_lt (S l)
  4. L44
    apply le_eq_or_lt
  5. L45
    exact hxle_succ
16Separate the logical casesL46–47

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

  1. L46
    cases hxsplit
  2. L47
    exfalso
17Use earlier factsL48–48

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

  1. L48
    apply hnonendpoint_right
18Calculate and transport equalitiesL49–50

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

  1. L49
    rewrite hxsplit_left
  2. L50
    refl
19Use earlier factsL51–54

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

  1. L51
    specialize le_of_succ_le_succ x
  2. L52
    specialize le_of_succ_le_succ l
  3. L53
    apply le_of_succ_le_succ
  4. L54
    exact hxsplit_right

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro n
  7. 0007intro hterminal
  8. 0008intro hstate
  9. 0009cases hstate
  10. 0010cases hstate_right
  11. 0011cases hstate_right_right
  12. 0012rewrite hterminal at hstate_right_left
  13. 0013rewrite hterminal at hstate_right_right_left
  14. 0014intro q
  15. 0015intro hq
  16. 0016have hentry : ∃ x. BetaAt(b,c,q,x) ∧ Lt(x,S S l)
    Exact native replay linehave hentry : exists x. ((((exists wpo_beta_height_wtp_terminal_entry_x. wpo_beta_height_wtp_terminal_entry_x + S (x) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_entry_x. b = wpo_beta_quotient_wtp_terminal_entry_x * S ((S (q)) * c) + (x))) /\ (exists wpo_gap_wtp_terminal_value_bound_x. wpo_gap_wtp_terminal_value_bound_x + S (x) = S (S l)))
  17. 0017specialize hstate_right_left q
  18. 0018apply hstate_right_left
  19. 0019exact hq
  20. 0020cases hentry
  21. 0021cases hentry_witness
  22. 0022have hnonendpoint : ~(x = 0) /\ ~((S x) = S (S l))
  23. 0023specialize hstate_right_right_left q
  24. 0024specialize hstate_right_right_left x
  25. 0025apply hstate_right_right_left
  26. 0026exact hq
  27. 0027exact hentry_witness_left
  28. 0028cases hnonendpoint
  29. 0029exists x
  30. 0030split
  31. 0031exact hentry_witness_left
  32. 0032split
  33. 0033specialize one_le_of_ne_zero x
  34. 0034apply one_le_of_ne_zero
  35. 0035exact hnonendpoint_left
  36. 0036have hxle_succ : Le(x,S l)
    Exact native replay linehave hxle_succ : exists h. h + x = S l
  37. 0037specialize le_of_succ_le_succ x
  38. 0038specialize le_of_succ_le_succ (S l)
  39. 0039apply le_of_succ_le_succ
  40. 0040exact hentry_witness_right
  41. 0041have hxsplit : x = S l ∨ Lt(x,S l)
    Exact native replay linehave hxsplit : x = S l \/ exists h. h + S x = S l
  42. 0042specialize le_eq_or_lt x
  43. 0043specialize le_eq_or_lt (S l)
  44. 0044apply le_eq_or_lt
  45. 0045exact hxle_succ
  46. 0046cases hxsplit
  47. 0047exfalso
  48. 0048apply hnonendpoint_right
  49. 0049rewrite hxsplit_left
  50. 0050refl
  51. 0051specialize le_of_succ_le_succ x
  52. 0052specialize le_of_succ_le_succ l
  53. 0053apply le_of_succ_le_succ
  54. 0054exact hxsplit_right