PA00CS · theorem

beta_magnitude_predecessor_recode_aligned_half_range

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

The magnitude-predecessor code aligns positive magnitudes with the canonical half range.

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

∀ b. ∀ c. ∀ mb. ∀ mc. ∀ rb. ∀ rc. ∀ h. Range(b,c,1,h) → (∀ x. Lt(x,h) → ∃ y. BetaAt(mb,mc,x,y) ∧ (Lt(0,y) ∧ Le(y,h))) → (∀ x. ∀ y. Lt(x,h) → BetaAt(mb,mc,x,S y) → BetaAt(rb,rc,x,y)) → ∀ x. ∀ y. ∀ z. Lt(x,h) → BetaAt(rb,rc,x,y) → BetaAt(b,c,y,z) → BetaAt(mb,mc,x,z)

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 PD0018 Range

12 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

6 occurrences

Exact expanded native-PA statement
forall b c mb mc rb rc h. (forall gsp_range_index_ges_half. (exists gsp_lt_gap_ges_half_range_bound. gsp_lt_gap_ges_half_range_bound + S gsp_range_index_ges_half = h) -> (((exists gsp_beta_height_ges_half_range_entry. gsp_beta_height_ges_half_range_entry + S (1 + gsp_range_index_ges_half) = S ((S (gsp_range_index_ges_half)) * c)) /\ exists gsp_beta_quotient_ges_half_range_entry. b = gsp_beta_quotient_ges_half_range_entry * S ((S (gsp_range_index_ges_half)) * c) + (1 + gsp_range_index_ges_half)))) -> (forall gmp_index_ges_magnitude_range. (exists gsp_lt_gap_ges_magnitude_range_index_bound. gsp_lt_gap_ges_magnitude_range_index_bound + S gmp_index_ges_magnitude_range = h) -> exists gmp_magnitude_ges_magnitude_range. ((((exists ff_h_gmp_ges_magnitude_range_decoded. ff_h_gmp_ges_magnitude_range_decoded + S (gmp_magnitude_ges_magnitude_range) = S ((S (gmp_index_ges_magnitude_range)) * mc)) /\ exists ff_q_gmp_ges_magnitude_range_decoded. mb = ff_q_gmp_ges_magnitude_range_decoded * S ((S (gmp_index_ges_magnitude_range)) * mc) + (gmp_magnitude_ges_magnitude_range))) /\ ((exists gsp_lt_gap_ges_magnitude_range_positive. gsp_lt_gap_ges_magnitude_range_positive + S 0 = gmp_magnitude_ges_magnitude_range) /\ (exists gsp_le_gap_ges_magnitude_range_bounded. gsp_le_gap_ges_magnitude_range_bounded + gmp_magnitude_ges_magnitude_range = h)))) -> (forall gmp_index_ges_recode gmp_predecessor_ges_recode. (exists gsp_lt_gap_ges_recode_index_bound. gsp_lt_gap_ges_recode_index_bound + S gmp_index_ges_recode = h) -> (((exists gsp_beta_height_gmp_ges_recode_source. gsp_beta_height_gmp_ges_recode_source + S (S gmp_predecessor_ges_recode) = S ((S (gmp_index_ges_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_ges_recode_source. mb = gsp_beta_quotient_gmp_ges_recode_source * S ((S (gmp_index_ges_recode)) * mc) + (S gmp_predecessor_ges_recode))) -> (((exists ff_h_gmp_ges_recode_target. ff_h_gmp_ges_recode_target + S (gmp_predecessor_ges_recode) = S ((S (gmp_index_ges_recode)) * rc)) /\ exists ff_q_gmp_ges_recode_target. rb = ff_q_gmp_ges_recode_target * S ((S (gmp_index_ges_recode)) * rc) + (gmp_predecessor_ges_recode)))) -> (forall fpr_i_ges_alignment fpr_j_ges_alignment fpr_x_ges_alignment. (exists fpr_h_ges_alignment. fpr_h_ges_alignment + S fpr_i_ges_alignment = h) -> (((exists ff_h_ges_alignment_map. ff_h_ges_alignment_map + S (fpr_j_ges_alignment) = S ((S (fpr_i_ges_alignment)) * rc)) /\ exists ff_q_ges_alignment_map. rb = ff_q_ges_alignment_map * S ((S (fpr_i_ges_alignment)) * rc) + (fpr_j_ges_alignment))) -> (((exists ff_h_ges_alignment_source. ff_h_ges_alignment_source + S (fpr_x_ges_alignment) = S ((S (fpr_j_ges_alignment)) * c)) /\ exists ff_q_ges_alignment_source. b = ff_q_ges_alignment_source * S ((S (fpr_j_ges_alignment)) * c) + (fpr_x_ges_alignment))) -> (((exists ff_h_ges_alignment_target. ff_h_ges_alignment_target + S (fpr_x_ges_alignment) = S ((S (fpr_i_ges_alignment)) * mc)) /\ exists ff_q_ges_alignment_target. mb = ff_q_ges_alignment_target * S ((S (fpr_i_ges_alignment)) * mc) + (fpr_x_ges_alignment))))

Proof neighborhood

Direct theorem prerequisites

PA007T beta_magnitude_predecessor_recode_reflect PA002F beta_at_unique PA000E add_succ_left PA0001 zero_add

Direct theorem dependents

PA00CY beta_magnitude_sum_permutation_exact

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

77 script commands · 12 reading checkpoints · 8 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 (4)
beta magnitude predecessor recode reflectbeta at uniqueadd succ leftzero add
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro mb
  4. L4
    intro mc
  5. L5
    intro rb
  6. L6
    intro rc
  7. L7
    intro h
  8. L8
    intro hhalf
  9. L9
    intro hrange
  10. L10
    intro hrecode
02Fix variables and assumptionsL11–16

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

  1. L11
    intro i
  2. L12
    intro j
  3. L13
    intro v
  4. L14
    intro hi
  5. L15
    intro hmap
  6. L16
    intro hsource
03Establish hmagnitude_succL17–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode reflect.

  1. L17
    have hmagnitude_succ : BetaAt(mb,mc,i,S j)Definitions: BetaAt(mb,mc,i,S j)Original native command in the exact edition
  2. L18
    specialize beta_magnitude_predecessor_recode_reflect mb
  3. L19
    specialize beta_magnitude_predecessor_recode_reflect mc
  4. L20
    specialize beta_magnitude_predecessor_recode_reflect rb
  5. L21
    specialize beta_magnitude_predecessor_recode_reflect rc
  6. L22
    specialize beta_magnitude_predecessor_recode_reflect h
  7. L23
    specialize beta_magnitude_predecessor_recode_reflect h
  8. L24
    specialize beta_magnitude_predecessor_recode_reflect i
  9. L25
    specialize beta_magnitude_predecessor_recode_reflect j
  10. L26
    apply beta_magnitude_predecessor_recode_reflect
04Use earlier factsL27–30

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

  1. L27
    exact hrange
  2. L28
    exact hrecode
  3. L29
    exact hi
  4. L30
    exact hmap
05Establish hrange_iL31–34

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

  1. L31
    have hrange_i : ∃ m. BetaAt(mb,mc,i,m) ∧ (Lt(0,m) ∧ Le(m,h))Definitions: BetaAt(mb,mc,i,m)Lt(0,m)Le(m,h)Original native command in the exact edition
  2. L32
    specialize hrange i
  3. L33
    apply hrange
  4. L34
    exact hi
06Separate the logical casesL35–37

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

  1. L35
    cases hrange_i
  2. L36
    cases hrange_i_witness
  3. L37
    cases hrange_i_witness_right
07Establish hmagnitude_eqL38–46

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

  1. L38
    have hmagnitude_eq : x = S j
  2. L39
    specialize beta_at_unique mb
  3. L40
    specialize beta_at_unique mc
  4. L41
    specialize beta_at_unique i
  5. L42
    specialize beta_at_unique x
  6. L43
    specialize beta_at_unique (S j)
  7. L44
    apply beta_at_unique
  8. L45
    exact hrange_i_witness_left
  9. L46
    exact hmagnitude_succ
08Establish hjL47–49

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

  1. L47
  2. L48
    rewrite <- hmagnitude_eq
  3. L49
    exact hrange_i_witness_right_right
09Establish hcanonicalL50–53

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

  1. L50
    have hcanonical : BetaAt(b,c,j,1 + j)Definitions: BetaAt(b,c,j,1 + j)Original native command in the exact edition
  2. L51
    specialize hhalf j
  3. L52
    apply hhalf
  4. L53
    exact hj
10Establish hvL54–62

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

  1. L54
    have hv : v = 1 + j
  2. L55
    specialize beta_at_unique b
  3. L56
    specialize beta_at_unique c
  4. L57
    specialize beta_at_unique j
  5. L58
    specialize beta_at_unique v
  6. L59
    specialize beta_at_unique (1 + j)
  7. L60
    apply beta_at_unique
  8. L61
    exact hsource
  9. L62
    exact hcanonical
11Establish honeL63–70

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

  1. L63
    have hone : 1 + j = S j
  2. L64
    specialize add_succ_left 0
  3. L65
    specialize add_succ_left j
  4. L66
    trans S (0 + j)
  5. L67
    exact add_succ_left
  6. L68
    congr
  7. L69
    specialize zero_add j
  8. L70
    exact zero_add
12Establish hv_succL71–77

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

  1. L71
    have hv_succ : v = S j
  2. L72
    trans 1 + j
  3. L73
    exact hv
  4. L74
    exact hone
  5. L75
    rewrite <- hv_succ at hmagnitude_succ
  6. L76
    rewrite <- hv_succ at hmagnitude_succ
  7. L77
    exact hmagnitude_succ

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro mb
  4. 0004intro mc
  5. 0005intro rb
  6. 0006intro rc
  7. 0007intro h
  8. 0008intro hhalf
  9. 0009intro hrange
  10. 0010intro hrecode
  11. 0011intro i
  12. 0012intro j
  13. 0013intro v
  14. 0014intro hi
  15. 0015intro hmap
  16. 0016intro hsource
  17. 0017have hmagnitude_succ : BetaAt(mb,mc,i,S j)
    Exact native replay linehave hmagnitude_succ : ((exists gsp_beta_height_ges_proof_magnitude_succ. gsp_beta_height_ges_proof_magnitude_succ + S (S j) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_ges_proof_magnitude_succ. mb = gsp_beta_quotient_ges_proof_magnitude_succ * S ((S (i)) * mc) + (S j))
  18. 0018specialize beta_magnitude_predecessor_recode_reflect mb
  19. 0019specialize beta_magnitude_predecessor_recode_reflect mc
  20. 0020specialize beta_magnitude_predecessor_recode_reflect rb
  21. 0021specialize beta_magnitude_predecessor_recode_reflect rc
  22. 0022specialize beta_magnitude_predecessor_recode_reflect h
  23. 0023specialize beta_magnitude_predecessor_recode_reflect h
  24. 0024specialize beta_magnitude_predecessor_recode_reflect i
  25. 0025specialize beta_magnitude_predecessor_recode_reflect j
  26. 0026apply beta_magnitude_predecessor_recode_reflect
  27. 0027exact hrange
  28. 0028exact hrecode
  29. 0029exact hi
  30. 0030exact hmap
  31. 0031have hrange_i : ∃ m. BetaAt(mb,mc,i,m) ∧ (Lt(0,m) ∧ Le(m,h))
    Exact native replay linehave hrange_i : exists m. (((exists ff_h_ges_proof_range_entry. ff_h_ges_proof_range_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_ges_proof_range_entry. mb = ff_q_ges_proof_range_entry * S ((S (i)) * mc) + (m))) /\ ((exists g. g + S 0 = m) /\ exists g. g + m = h)
  32. 0032specialize hrange i
  33. 0033apply hrange
  34. 0034exact hi
  35. 0035cases hrange_i
  36. 0036cases hrange_i_witness
  37. 0037cases hrange_i_witness_right
  38. 0038have hmagnitude_eq : x = S j
  39. 0039specialize beta_at_unique mb
  40. 0040specialize beta_at_unique mc
  41. 0041specialize beta_at_unique i
  42. 0042specialize beta_at_unique x
  43. 0043specialize beta_at_unique (S j)
  44. 0044apply beta_at_unique
  45. 0045exact hrange_i_witness_left
  46. 0046exact hmagnitude_succ
  47. 0047have hj : Lt(j,h)
    Exact native replay linehave hj : exists g. g + S j = h
  48. 0048rewrite <- hmagnitude_eq
  49. 0049exact hrange_i_witness_right_right
  50. 0050have hcanonical : BetaAt(b,c,j,1 + j)
    Exact native replay linehave hcanonical : ((exists gsp_beta_height_ges_proof_canonical. gsp_beta_height_ges_proof_canonical + S (1 + j) = S ((S (j)) * c)) /\ exists gsp_beta_quotient_ges_proof_canonical. b = gsp_beta_quotient_ges_proof_canonical * S ((S (j)) * c) + (1 + j))
  51. 0051specialize hhalf j
  52. 0052apply hhalf
  53. 0053exact hj
  54. 0054have hv : v = 1 + j
  55. 0055specialize beta_at_unique b
  56. 0056specialize beta_at_unique c
  57. 0057specialize beta_at_unique j
  58. 0058specialize beta_at_unique v
  59. 0059specialize beta_at_unique (1 + j)
  60. 0060apply beta_at_unique
  61. 0061exact hsource
  62. 0062exact hcanonical
  63. 0063have hone : 1 + j = S j
  64. 0064specialize add_succ_left 0
  65. 0065specialize add_succ_left j
  66. 0066trans S (0 + j)
  67. 0067exact add_succ_left
  68. 0068congr
  69. 0069specialize zero_add j
  70. 0070exact zero_add
  71. 0071have hv_succ : v = S j
  72. 0072trans 1 + j
  73. 0073exact hv
  74. 0074exact hone
  75. 0075rewrite <- hv_succ at hmagnitude_succ
  76. 0076rewrite <- hv_succ at hmagnitude_succ
  77. 0077exact hmagnitude_succ