PA00BY · theorem

beta_division_prefix_exists

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

Every finite beta source prefix has beta-coded quotients and bounded remainders for a nonzero modulus.

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. ∀ b. ∀ c. ∀ l. ¬p = 0 → ∃ x. ∃ y. ∃ z. ∃ n. DivisionPrefix(p,b,c,x,y,z,n,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

PD0040 DivisionPrefix

1 occurrences

In local proof propositions

PD0007 DivRem PD0013 BetaAt PD0040 DivisionPrefix

6 occurrences

Exact expanded native-PA statement
forall p b c l. ~(p = 0) -> exists qb qc rb rc. (forall fdp_index_exists_result. (exists gsp_lt_gap_exists_result_index_bound. gsp_lt_gap_exists_result_index_bound + S fdp_index_exists_result = l) -> exists fdp_value_exists_result fdp_quotient_exists_result fdp_remainder_exists_result. (((exists ff_h_fdp_exists_result_source. ff_h_fdp_exists_result_source + S (fdp_value_exists_result) = S ((S (fdp_index_exists_result)) * c)) /\ exists ff_q_fdp_exists_result_source. b = ff_q_fdp_exists_result_source * S ((S (fdp_index_exists_result)) * c) + (fdp_value_exists_result))) /\ ((((exists ff_h_fdp_exists_result_quotient_entry. ff_h_fdp_exists_result_quotient_entry + S (fdp_quotient_exists_result) = S ((S (fdp_index_exists_result)) * qc)) /\ exists ff_q_fdp_exists_result_quotient_entry. qb = ff_q_fdp_exists_result_quotient_entry * S ((S (fdp_index_exists_result)) * qc) + (fdp_quotient_exists_result))) /\ ((((exists ff_h_fdp_exists_result_remainder_entry. ff_h_fdp_exists_result_remainder_entry + S (fdp_remainder_exists_result) = S ((S (fdp_index_exists_result)) * rc)) /\ exists ff_q_fdp_exists_result_remainder_entry. rb = ff_q_fdp_exists_result_remainder_entry * S ((S (fdp_index_exists_result)) * rc) + (fdp_remainder_exists_result))) /\ (fdp_value_exists_result = p * fdp_quotient_exists_result + fdp_remainder_exists_result /\ (exists gsp_lt_gap_exists_result_remainder_bound. gsp_lt_gap_exists_result_remainder_bound + S fdp_remainder_exists_result = p)))))

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0029 beta_at_exists PA001D division_remainder_exists PA00BX beta_division_prefix_extend

Direct theorem dependents

PA00C0 prime_scaled_half_division_prefix_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

62 script commands · 18 reading checkpoints · 6 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 (5)
add eq zero rightsucc ne zerobeta at existsdivision remainder existsbeta division prefix extend
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
02Induction on lL4–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
  2. L5
    intro hp0
03Construct an explicit witnessL6–9

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

  1. L6
    exists 0
  2. L7
    exists 0
  3. L8
    exists 0
  4. L9
    exists 0
04Fix variables and assumptionsL10–11

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

  1. L10
    intro i
  2. L11
    intro hi
05Separate the logical casesL12–13

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

  1. L12
    exfalso
  2. L13
    cases hi
06Establish hsiL14–22

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

  1. L14
    have hsi : S i = 0
  2. L15
    specialize add_eq_zero_right x
  3. L16
    specialize add_eq_zero_right (S i)
  4. L17
    apply add_eq_zero_right
  5. L18
    exact hi_witness
  6. L19
    specialize succ_ne_zero i
  7. L20
    apply succ_ne_zero
  8. L21
    exact hsi
  9. L22
    intro hp0
07Establish hpreviousL23–25

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

  1. L23
    have hprevious : ∃ qb. ∃ qc. ∃ rb. ∃ rc. DivisionPrefix(p,b,c,qb,qc,rb,rc,l)Definitions: DivisionPrefix(p,b,c,qb,qc,rb,rc,l)Original native command in the exact edition
  2. L24
    apply IH
  3. L25
    exact hp0
08Separate the logical casesL26–29

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

  1. L26
    cases hprevious
  2. L27
    cases hprevious_witness
  3. L28
    cases hprevious_witness_witness
  4. L29
    cases hprevious_witness_witness_witness
09Establish hdecodedL30–34

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

  1. L30
    have hdecoded : ∃ x. BetaAt(b,c,l,x)Definitions: BetaAt(b,c,l,x)Original native command in the exact edition
  2. L31
    specialize beta_at_exists b
  3. L32
    specialize beta_at_exists c
  4. L33
    specialize beta_at_exists l
  5. L34
    exact beta_at_exists
10Separate the logical casesL35–35

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

  1. L35
    cases hdecoded
11Establish hdivisionL36–40

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

  1. L36
    have hdivision : ∃ q. ∃ r. DivRem(x4,p,q,r)Definitions: DivRem(x4,p,q,r)Original native command in the exact edition
  2. L37
    specialize division_remainder_exists p
  3. L38
    specialize division_remainder_exists x4
  4. L39
    apply division_remainder_exists
  5. L40
    exact hp0
12Separate the logical casesL41–42

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

  1. L41
    cases hdivision
  2. L42
    cases hdivision_witness
13Establish hchoiceL43–43

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

  1. L43
    have hchoice : ∃ x. ∃ q. ∃ r. BetaAt(b,c,l,x) ∧ DivRem(x,p,q,r)Definitions: BetaAt(b,c,l,x)DivRem(x,p,q,r)Original native command in the exact edition
14Construct an explicit witnessL44–46

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

  1. L44
    exists x4
  2. L45
    exists x5
  3. L46
    exists x6
15Separate the logical casesL47–47

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

  1. L47
    split
16Use earlier factsL48–49

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

  1. L48
    exact hdecoded_witness
  2. L49
    exact hdivision_witness_witness
17Establish hnextL50–59

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

  1. L50
    have hnext : ∃ qb. ∃ qc. ∃ rb. ∃ rc. DivisionPrefix(p,b,c,qb,qc,rb,rc,S l)Definitions: DivisionPrefix(p,b,c,qb,qc,rb,rc,S l)Original native command in the exact edition
  2. L51
    specialize beta_division_prefix_extend p
  3. L52
    specialize beta_division_prefix_extend b
  4. L53
    specialize beta_division_prefix_extend c
  5. L54
    specialize beta_division_prefix_extend x
  6. L55
    specialize beta_division_prefix_extend x1
  7. L56
    specialize beta_division_prefix_extend x2
  8. L57
    specialize beta_division_prefix_extend x3
  9. L58
    specialize beta_division_prefix_extend l
  10. L59
    apply beta_division_prefix_extend
18Use earlier factsL60–62

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

  1. L60
    exact hprevious_witness_witness_witness_witness
  2. L61
    exact hchoice
  3. L62
    exact hnext

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004induction l
  5. 0005intro hp0
  6. 0006exists 0
  7. 0007exists 0
  8. 0008exists 0
  9. 0009exists 0
  10. 0010intro i
  11. 0011intro hi
  12. 0012exfalso
  13. 0013cases hi
  14. 0014have hsi : S i = 0
  15. 0015specialize add_eq_zero_right x
  16. 0016specialize add_eq_zero_right (S i)
  17. 0017apply add_eq_zero_right
  18. 0018exact hi_witness
  19. 0019specialize succ_ne_zero i
  20. 0020apply succ_ne_zero
  21. 0021exact hsi
  22. 0022intro hp0
  23. 0023have hprevious : ∃ qb. ∃ qc. ∃ rb. ∃ rc. DivisionPrefix(p,b,c,qb,qc,rb,rc,l)
    Exact native replay linehave hprevious : exists qb qc rb rc. (forall fdp_index_exists_previous. (exists gsp_lt_gap_exists_previous_index_bound. gsp_lt_gap_exists_previous_index_bound + S fdp_index_exists_previous = l) -> exists fdp_value_exists_previous fdp_quotient_exists_previous fdp_remainder_exists_previous. (((exists ff_h_fdp_exists_previous_source. ff_h_fdp_exists_previous_source + S (fdp_value_exists_previous) = S ((S (fdp_index_exists_previous)) * c)) /\ exists ff_q_fdp_exists_previous_source. b = ff_q_fdp_exists_previous_source * S ((S (fdp_index_exists_previous)) * c) + (fdp_value_exists_previous))) /\ ((((exists ff_h_fdp_exists_previous_quotient_entry. ff_h_fdp_exists_previous_quotient_entry + S (fdp_quotient_exists_previous) = S ((S (fdp_index_exists_previous)) * qc)) /\ exists ff_q_fdp_exists_previous_quotient_entry. qb = ff_q_fdp_exists_previous_quotient_entry * S ((S (fdp_index_exists_previous)) * qc) + (fdp_quotient_exists_previous))) /\ ((((exists ff_h_fdp_exists_previous_remainder_entry. ff_h_fdp_exists_previous_remainder_entry + S (fdp_remainder_exists_previous) = S ((S (fdp_index_exists_previous)) * rc)) /\ exists ff_q_fdp_exists_previous_remainder_entry. rb = ff_q_fdp_exists_previous_remainder_entry * S ((S (fdp_index_exists_previous)) * rc) + (fdp_remainder_exists_previous))) /\ (fdp_value_exists_previous = p * fdp_quotient_exists_previous + fdp_remainder_exists_previous /\ (exists gsp_lt_gap_exists_previous_remainder_bound. gsp_lt_gap_exists_previous_remainder_bound + S fdp_remainder_exists_previous = p)))))
  24. 0024apply IH
  25. 0025exact hp0
  26. 0026cases hprevious
  27. 0027cases hprevious_witness
  28. 0028cases hprevious_witness_witness
  29. 0029cases hprevious_witness_witness_witness
  30. 0030have hdecoded : ∃ x. BetaAt(b,c,l,x)
    Exact native replay linehave hdecoded : exists x. (((exists ff_h_fdp_exists_last_source. ff_h_fdp_exists_last_source + S (x) = S ((S (l)) * c)) /\ exists ff_q_fdp_exists_last_source. b = ff_q_fdp_exists_last_source * S ((S (l)) * c) + (x)))
  31. 0031specialize beta_at_exists b
  32. 0032specialize beta_at_exists c
  33. 0033specialize beta_at_exists l
  34. 0034exact beta_at_exists
  35. 0035cases hdecoded
  36. 0036have hdivision : ∃ q. ∃ r. DivRem(x4,p,q,r)
    Exact native replay linehave hdivision : exists q r. x4 = p * q + r /\ (exists gsp_lt_gap_fdp_exists_last_remainder_bound. gsp_lt_gap_fdp_exists_last_remainder_bound + S r = p)
  37. 0037specialize division_remainder_exists p
  38. 0038specialize division_remainder_exists x4
  39. 0039apply division_remainder_exists
  40. 0040exact hp0
  41. 0041cases hdivision
  42. 0042cases hdivision_witness
  43. 0043have hchoice : ∃ x. ∃ q. ∃ r. BetaAt(b,c,l,x) ∧ DivRem(x,p,q,r)
    Exact native replay linehave hchoice : exists x q r. (((exists ff_h_fdp_choice_source. ff_h_fdp_choice_source + S (x) = S ((S (l)) * c)) /\ exists ff_q_fdp_choice_source. b = ff_q_fdp_choice_source * S ((S (l)) * c) + (x))) /\ (x = p * q + r /\ (exists gsp_lt_gap_fdp_choice_remainder_bound. gsp_lt_gap_fdp_choice_remainder_bound + S r = p))
  44. 0044exists x4
  45. 0045exists x5
  46. 0046exists x6
  47. 0047split
  48. 0048exact hdecoded_witness
  49. 0049exact hdivision_witness_witness
  50. 0050have hnext : ∃ qb. ∃ qc. ∃ rb. ∃ rc. DivisionPrefix(p,b,c,qb,qc,rb,rc,S l)
    Exact native replay linehave hnext : exists qb qc rb rc. (forall fdp_index_exists_next. (exists gsp_lt_gap_exists_next_index_bound. gsp_lt_gap_exists_next_index_bound + S fdp_index_exists_next = S l) -> exists fdp_value_exists_next fdp_quotient_exists_next fdp_remainder_exists_next. (((exists ff_h_fdp_exists_next_source. ff_h_fdp_exists_next_source + S (fdp_value_exists_next) = S ((S (fdp_index_exists_next)) * c)) /\ exists ff_q_fdp_exists_next_source. b = ff_q_fdp_exists_next_source * S ((S (fdp_index_exists_next)) * c) + (fdp_value_exists_next))) /\ ((((exists ff_h_fdp_exists_next_quotient_entry. ff_h_fdp_exists_next_quotient_entry + S (fdp_quotient_exists_next) = S ((S (fdp_index_exists_next)) * qc)) /\ exists ff_q_fdp_exists_next_quotient_entry. qb = ff_q_fdp_exists_next_quotient_entry * S ((S (fdp_index_exists_next)) * qc) + (fdp_quotient_exists_next))) /\ ((((exists ff_h_fdp_exists_next_remainder_entry. ff_h_fdp_exists_next_remainder_entry + S (fdp_remainder_exists_next) = S ((S (fdp_index_exists_next)) * rc)) /\ exists ff_q_fdp_exists_next_remainder_entry. rb = ff_q_fdp_exists_next_remainder_entry * S ((S (fdp_index_exists_next)) * rc) + (fdp_remainder_exists_next))) /\ (fdp_value_exists_next = p * fdp_quotient_exists_next + fdp_remainder_exists_next /\ (exists gsp_lt_gap_exists_next_remainder_bound. gsp_lt_gap_exists_next_remainder_bound + S fdp_remainder_exists_next = p)))))
  51. 0051specialize beta_division_prefix_extend p
  52. 0052specialize beta_division_prefix_extend b
  53. 0053specialize beta_division_prefix_extend c
  54. 0054specialize beta_division_prefix_extend x
  55. 0055specialize beta_division_prefix_extend x1
  56. 0056specialize beta_division_prefix_extend x2
  57. 0057specialize beta_division_prefix_extend x3
  58. 0058specialize beta_division_prefix_extend l
  59. 0059apply beta_division_prefix_extend
  60. 0060exact hprevious_witness_witness_witness_witness
  61. 0061exact hchoice
  62. 0062exact hnext