PA008H · theorem

beta_successor_range_scale_mod

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

The range and its successor-lifted residue map are pointwise congruent after scaling.

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

∀ p. ∀ n. ∀ a. ∀ r. ∀ s. ∀ b. ∀ c. ∀ z. ∀ d. (∀ x. Lt(x,n) → ∃ y. Lt(y,n) ∧ (BetaAt(r,s,x,y) ∧ ModEq(p,a · S x,S y))) → 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(b,c,x,y) → BetaAt(z,d,x,m) → ModEq(p,a · y,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 PD0008 ModEq PD0013 BetaAt PD0018 Range

12 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall p n a r s b c z d. (forall frm_index_scale_map. (exists frm_gap_scale_map_index_bound. frm_gap_scale_map_index_bound + S frm_index_scale_map = n) -> (exists frm_residue_scale_map_result. (exists frm_gap_scale_map_result_residue_bound. frm_gap_scale_map_result_residue_bound + S frm_residue_scale_map_result = n) /\ ((((exists ff_h_frm_scale_map_result_decoded. ff_h_frm_scale_map_result_decoded + S (frm_residue_scale_map_result) = S ((S (frm_index_scale_map)) * s)) /\ exists ff_q_frm_scale_map_result_decoded. r = ff_q_frm_scale_map_result_decoded * S ((S (frm_index_scale_map)) * s) + (frm_residue_scale_map_result))) /\ (exists frm_mod_left_scale_map_result_congruence frm_mod_right_scale_map_result_congruence. a * S frm_index_scale_map + p * frm_mod_left_scale_map_result_congruence = S frm_residue_scale_map_result + p * frm_mod_right_scale_map_result_congruence)))) -> (forall ff_i_frp_range_scale_range. (exists ff_lt_frp_range_scale_range_bound. ff_lt_frp_range_scale_range_bound + S ff_i_frp_range_scale_range = n) -> (((exists ff_h_frp_range_scale_range_decoded. ff_h_frp_range_scale_range_decoded + S (1 + ff_i_frp_range_scale_range) = S ((S (ff_i_frp_range_scale_range)) * c)) /\ exists ff_q_frp_range_scale_range_decoded. b = ff_q_frp_range_scale_range_decoded * S ((S (ff_i_frp_range_scale_range)) * c) + (1 + ff_i_frp_range_scale_range)))) -> (forall frr_index_scale_lift frr_value_scale_lift. (exists frr_gap_scale_lift. frr_gap_scale_lift + S frr_index_scale_lift = n) -> (((exists ff_h_frr_scale_lift_source. ff_h_frr_scale_lift_source + S (frr_value_scale_lift) = S ((S (frr_index_scale_lift)) * s)) /\ exists ff_q_frr_scale_lift_source. r = ff_q_frr_scale_lift_source * S ((S (frr_index_scale_lift)) * s) + (frr_value_scale_lift))) -> (((exists frm_height_frr_scale_lift_target. frm_height_frr_scale_lift_target + S (S frr_value_scale_lift) = S ((S (frr_index_scale_lift)) * d)) /\ exists frm_quotient_frr_scale_lift_target. z = frm_quotient_frr_scale_lift_target * S ((S (frr_index_scale_lift)) * d) + (S frr_value_scale_lift)))) -> (forall fsp_index_scale_result fsp_source_scale_result fsp_target_scale_result. (exists fsp_gap_scale_result. fsp_gap_scale_result + S fsp_index_scale_result = n) -> (((exists fsp_source_height_scale_result. fsp_source_height_scale_result + S (fsp_source_scale_result) = S ((S (fsp_index_scale_result)) * c)) /\ exists fsp_source_quotient_scale_result. b = fsp_source_quotient_scale_result * S ((S (fsp_index_scale_result)) * c) + (fsp_source_scale_result))) -> (((exists fsp_target_height_scale_result. fsp_target_height_scale_result + S (fsp_target_scale_result) = S ((S (fsp_index_scale_result)) * d)) /\ exists fsp_target_quotient_scale_result. z = fsp_target_quotient_scale_result * S ((S (fsp_index_scale_result)) * d) + (fsp_target_scale_result))) -> (exists fsp_mod_left_scale_result fsp_mod_right_scale_result. a * fsp_source_scale_result + p * fsp_mod_left_scale_result = fsp_target_scale_result + p * fsp_mod_right_scale_result))

Proof neighborhood

Direct theorem prerequisites

PA008F beta_range_one_entry_eq_succ PA002F beta_at_unique

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 · 9 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 (2)
beta range one entry eq succbeta at unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro a
  4. L4
    intro r
  5. L5
    intro s
  6. L6
    intro b
  7. L7
    intro c
  8. L8
    intro z
  9. L9
    intro d
  10. L10
    intro hmap
02Fix variables and assumptionsL11–18

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

  1. L11
    intro hrange
  2. L12
    intro hlift
  3. L13
    intro i
  4. L14
    intro source
  5. L15
    intro target
  6. L16
    intro hi
  7. L17
    intro hsource
  8. L18
    intro htarget
03Establish hmiL19–22

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

  1. L19
    have hmi : ∃ frm_residue_scale_at_i. Lt(frm_residue_scale_at_i,n) ∧ (BetaAt(r,s,i,frm_residue_scale_at_i) ∧ ModEq(p,a · S i,S frm_residue_scale_at_i))Definitions: Lt(frm_residue_scale_at_i,n)BetaAt(r,s,i,frm_residue_scale_at_i)ModEq(p,a · S i,S frm_residue_scale_at_i)Original native command in the exact edition
  2. L20
    specialize hmap i
  3. L21
    apply hmap
  4. L22
    exact hi
04Separate the logical casesL23–25

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

  1. L23
    cases hmi
  2. L24
    cases hmi_witness
  3. L25
    cases hmi_witness_right
05Establish hsource_valueL26–35

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. L26
    have hsource_value : source = S i
  2. L27
    specialize beta_range_one_entry_eq_succ b
  3. L28
    specialize beta_range_one_entry_eq_succ c
  4. L29
    specialize beta_range_one_entry_eq_succ n
  5. L30
    specialize beta_range_one_entry_eq_succ i
  6. L31
    specialize beta_range_one_entry_eq_succ source
  7. L32
    apply beta_range_one_entry_eq_succ
  8. L33
    exact hrange
  9. L34
    exact hi
  10. L35
    exact hsource
06Establish htarget_succL36–41

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

  1. L36
    have htarget_succ : BetaAt(z,d,i,S x)Definitions: BetaAt(z,d,i,S x)Original native command in the exact edition
  2. L37
    specialize hlift i
  3. L38
    specialize hlift x
  4. L39
    apply hlift
  5. L40
    exact hi
  6. L41
    exact hmi_witness_right_left
07Establish htarget_valueL42–51

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

  1. L42
    have htarget_value : target = S x
  2. L43
    specialize beta_at_unique z
  3. L44
    specialize beta_at_unique d
  4. L45
    specialize beta_at_unique i
  5. L46
    specialize beta_at_unique target
  6. L47
    specialize beta_at_unique (S x)
  7. L48
    apply beta_at_unique
  8. L49
    exact htarget
  9. L50
    exact htarget_succ
  10. L51
    rewrite hsource_value
08Calculate and transport equalitiesL52–52

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

  1. L52
    rewrite htarget_value
09Use earlier factsL53–53

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

  1. L53
    exact hmi_witness_right_right

Library-wide reading audit

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