PA008G · theorem

beta_successor_range_reindex_aligned

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

A bounded residue map aligns the range 1,...,n with its successor lift.

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

∀ r. ∀ s. ∀ b. ∀ c. ∀ z. ∀ d. ∀ n. BoundedPrefix(r,s,n) → Range(b,c,1,n) → (∀ x. ∀ y. Lt(x,n) → BetaAt(r,s,x,y) → BetaAt(z,d,x,S y)) → ∀ x. ∀ y. ∀ m. Lt(x,n) → BetaAt(r,s,x,y) → BetaAt(b,c,y,m) → BetaAt(z,d,x,m)

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

9 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall r s b c z d n. (forall fp_i_aligned_bounded. (exists fp_gap_aligned_bounded_index. fp_gap_aligned_bounded_index + S fp_i_aligned_bounded = n) -> exists fp_value_aligned_bounded. ((((exists ff_h_aligned_bounded_entry. ff_h_aligned_bounded_entry + S (fp_value_aligned_bounded) = S ((S (fp_i_aligned_bounded)) * s)) /\ exists ff_q_aligned_bounded_entry. r = ff_q_aligned_bounded_entry * S ((S (fp_i_aligned_bounded)) * s) + (fp_value_aligned_bounded))) /\ (exists fp_gap_aligned_bounded_value. fp_gap_aligned_bounded_value + S fp_value_aligned_bounded = n))) -> (forall ff_i_frp_range_aligned_range. (exists ff_lt_frp_range_aligned_range_bound. ff_lt_frp_range_aligned_range_bound + S ff_i_frp_range_aligned_range = n) -> (((exists ff_h_frp_range_aligned_range_decoded. ff_h_frp_range_aligned_range_decoded + S (1 + ff_i_frp_range_aligned_range) = S ((S (ff_i_frp_range_aligned_range)) * c)) /\ exists ff_q_frp_range_aligned_range_decoded. b = ff_q_frp_range_aligned_range_decoded * S ((S (ff_i_frp_range_aligned_range)) * c) + (1 + ff_i_frp_range_aligned_range)))) -> (forall frr_index_aligned_lift frr_value_aligned_lift. (exists frr_gap_aligned_lift. frr_gap_aligned_lift + S frr_index_aligned_lift = n) -> (((exists ff_h_frr_aligned_lift_source. ff_h_frr_aligned_lift_source + S (frr_value_aligned_lift) = S ((S (frr_index_aligned_lift)) * s)) /\ exists ff_q_frr_aligned_lift_source. r = ff_q_frr_aligned_lift_source * S ((S (frr_index_aligned_lift)) * s) + (frr_value_aligned_lift))) -> (((exists frm_height_frr_aligned_lift_target. frm_height_frr_aligned_lift_target + S (S frr_value_aligned_lift) = S ((S (frr_index_aligned_lift)) * d)) /\ exists frm_quotient_frr_aligned_lift_target. z = frm_quotient_frr_aligned_lift_target * S ((S (frr_index_aligned_lift)) * d) + (S frr_value_aligned_lift)))) -> (forall fpr_i_aligned_result fpr_j_aligned_result fpr_x_aligned_result. (exists fpr_h_aligned_result. fpr_h_aligned_result + S fpr_i_aligned_result = n) -> (((exists ff_h_aligned_result_map. ff_h_aligned_result_map + S (fpr_j_aligned_result) = S ((S (fpr_i_aligned_result)) * s)) /\ exists ff_q_aligned_result_map. r = ff_q_aligned_result_map * S ((S (fpr_i_aligned_result)) * s) + (fpr_j_aligned_result))) -> (((exists ff_h_aligned_result_source. ff_h_aligned_result_source + S (fpr_x_aligned_result) = S ((S (fpr_j_aligned_result)) * c)) /\ exists ff_q_aligned_result_source. b = ff_q_aligned_result_source * S ((S (fpr_j_aligned_result)) * c) + (fpr_x_aligned_result))) -> (((exists ff_h_aligned_result_target. ff_h_aligned_result_target + S (fpr_x_aligned_result) = S ((S (fpr_i_aligned_result)) * d)) /\ exists ff_q_aligned_result_target. z = ff_q_aligned_result_target * S ((S (fpr_i_aligned_result)) * d) + (fpr_x_aligned_result))))

Proof neighborhood

Direct theorem prerequisites

PA002F beta_at_unique PA008F beta_range_one_entry_eq_succ

Direct theorem dependents

PA008I prime_mul_residue_reindex_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

53 script commands · 8 reading checkpoints · 5 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 (2)
beta at uniquebeta range one entry eq succ
01Fix variables and assumptionsL1–10

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro z
  6. L6
    intro d
  7. L7
    intro n
  8. L8
    intro hbounded
  9. L9
    intro hrange
  10. L10
    intro hlift
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 value
  4. L14
    intro hi
  5. L15
    intro hmap
  6. L16
    intro hsource
