PA007L · theorem

beta_pointwise_mul_prefix_exists

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

Two beta prefixes admit a third beta prefix of their pointwise products.

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. ∀ sb. ∀ sc. ∀ l. ∃ tb. ∃ tc. ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → BetaAt(mb,mc,x,y) → BetaAt(sb,sc,x,z) → BetaAt(tb,tc,x,n) → n = y · 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

PD0002 Lt PD0013 BetaAt

4 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

6 occurrences

Exact expanded native-PA statement
forall mb mc sb sc l. exists tb tc. (forall fpmp_index_recode_exists_result fpmp_left_recode_exists_result fpmp_right_recode_exists_result fpmp_target_recode_exists_result. (exists fpmp_gap_recode_exists_result. fpmp_gap_recode_exists_result + S fpmp_index_recode_exists_result = l) -> (((exists ff_h_fpmp_recode_exists_result_left. ff_h_fpmp_recode_exists_result_left + S (fpmp_left_recode_exists_result) = S ((S (fpmp_index_recode_exists_result)) * mc)) /\ exists ff_q_fpmp_recode_exists_result_left. mb = ff_q_fpmp_recode_exists_result_left * S ((S (fpmp_index_recode_exists_result)) * mc) + (fpmp_left_recode_exists_result))) -> (((exists ff_h_fpmp_recode_exists_result_right. ff_h_fpmp_recode_exists_result_right + S (fpmp_right_recode_exists_result) = S ((S (fpmp_index_recode_exists_result)) * sc)) /\ exists ff_q_fpmp_recode_exists_result_right. sb = ff_q_fpmp_recode_exists_result_right * S ((S (fpmp_index_recode_exists_result)) * sc) + (fpmp_right_recode_exists_result))) -> (((exists ff_h_fpmp_recode_exists_result_target. ff_h_fpmp_recode_exists_result_target + S (fpmp_target_recode_exists_result) = S ((S (fpmp_index_recode_exists_result)) * tc)) /\ exists ff_q_fpmp_recode_exists_result_target. tb = ff_q_fpmp_recode_exists_result_target * S ((S (fpmp_index_recode_exists_result)) * tc) + (fpmp_target_recode_exists_result))) -> fpmp_target_recode_exists_result = fpmp_left_recode_exists_result * fpmp_right_recode_exists_result)

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0029 beta_at_exists PA007K beta_pointwise_mul_prefix_extend

Direct theorem dependents

PA007O beta_pointwise_mul_product_exists 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

54 script commands · 14 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 (4)
add eq zero rightsucc ne zerobeta at existsbeta pointwise mul prefix extend
01Fix variables and assumptionsL1–4

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

  1. L1
    intro mb
  2. L2
    intro mc
  3. L3
    intro sb
  4. L4
    intro sc
02Induction on lL5–5

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

  1. L5
    induction l
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–15

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

  1. L8
    intro i
  2. L9
    intro a
  3. L10
    intro b
  4. L11
    intro t
  5. L12
    intro hi
  6. L13
    intro ha
  7. L14
    intro hb
  8. L15
    intro ht
05Separate the logical casesL16–17

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

  1. L16
    exfalso
  2. L17
    cases hi
06Establish hsiL18–25

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

  1. L18
    have hsi : S i = 0
  2. L19
    specialize add_eq_zero_right x
  3. L20
    specialize add_eq_zero_right (S i)
  4. L21
    apply add_eq_zero_right
  5. L22
    exact hi_witness
  6. L23
    specialize succ_ne_zero i
  7. L24
    apply succ_ne_zero
  8. L25
    exact hsi
07Establish hpreviousL26–27

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

  1. L26
    have hprevious : ∃ tb. ∃ tc. ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → BetaAt(mb,mc,x,y) → BetaAt(sb,sc,x,z) → BetaAt(tb,tc,x,n) → n = y · zDefinitions: Lt(x,l)BetaAt(mb,mc,x,y)BetaAt(sb,sc,x,z)BetaAt(tb,tc,x,n)Original native command in the exact edition
  2. L27
    exact IH
08Separate the logical casesL28–29

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

  1. L28
    cases hprevious
  2. L29
    cases hprevious_witness
09Establish hleftL30–34

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

  1. L30
    have hleft : ∃ m. BetaAt(mb,mc,l,m)Definitions: BetaAt(mb,mc,l,m)Original native command in the exact edition
  2. L31
    specialize beta_at_exists mb
  3. L32
    specialize beta_at_exists mc
  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 hleft
11Establish hrightL36–40

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

  1. L36
    have hright : ∃ s. BetaAt(sb,sc,l,s)Definitions: BetaAt(sb,sc,l,s)Original native command in the exact edition
  2. L37
    specialize beta_at_exists sb
  3. L38
    specialize beta_at_exists sc
  4. L39
    specialize beta_at_exists l
  5. L40
    exact beta_at_exists
12Separate the logical casesL41–41

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

  1. L41
    cases hright
13Use earlier factsL42–51

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

  1. L42
    specialize beta_pointwise_mul_prefix_extend mb
  2. L43
    specialize beta_pointwise_mul_prefix_extend mc
  3. L44
    specialize beta_pointwise_mul_prefix_extend sb
  4. L45
    specialize beta_pointwise_mul_prefix_extend sc
  5. L46
    specialize beta_pointwise_mul_prefix_extend x
  6. L47
    specialize beta_pointwise_mul_prefix_extend x1
  7. L48
    specialize beta_pointwise_mul_prefix_extend l
  8. L49
    specialize beta_pointwise_mul_prefix_extend x2
  9. L50
    specialize beta_pointwise_mul_prefix_extend x3
  10. L51
    apply beta_pointwise_mul_prefix_extend
