PA007V · theorem

gauss_predecessor_half_range_aligned

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

The predecessor map aligns canonical factor 1+j with magnitude S j at every position.

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

∀ mb. ∀ mc. ∀ rb. ∀ rc. ∀ b. ∀ c. ∀ 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)) → Range(b,c,1,h) → ∀ 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

PD0002 Lt PD0013 BetaAt PD0024 BoundedPrefix

5 occurrences

Exact expanded native-PA statement
forall mb mc rb rc b c h. (forall gmp_index_product_magnitude_range. (exists gsp_lt_gap_product_magnitude_range_index_bound. gsp_lt_gap_product_magnitude_range_index_bound + S gmp_index_product_magnitude_range = h) -> exists gmp_magnitude_product_magnitude_range. ((((exists ff_h_gmp_product_magnitude_range_decoded. ff_h_gmp_product_magnitude_range_decoded + S (gmp_magnitude_product_magnitude_range) = S ((S (gmp_index_product_magnitude_range)) * mc)) /\ exists ff_q_gmp_product_magnitude_range_decoded. mb = ff_q_gmp_product_magnitude_range_decoded * S ((S (gmp_index_product_magnitude_range)) * mc) + (gmp_magnitude_product_magnitude_range))) /\ ((exists gsp_lt_gap_product_magnitude_range_positive. gsp_lt_gap_product_magnitude_range_positive + S 0 = gmp_magnitude_product_magnitude_range) /\ (exists gsp_le_gap_product_magnitude_range_bounded. gsp_le_gap_product_magnitude_range_bounded + gmp_magnitude_product_magnitude_range = h)))) -> (forall gmp_index_product_predecessor_recode gmp_predecessor_product_predecessor_recode. (exists gsp_lt_gap_product_predecessor_recode_index_bound. gsp_lt_gap_product_predecessor_recode_index_bound + S gmp_index_product_predecessor_recode = h) -> (((exists gsp_beta_height_gmp_product_predecessor_recode_source. gsp_beta_height_gmp_product_predecessor_recode_source + S (S gmp_predecessor_product_predecessor_recode) = S ((S (gmp_index_product_predecessor_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_product_predecessor_recode_source. mb = gsp_beta_quotient_gmp_product_predecessor_recode_source * S ((S (gmp_index_product_predecessor_recode)) * mc) + (S gmp_predecessor_product_predecessor_recode))) -> (((exists ff_h_gmp_product_predecessor_recode_target. ff_h_gmp_product_predecessor_recode_target + S (gmp_predecessor_product_predecessor_recode) = S ((S (gmp_index_product_predecessor_recode)) * rc)) /\ exists ff_q_gmp_product_predecessor_recode_target. rb = ff_q_gmp_product_predecessor_recode_target * S ((S (gmp_index_product_predecessor_recode)) * rc) + (gmp_predecessor_product_predecessor_recode)))) -> (forall gsp_range_index_product_canonical_half_range. (exists gsp_lt_gap_product_canonical_half_range_range_bound. gsp_lt_gap_product_canonical_half_range_range_bound + S gsp_range_index_product_canonical_half_range = h) -> (((exists gsp_beta_height_product_canonical_half_range_range_entry. gsp_beta_height_product_canonical_half_range_range_entry + S (1 + gsp_range_index_product_canonical_half_range) = S ((S (gsp_range_index_product_canonical_half_range)) * c)) /\ exists gsp_beta_quotient_product_canonical_half_range_range_entry. b = gsp_beta_quotient_product_canonical_half_range_range_entry * S ((S (gsp_range_index_product_canonical_half_range)) * c) + (1 + gsp_range_index_product_canonical_half_range)))) -> (forall fpr_i_product_alignment fpr_j_product_alignment fpr_x_product_alignment. (exists fpr_h_product_alignment. fpr_h_product_alignment + S fpr_i_product_alignment = h) -> (((exists ff_h_product_alignment_map. ff_h_product_alignment_map + S (fpr_j_product_alignment) = S ((S (fpr_i_product_alignment)) * rc)) /\ exists ff_q_product_alignment_map. rb = ff_q_product_alignment_map * S ((S (fpr_i_product_alignment)) * rc) + (fpr_j_product_alignment))) -> (((exists ff_h_product_alignment_source. ff_h_product_alignment_source + S (fpr_x_product_alignment) = S ((S (fpr_j_product_alignment)) * c)) /\ exists ff_q_product_alignment_source. b = ff_q_product_alignment_source * S ((S (fpr_j_product_alignment)) * c) + (fpr_x_product_alignment))) -> (((exists ff_h_product_alignment_target. ff_h_product_alignment_target + S (fpr_x_product_alignment) = S ((S (fpr_i_product_alignment)) * mc)) /\ exists ff_q_product_alignment_target. mb = ff_q_product_alignment_target * S ((S (fpr_i_product_alignment)) * mc) + (fpr_x_product_alignment))))

Proof neighborhood

Direct theorem prerequisites

PA007S beta_magnitude_predecessor_recode_bounded PA007T beta_magnitude_predecessor_recode_reflect PA002F beta_at_unique PA0032 beta_range_entry_eq PA000E add_succ_left PA0001 zero_add

Direct theorem dependents

PA007Y gauss_magnitude_product_eq_half_range

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

83 script commands · 13 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 (6)
beta magnitude predecessor recode boundedbeta magnitude predecessor recode reflectbeta at uniquebeta range entry eqadd succ leftzero add
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    have hbounded : BoundedPrefix(rb,rc,h)Definitions: BoundedPrefix(rb,rc,h)Original native command in the exact edition
  2. L12
    specialize beta_magnitude_predecessor_recode_bounded mb
  3. L13
    specialize beta_magnitude_predecessor_recode_bounded mc
  4. L14
    specialize beta_magnitude_predecessor_recode_bounded rb
  5. L15
    specialize beta_magnitude_predecessor_recode_bounded rc
  6. L16
    specialize beta_magnitude_predecessor_recode_bounded h
  7. L17
    apply beta_magnitude_predecessor_recode_bounded
  8. L18
    exact hrange
  9. L19
    exact hrecode
  10. L20
    intro i
03Fix variables and assumptionsL21–25

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

  1. L21
    intro j
  2. L22
    intro x
  3. L23
    intro hi
  4. L24
    intro hmap
  5. L25
    intro hsource
04Establish hjdataL26–29

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

  1. L26
    have hjdata : ∃ y. BetaAt(rb,rc,i,y) ∧ Lt(y,h)Definitions: BetaAt(rb,rc,i,y)Lt(y,h)Original native command in the exact edition
  2. L27
    specialize hbounded i
  3. L28
    apply hbounded
  4. L29
    exact hi
05Separate the logical casesL30–31

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

  1. L30
    cases hjdata
  2. L31
    cases hjdata_witness
06Establish hjyL32–40

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

  1. L32
    have hjy : j = x1
  2. L33
    specialize beta_at_unique rb
  3. L34
    specialize beta_at_unique rc
  4. L35
    specialize beta_at_unique i
  5. L36
    specialize beta_at_unique j
  6. L37
    specialize beta_at_unique x1
  7. L38
    apply beta_at_unique
  8. L39
    exact hmap
  9. L40
    exact hjdata_witness_left
07Establish hjL41–43

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

  1. L41
  2. L42
    rewrite hjy
  3. L43
    exact hjdata_witness_right
08Establish hmagnitudeL44–53

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

  1. L44
    have hmagnitude : BetaAt(mb,mc,i,S j)Definitions: BetaAt(mb,mc,i,S j)Original native command in the exact edition
  2. L45
    specialize beta_magnitude_predecessor_recode_reflect mb
  3. L46
    specialize beta_magnitude_predecessor_recode_reflect mc
  4. L47
    specialize beta_magnitude_predecessor_recode_reflect rb
  5. L48
    specialize beta_magnitude_predecessor_recode_reflect rc
  6. L49
    specialize beta_magnitude_predecessor_recode_reflect h
  7. L50
    specialize beta_magnitude_predecessor_recode_reflect h
  8. L51
    specialize beta_magnitude_predecessor_recode_reflect i
  9. L52
    specialize beta_magnitude_predecessor_recode_reflect j
  10. L53
    apply beta_magnitude_predecessor_recode_reflect
09Use earlier factsL54–57

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

  1. L54
    exact hrange
  2. L55
    exact hrecode
  3. L56
    exact hi
  4. L57
    exact hmap
10Establish hxrawL58–67

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

  1. L58
    have hxraw : x = 1 + j
  2. L59
    specialize beta_range_entry_eq b
  3. L60
    specialize beta_range_entry_eq c
  4. L61
    specialize beta_range_entry_eq 1
  5. L62
    specialize beta_range_entry_eq h
  6. L63
    specialize beta_range_entry_eq j
  7. L64
    specialize beta_range_entry_eq x
  8. L65
    apply beta_range_entry_eq
  9. L66
    exact hhalf
  10. L67
    exact hj
11Use earlier factsL68–68

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

  1. L68
    exact hsource
12Establish honeL69–76

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

  1. L69
    have hone : 1 + j = S j
  2. L70
    trans S (0 + j)
  3. L71
    specialize add_succ_left 0
  4. L72
    specialize add_succ_left j
  5. L73
    exact add_succ_left
  6. L74
    congr
  7. L75
    specialize zero_add j
  8. L76
    exact zero_add
13Establish hxsuccL77–83

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

  1. L77
    have hxsucc : x = S j
  2. L78
    trans 1 + j
  3. L79
    exact hxraw
  4. L80
    exact hone
  5. L81
    rewrite hxsucc
  6. L82
    rewrite hxsucc
  7. L83
    exact hmagnitude

Library-wide reading audit

Original defined command ledger · 83 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro b
  6. 0006intro c
  7. 0007intro h
  8. 0008intro hrange
  9. 0009intro hrecode
  10. 0010intro hhalf
  11. 0011have hbounded : BoundedPrefix(rb,rc,h)
    Exact native replay linehave hbounded : forall fp_i_product_predecessor_bounded. (exists fp_gap_product_predecessor_bounded_index. fp_gap_product_predecessor_bounded_index + S fp_i_product_predecessor_bounded = h) -> exists fp_value_product_predecessor_bounded. ((((exists ff_h_product_predecessor_bounded_entry. ff_h_product_predecessor_bounded_entry + S (fp_value_product_predecessor_bounded) = S ((S (fp_i_product_predecessor_bounded)) * rc)) /\ exists ff_q_product_predecessor_bounded_entry. rb = ff_q_product_predecessor_bounded_entry * S ((S (fp_i_product_predecessor_bounded)) * rc) + (fp_value_product_predecessor_bounded))) /\ (exists fp_gap_product_predecessor_bounded_value. fp_gap_product_predecessor_bounded_value + S fp_value_product_predecessor_bounded = h))
  12. 0012specialize beta_magnitude_predecessor_recode_bounded mb
  13. 0013specialize beta_magnitude_predecessor_recode_bounded mc
  14. 0014specialize beta_magnitude_predecessor_recode_bounded rb
  15. 0015specialize beta_magnitude_predecessor_recode_bounded rc
  16. 0016specialize beta_magnitude_predecessor_recode_bounded h
  17. 0017apply beta_magnitude_predecessor_recode_bounded
  18. 0018exact hrange
  19. 0019exact hrecode
  20. 0020intro i
  21. 0021intro j
  22. 0022intro x
  23. 0023intro hi
  24. 0024intro hmap
  25. 0025intro hsource
  26. 0026have hjdata : ∃ y. BetaAt(rb,rc,i,y) ∧ Lt(y,h)
    Exact native replay linehave hjdata : exists y. ((((exists ff_h_product_alignment_bounded_entry. ff_h_product_alignment_bounded_entry + S (y) = S ((S (i)) * rc)) /\ exists ff_q_product_alignment_bounded_entry. rb = ff_q_product_alignment_bounded_entry * S ((S (i)) * rc) + (y))) /\ (exists gsp_lt_gap_product_alignment_bounded_value. gsp_lt_gap_product_alignment_bounded_value + S y = h))
  27. 0027specialize hbounded i
  28. 0028apply hbounded
  29. 0029exact hi
  30. 0030cases hjdata
  31. 0031cases hjdata_witness
  32. 0032have hjy : j = x1
  33. 0033specialize beta_at_unique rb
  34. 0034specialize beta_at_unique rc
  35. 0035specialize beta_at_unique i
  36. 0036specialize beta_at_unique j
  37. 0037specialize beta_at_unique x1
  38. 0038apply beta_at_unique
  39. 0039exact hmap
  40. 0040exact hjdata_witness_left
  41. 0041have hj : Lt(j,h)
    Exact native replay linehave hj : exists gsp_lt_gap_product_alignment_j_bound. gsp_lt_gap_product_alignment_j_bound + S j = h
  42. 0042rewrite hjy
  43. 0043exact hjdata_witness_right
  44. 0044have hmagnitude : BetaAt(mb,mc,i,S j)
    Exact native replay linehave hmagnitude : ((exists gsp_beta_height_product_alignment_magnitude_successor. gsp_beta_height_product_alignment_magnitude_successor + S (S j) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_product_alignment_magnitude_successor. mb = gsp_beta_quotient_product_alignment_magnitude_successor * S ((S (i)) * mc) + (S j))
  45. 0045specialize beta_magnitude_predecessor_recode_reflect mb
  46. 0046specialize beta_magnitude_predecessor_recode_reflect mc
  47. 0047specialize beta_magnitude_predecessor_recode_reflect rb
  48. 0048specialize beta_magnitude_predecessor_recode_reflect rc
  49. 0049specialize beta_magnitude_predecessor_recode_reflect h
  50. 0050specialize beta_magnitude_predecessor_recode_reflect h
  51. 0051specialize beta_magnitude_predecessor_recode_reflect i
  52. 0052specialize beta_magnitude_predecessor_recode_reflect j
  53. 0053apply beta_magnitude_predecessor_recode_reflect
  54. 0054exact hrange
  55. 0055exact hrecode
  56. 0056exact hi
  57. 0057exact hmap
  58. 0058have hxraw : x = 1 + j
  59. 0059specialize beta_range_entry_eq b
  60. 0060specialize beta_range_entry_eq c
  61. 0061specialize beta_range_entry_eq 1
  62. 0062specialize beta_range_entry_eq h
  63. 0063specialize beta_range_entry_eq j
  64. 0064specialize beta_range_entry_eq x
  65. 0065apply beta_range_entry_eq
  66. 0066exact hhalf
  67. 0067exact hj
  68. 0068exact hsource
  69. 0069have hone : 1 + j = S j
  70. 0070trans S (0 + j)
  71. 0071specialize add_succ_left 0
  72. 0072specialize add_succ_left j
  73. 0073exact add_succ_left
  74. 0074congr
  75. 0075specialize zero_add j
  76. 0076exact zero_add
  77. 0077have hxsucc : x = S j
  78. 0078trans 1 + j
  79. 0079exact hxraw
  80. 0080exact hone
  81. 0081rewrite hxsucc
  82. 0082rewrite hxsucc
  83. 0083exact hmagnitude