03Establish hbounded_iL17–20

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

  1. L17
    have hbounded_i : ∃ frr_value_aligned_entry. BetaAt(r,s,i,frr_value_aligned_entry) ∧ Lt(frr_value_aligned_entry,n)Definitions: BetaAt(r,s,i,frr_value_aligned_entry)Lt(frr_value_aligned_entry,n)Original native command in the exact edition
  2. L18
    specialize hbounded i
  3. L19
    apply hbounded
  4. L20
    exact hi
04Separate the logical casesL21–22

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

  1. L21
    cases hbounded_i
  2. L22
    cases hbounded_i_witness
05Establish hjxL23–31

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

  1. L23
    have hjx : j = x
  2. L24
    specialize beta_at_unique r
  3. L25
    specialize beta_at_unique s
  4. L26
    specialize beta_at_unique i
  5. L27
    specialize beta_at_unique j
  6. L28
    specialize beta_at_unique x
  7. L29
    apply beta_at_unique
  8. L30
    exact hmap
  9. L31
    exact hbounded_i_witness_left
06Establish hjboundL32–34

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

  1. L32
    have hjbound : Lt(j,n)Definitions: Lt(j,n)Original native command in the exact edition
  2. L33
    rewrite hjx
  3. L34
    exact hbounded_i_witness_right
07Establish hvalueL35–44

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

  1. L35
    have hvalue : value = S j
  2. L36
    specialize beta_range_one_entry_eq_succ b
  3. L37
    specialize beta_range_one_entry_eq_succ c
  4. L38
    specialize beta_range_one_entry_eq_succ n
  5. L39
    specialize beta_range_one_entry_eq_succ j
  6. L40
    specialize beta_range_one_entry_eq_succ value
  7. L41
    apply beta_range_one_entry_eq_succ
  8. L42
    exact hrange
  9. L43
    exact hjbound
  10. L44
    exact hsource
08Establish htarget_succL45–53

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

  1. L45
    have htarget_succ : BetaAt(z,d,i,S j)Definitions: BetaAt(z,d,i,S j)Original native command in the exact edition
  2. L46
    specialize hlift i
  3. L47
    specialize hlift j
  4. L48
    apply hlift
  5. L49
    exact hi
  6. L50
    exact hmap
  7. L51
    rewrite hvalue
  8. L52
    rewrite hvalue
  9. L53
    exact htarget_succ

Library-wide reading audit

Original defined command ledger · 53 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro n
  8. 0008intro hbounded
  9. 0009intro hrange
  10. 0010intro hlift
  11. 0011intro i
  12. 0012intro j
  13. 0013intro value
  14. 0014intro hi
  15. 0015intro hmap
  16. 0016intro hsource
  17. 0017have hbounded_i : ∃ frr_value_aligned_entry. BetaAt(r,s,i,frr_value_aligned_entry) ∧ Lt(frr_value_aligned_entry,n)
    Exact native replay linehave hbounded_i : exists frr_value_aligned_entry. (((exists ff_h_frr_aligned_entry_entry. ff_h_frr_aligned_entry_entry + S (frr_value_aligned_entry) = S ((S (i)) * s)) /\ exists ff_q_frr_aligned_entry_entry. r = ff_q_frr_aligned_entry_entry * S ((S (i)) * s) + (frr_value_aligned_entry))) /\ (exists frr_gap_aligned_entry. frr_gap_aligned_entry + S frr_value_aligned_entry = n)
  18. 0018specialize hbounded i
  19. 0019apply hbounded
  20. 0020exact hi
  21. 0021cases hbounded_i
  22. 0022cases hbounded_i_witness
  23. 0023have hjx : j = x
  24. 0024specialize beta_at_unique r
  25. 0025specialize beta_at_unique s
  26. 0026specialize beta_at_unique i
  27. 0027specialize beta_at_unique j
  28. 0028specialize beta_at_unique x
  29. 0029apply beta_at_unique
  30. 0030exact hmap
  31. 0031exact hbounded_i_witness_left
  32. 0032have hjbound : Lt(j,n)
    Exact native replay linehave hjbound : exists frr_gap_aligned_j_bound. frr_gap_aligned_j_bound + S j = n
  33. 0033rewrite hjx
  34. 0034exact hbounded_i_witness_right
  35. 0035have hvalue : value = S j
  36. 0036specialize beta_range_one_entry_eq_succ b
  37. 0037specialize beta_range_one_entry_eq_succ c
  38. 0038specialize beta_range_one_entry_eq_succ n
  39. 0039specialize beta_range_one_entry_eq_succ j
  40. 0040specialize beta_range_one_entry_eq_succ value
  41. 0041apply beta_range_one_entry_eq_succ
  42. 0042exact hrange
  43. 0043exact hjbound
  44. 0044exact hsource
  45. 0045have htarget_succ : BetaAt(z,d,i,S j)
    Exact native replay linehave htarget_succ : ((exists frm_height_aligned_target. frm_height_aligned_target + S (S j) = S ((S (i)) * d)) /\ exists frm_quotient_aligned_target. z = frm_quotient_aligned_target * S ((S (i)) * d) + (S j))
  46. 0046specialize hlift i
  47. 0047specialize hlift j
  48. 0048apply hlift
  49. 0049exact hi
  50. 0050exact hmap
  51. 0051rewrite hvalue
  52. 0052rewrite hvalue
  53. 0053exact htarget_succ