14Use earlier factsL52–54

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

  1. L52
    exact hprevious_witness_witness
  2. L53
    exact hleft_witness
  3. L54
    exact hright_witness

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005induction l
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro a
  10. 0010intro b
  11. 0011intro t
  12. 0012intro hi
  13. 0013intro ha
  14. 0014intro hb
  15. 0015intro ht
  16. 0016exfalso
  17. 0017cases hi
  18. 0018have hsi : S i = 0
  19. 0019specialize add_eq_zero_right x
  20. 0020specialize add_eq_zero_right (S i)
  21. 0021apply add_eq_zero_right
  22. 0022exact hi_witness
  23. 0023specialize succ_ne_zero i
  24. 0024apply succ_ne_zero
  25. 0025exact hsi
  26. 0026have hprevious : ∃ tb. ∃ tc. ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → BetaAt(mb,mc,x,y) → BetaAt(sb,sc,x,z) → BetaAt(tb,tc,x,n) → n = y · z
    Exact native replay linehave hprevious : exists tb tc. (forall fpmp_index_recode_exists_previous fpmp_left_recode_exists_previous fpmp_right_recode_exists_previous fpmp_target_recode_exists_previous. (exists fpmp_gap_recode_exists_previous. fpmp_gap_recode_exists_previous + S fpmp_index_recode_exists_previous = l) -> (((exists ff_h_fpmp_recode_exists_previous_left. ff_h_fpmp_recode_exists_previous_left + S (fpmp_left_recode_exists_previous) = S ((S (fpmp_index_recode_exists_previous)) * mc)) /\ exists ff_q_fpmp_recode_exists_previous_left. mb = ff_q_fpmp_recode_exists_previous_left * S ((S (fpmp_index_recode_exists_previous)) * mc) + (fpmp_left_recode_exists_previous))) -> (((exists ff_h_fpmp_recode_exists_previous_right. ff_h_fpmp_recode_exists_previous_right + S (fpmp_right_recode_exists_previous) = S ((S (fpmp_index_recode_exists_previous)) * sc)) /\ exists ff_q_fpmp_recode_exists_previous_right. sb = ff_q_fpmp_recode_exists_previous_right * S ((S (fpmp_index_recode_exists_previous)) * sc) + (fpmp_right_recode_exists_previous))) -> (((exists ff_h_fpmp_recode_exists_previous_target. ff_h_fpmp_recode_exists_previous_target + S (fpmp_target_recode_exists_previous) = S ((S (fpmp_index_recode_exists_previous)) * tc)) /\ exists ff_q_fpmp_recode_exists_previous_target. tb = ff_q_fpmp_recode_exists_previous_target * S ((S (fpmp_index_recode_exists_previous)) * tc) + (fpmp_target_recode_exists_previous))) -> fpmp_target_recode_exists_previous = fpmp_left_recode_exists_previous * fpmp_right_recode_exists_previous)
  27. 0027exact IH
  28. 0028cases hprevious
  29. 0029cases hprevious_witness
  30. 0030have hleft : ∃ m. BetaAt(mb,mc,l,m)
    Exact native replay linehave hleft : exists m. (((exists ff_h_recode_exists_left_last. ff_h_recode_exists_left_last + S (m) = S ((S (l)) * mc)) /\ exists ff_q_recode_exists_left_last. mb = ff_q_recode_exists_left_last * S ((S (l)) * mc) + (m)))
  31. 0031specialize beta_at_exists mb
  32. 0032specialize beta_at_exists mc
  33. 0033specialize beta_at_exists l
  34. 0034exact beta_at_exists
  35. 0035cases hleft
  36. 0036have hright : ∃ s. BetaAt(sb,sc,l,s)
    Exact native replay linehave hright : exists s. (((exists ff_h_recode_exists_right_last. ff_h_recode_exists_right_last + S (s) = S ((S (l)) * sc)) /\ exists ff_q_recode_exists_right_last. sb = ff_q_recode_exists_right_last * S ((S (l)) * sc) + (s)))
  37. 0037specialize beta_at_exists sb
  38. 0038specialize beta_at_exists sc
  39. 0039specialize beta_at_exists l
  40. 0040exact beta_at_exists
  41. 0041cases hright
  42. 0042specialize beta_pointwise_mul_prefix_extend mb
  43. 0043specialize beta_pointwise_mul_prefix_extend mc
  44. 0044specialize beta_pointwise_mul_prefix_extend sb
  45. 0045specialize beta_pointwise_mul_prefix_extend sc
  46. 0046specialize beta_pointwise_mul_prefix_extend x
  47. 0047specialize beta_pointwise_mul_prefix_extend x1
  48. 0048specialize beta_pointwise_mul_prefix_extend l
  49. 0049specialize beta_pointwise_mul_prefix_extend x2
  50. 0050specialize beta_pointwise_mul_prefix_extend x3
  51. 0051apply beta_pointwise_mul_prefix_extend
  52. 0052exact hprevious_witness_witness
  53. 0053exact hleft_witness
  54. 0054exact hright_witness