PA007P · theorem

gauss_signed_pointwise_mul_scale_mod

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

Signed magnitudes times their 1/r factors are pointwise congruent to the scaled source prefix.

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. ∀ h. ∀ r. ∀ a. ∀ b. ∀ c. ∀ mb. ∀ mc. ∀ sb. ∀ sc. ∀ fb. ∀ fc. ∀ tb. ∀ tc. p = S r → r = 2 · h → (∀ x. Lt(x,h) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(mb,mc,x,z) ∧ (BetaAt(sb,sc,x,n) ∧ (Lt(0,z) ∧ (Le(z,h) ∧ ((n = 0 ∨ n = 1) ∧ (n = 0 ∧ ModEq(p,a · y,z) ∨ n = 1 ∧ ModEq(p,a · y,2 · h · z)))))))) → (∀ x. ∀ y. Lt(x,h) → BetaAt(sb,sc,x,y) → y = 0 ∧ BetaAt(fb,fc,x,1) ∨ y = 1 ∧ BetaAt(fb,fc,x,r)) → (∀ x. ∀ y. ∀ z. ∀ n. Lt(x,h) → BetaAt(mb,mc,x,y) → BetaAt(fb,fc,x,z) → BetaAt(tb,tc,x,n) → n = y · z) → ∀ x. ∀ y. ∀ z. Lt(x,h) → BetaAt(b,c,x,y) → BetaAt(tb,tc,x,z) → ModEq(p,a · 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

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt

20 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt

9 occurrences

Exact expanded native-PA statement
forall p h r a b c mb mc sb sc fb fc tb tc. p = S r -> r = 2 * h -> (forall gsp_index_pointwise_signed_prefix. (exists gsp_lt_gap_pointwise_signed_prefix_index_bound. gsp_lt_gap_pointwise_signed_prefix_index_bound + S gsp_index_pointwise_signed_prefix = h) -> (exists gsp_value_pointwise_signed_prefix_entry gsp_magnitude_pointwise_signed_prefix_entry gsp_sign_pointwise_signed_prefix_entry. (((exists ff_h_gsp_pointwise_signed_prefix_entry_source. ff_h_gsp_pointwise_signed_prefix_entry_source + S (gsp_value_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * c)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_source. b = ff_q_gsp_pointwise_signed_prefix_entry_source * S ((S (gsp_index_pointwise_signed_prefix)) * c) + (gsp_value_pointwise_signed_prefix_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_prefix_entry_magnitude. ff_h_gsp_pointwise_signed_prefix_entry_magnitude + S (gsp_magnitude_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * mc)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_magnitude. mb = ff_q_gsp_pointwise_signed_prefix_entry_magnitude * S ((S (gsp_index_pointwise_signed_prefix)) * mc) + (gsp_magnitude_pointwise_signed_prefix_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_prefix_entry_sign. ff_h_gsp_pointwise_signed_prefix_entry_sign + S (gsp_sign_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * sc)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_sign. sb = ff_q_gsp_pointwise_signed_prefix_entry_sign * S ((S (gsp_index_pointwise_signed_prefix)) * sc) + (gsp_sign_pointwise_signed_prefix_entry))) /\ ((exists gsp_lt_gap_pointwise_signed_prefix_entry_positive. gsp_lt_gap_pointwise_signed_prefix_entry_positive + S 0 = gsp_magnitude_pointwise_signed_prefix_entry) /\ ((exists gsp_le_gap_pointwise_signed_prefix_entry_bounded. gsp_le_gap_pointwise_signed_prefix_entry_bounded + gsp_magnitude_pointwise_signed_prefix_entry = h) /\ ((gsp_sign_pointwise_signed_prefix_entry = 0 \/ gsp_sign_pointwise_signed_prefix_entry = 1) /\ (((gsp_sign_pointwise_signed_prefix_entry = 0 /\ (exists gsp_mod_left_pointwise_signed_prefix_entry_lower gsp_mod_right_pointwise_signed_prefix_entry_lower. (a * gsp_value_pointwise_signed_prefix_entry) + p * gsp_mod_left_pointwise_signed_prefix_entry_lower = (gsp_magnitude_pointwise_signed_prefix_entry) + p * gsp_mod_right_pointwise_signed_prefix_entry_lower)) \/ (gsp_sign_pointwise_signed_prefix_entry = 1 /\ (exists gsp_mod_left_pointwise_signed_prefix_entry_reflected gsp_mod_right_pointwise_signed_prefix_entry_reflected. (a * gsp_value_pointwise_signed_prefix_entry) + p * gsp_mod_left_pointwise_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_pointwise_signed_prefix_entry) + p * gsp_mod_right_pointwise_signed_prefix_entry_reflected))))))))))) -> (forall gspf_index_pointwise_sign_factors gspf_bit_pointwise_sign_factors. (exists gsp_lt_gap_pointwise_sign_factors_bound. gsp_lt_gap_pointwise_sign_factors_bound + S gspf_index_pointwise_sign_factors = h) -> (((exists ff_h_gspf_pointwise_sign_factors_bit. ff_h_gspf_pointwise_sign_factors_bit + S (gspf_bit_pointwise_sign_factors) = S ((S (gspf_index_pointwise_sign_factors)) * sc)) /\ exists ff_q_gspf_pointwise_sign_factors_bit. sb = ff_q_gspf_pointwise_sign_factors_bit * S ((S (gspf_index_pointwise_sign_factors)) * sc) + (gspf_bit_pointwise_sign_factors))) -> (((gspf_bit_pointwise_sign_factors = 0) /\ (((exists gsp_beta_height_gspf_pointwise_sign_factors_one. gsp_beta_height_gspf_pointwise_sign_factors_one + S (1) = S ((S (gspf_index_pointwise_sign_factors)) * fc)) /\ exists gsp_beta_quotient_gspf_pointwise_sign_factors_one. fb = gsp_beta_quotient_gspf_pointwise_sign_factors_one * S ((S (gspf_index_pointwise_sign_factors)) * fc) + (1)))) \/ ((gspf_bit_pointwise_sign_factors = 1) /\ (((exists ff_h_gspf_pointwise_sign_factors_predecessor. ff_h_gspf_pointwise_sign_factors_predecessor + S (r) = S ((S (gspf_index_pointwise_sign_factors)) * fc)) /\ exists ff_q_gspf_pointwise_sign_factors_predecessor. fb = ff_q_gspf_pointwise_sign_factors_predecessor * S ((S (gspf_index_pointwise_sign_factors)) * fc) + (r)))))) -> (forall fpmp_index_pointwise_products fpmp_left_pointwise_products fpmp_right_pointwise_products fpmp_target_pointwise_products. (exists fpmp_gap_pointwise_products. fpmp_gap_pointwise_products + S fpmp_index_pointwise_products = h) -> (((exists ff_h_fpmp_pointwise_products_left. ff_h_fpmp_pointwise_products_left + S (fpmp_left_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * mc)) /\ exists ff_q_fpmp_pointwise_products_left. mb = ff_q_fpmp_pointwise_products_left * S ((S (fpmp_index_pointwise_products)) * mc) + (fpmp_left_pointwise_products))) -> (((exists ff_h_fpmp_pointwise_products_right. ff_h_fpmp_pointwise_products_right + S (fpmp_right_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * fc)) /\ exists ff_q_fpmp_pointwise_products_right. fb = ff_q_fpmp_pointwise_products_right * S ((S (fpmp_index_pointwise_products)) * fc) + (fpmp_right_pointwise_products))) -> (((exists ff_h_fpmp_pointwise_products_target. ff_h_fpmp_pointwise_products_target + S (fpmp_target_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * tc)) /\ exists ff_q_fpmp_pointwise_products_target. tb = ff_q_fpmp_pointwise_products_target * S ((S (fpmp_index_pointwise_products)) * tc) + (fpmp_target_pointwise_products))) -> fpmp_target_pointwise_products = fpmp_left_pointwise_products * fpmp_right_pointwise_products) -> (forall fsp_index_pointwise_scale_result fsp_source_pointwise_scale_result fsp_target_pointwise_scale_result. (exists fsp_gap_pointwise_scale_result. fsp_gap_pointwise_scale_result + S fsp_index_pointwise_scale_result = h) -> (((exists fsp_source_height_pointwise_scale_result. fsp_source_height_pointwise_scale_result + S (fsp_source_pointwise_scale_result) = S ((S (fsp_index_pointwise_scale_result)) * c)) /\ exists fsp_source_quotient_pointwise_scale_result. b = fsp_source_quotient_pointwise_scale_result * S ((S (fsp_index_pointwise_scale_result)) * c) + (fsp_source_pointwise_scale_result))) -> (((exists fsp_target_height_pointwise_scale_result. fsp_target_height_pointwise_scale_result + S (fsp_target_pointwise_scale_result) = S ((S (fsp_index_pointwise_scale_result)) * tc)) /\ exists fsp_target_quotient_pointwise_scale_result. tb = fsp_target_quotient_pointwise_scale_result * S ((S (fsp_index_pointwise_scale_result)) * tc) + (fsp_target_pointwise_scale_result))) -> (exists fsp_mod_left_pointwise_scale_result fsp_mod_right_pointwise_scale_result. a * fsp_source_pointwise_scale_result + p * fsp_mod_left_pointwise_scale_result = fsp_target_pointwise_scale_result + p * fsp_mod_right_pointwise_scale_result))

Proof neighborhood

Direct theorem prerequisites

PA002F beta_at_unique PA0002 mul_one PA000H mul_comm

Direct theorem dependents

PA007R gauss_signed_pointwise_mul_product_mod

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

110 script commands · 25 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 (3)
beta at uniquemul onemul comm
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro r
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro mb
  8. L8
    intro mc
  9. L9
    intro sb
  10. L10
    intro sc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro fb
  2. L12
    intro fc
  3. L13
    intro tb
  4. L14
    intro tc
  5. L15
    intro hp
  6. L16
    intro hr
  7. L17
    intro hsigned
  8. L18
    intro hfactor
  9. L19
    intro hmul
  10. L20
    intro i
03Fix variables and assumptionsL21–25

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

  1. L21
    intro v
  2. L22
    intro t
  3. L23
    intro hi
  4. L24
    intro hv
  5. L25
    intro ht
04Establish hentryL26–29

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

  1. L26
    have hentry · expand full local formula (710 characters)have hentry : ∃ gsp_value_pointwise_signed_entry. ∃ gsp_magnitude_pointwise_signed_entry. ∃ gsp_sign_pointwise_signed_entry. BetaAt(b,c,i,gsp_value_pointwise_signed_entry) ∧ (BetaAt(mb,mc,i,gsp_magnitude_pointwise_signed_entry) ∧ (BetaAt(sb,sc,i,gsp_sign_pointwise_signed_entry) ∧ (Lt(0,gsp_magnitude_pointwise_signed_entry) ∧ (Le(gsp_magnitude_pointwise_signed_entry,h) ∧ ((gsp_sign_pointwise_signed_entry = 0 ∨ gsp_sign_pointwise_signed_entry = 1) ∧ (gsp_sign_pointwise_signed_entry = 0 ∧ ModEq(p,a · gsp_value_pointwise_signed_entry,gsp_magnitude_pointwise_signed_entry) ∨ gsp_sign_pointwise_signed_entry = 1 ∧ ModEq(p,a · gsp_value_pointwise_signed_entry,2 · h · gsp_magnitude_pointwise_signed_entry)))))))
    Definitions: BetaAt(b,c,i,gsp_value_pointwise_signed_entry)BetaAt(mb,mc,i,gsp_magnitude_pointwise_signed_entry)BetaAt(sb,sc,i,gsp_sign_pointwise_signed_entry)Lt(0,gsp_magnitude_pointwise_signed_entry)Le(gsp_magnitude_pointwise_signed_entry,h)ModEq(p,a · gsp_value_pointwise_signed_entry,gsp_magnitude_pointwise_signed_entry)ModEq(p,a · gsp_value_pointwise_signed_entry,2 · h · gsp_magnitude_pointwise_signed_entry)Original native command in the exact edition
  2. L27
    specialize hsigned i
  3. L28
    apply hsigned
  4. L29
    exact hi
05Separate the logical casesL30–38

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

  1. L30
    cases hentry
  2. L31
    cases hentry_witness
  3. L32
    cases hentry_witness_witness
  4. L33
    cases hentry_witness_witness_witness
  5. L34
    cases hentry_witness_witness_witness_right
  6. L35
    cases hentry_witness_witness_witness_right_right
  7. L36
    cases hentry_witness_witness_witness_right_right_right
  8. L37
    cases hentry_witness_witness_witness_right_right_right_right
  9. L38
    cases hentry_witness_witness_witness_right_right_right_right_right
06Establish hvxL39–47

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

  1. L39
    have hvx : v = x
  2. L40
    specialize beta_at_unique b
  3. L41
    specialize beta_at_unique c
  4. L42
    specialize beta_at_unique i
  5. L43
    specialize beta_at_unique v
  6. L44
    specialize beta_at_unique x
  7. L45
    apply beta_at_unique
  8. L46
    exact hv
  9. L47
    exact hentry_witness_witness_witness_left
07Establish hfactor_caseL48–53

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

  1. L48
    have hfactor_case : x2 = 0 ∧ BetaAt(fb,fc,i,1) ∨ x2 = 1 ∧ BetaAt(fb,fc,i,r)Definitions: BetaAt(fb,fc,i,1)BetaAt(fb,fc,i,r)Original native command in the exact edition
  2. L49
    specialize hfactor i
  3. L50
    specialize hfactor x2
  4. L51
    apply hfactor
  5. L52
    exact hi
  6. L53
    exact hentry_witness_witness_witness_right_right_left
08Separate the logical casesL54–57

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

  1. L54
    cases hentry_witness_witness_witness_right_right_right_right_right_right
  2. L55
    cases hentry_witness_witness_witness_right_right_right_right_right_right_left
  3. L56
    cases hfactor_case
  4. L57
    cases hfactor_case_left
09Establish ht_oneL58–67

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

  1. L58
    have ht_one : t = x1 * 1
  2. L59
    specialize hmul i
  3. L60
    specialize hmul x1
  4. L61
    specialize hmul 1
  5. L62
    specialize hmul t
  6. L63
    apply hmul
  7. L64
    exact hi
  8. L65
    exact hentry_witness_witness_witness_right_left
  9. L66
    exact hfactor_case_left_right
  10. L67
    exact ht
10Calculate and transport equalitiesL68–69

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

  1. L68
    rewrite hvx
  2. L69
    rewrite ht_one
11Use earlier factsL70–70

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

  1. L70
    specialize mul_one x1
12Calculate and transport equalitiesL71–71

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

  1. L71
    rewrite mul_one
13Use earlier factsL72–72

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

  1. L72
    exact hentry_witness_witness_witness_right_right_right_right_right_right_left_right
14Separate the logical casesL73–74

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

  1. L73
    cases hfactor_case_right
  2. L74
    exfalso
15Use earlier factsL75–75

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

  1. L75
    apply PA1
16Calculate and transport equalitiesL76–77

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

  1. L76
    trans x2
  2. L77
    symm
17Use earlier factsL78–79

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

  1. L78
    exact hfactor_case_right_left
  2. L79
    exact hentry_witness_witness_witness_right_right_right_right_right_right_left_left
18Separate the logical casesL80–83

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

  1. L80
    cases hentry_witness_witness_witness_right_right_right_right_right_right_right
  2. L81
    cases hfactor_case
  3. L82
    cases hfactor_case_left
  4. L83
    exfalso
19Use earlier factsL84–84

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

  1. L84
    apply PA1
20Calculate and transport equalitiesL85–86

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

  1. L85
    trans x2
  2. L86
    symm
21Use earlier factsL87–88

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

  1. L87
    exact hentry_witness_witness_witness_right_right_right_right_right_right_right_left
  2. L88
    exact hfactor_case_left_left
22Separate the logical casesL89–89

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

  1. L89
    cases hfactor_case_right
23Establish ht_rL90–99

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

  1. L90
    have ht_r : t = x1 * r
  2. L91
    specialize hmul i
  3. L92
    specialize hmul x1
  4. L93
    specialize hmul r
  5. L94
    specialize hmul t
  6. L95
    apply hmul
  7. L96
    exact hi
  8. L97
    exact hentry_witness_witness_witness_right_left
  9. L98
    exact hfactor_case_right_right
  10. L99
    exact ht
24Establish ht_reflectedL100–109

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

  1. L100
    have ht_reflected : t = (2 * h) * x1
  2. L101
    trans x1 * r
  3. L102
    exact ht_r
  4. L103
    trans r * x1
  5. L104
    apply mul_comm
  6. L105
    congr
  7. L106
    exact hr
  8. L107
    refl
  9. L108
    rewrite hvx
  10. L109
    rewrite ht_reflected
25Use earlier factsL110–110

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

  1. L110
    exact hentry_witness_witness_witness_right_right_right_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 110 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro r
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro mb
  8. 0008intro mc
  9. 0009intro sb
  10. 0010intro sc
  11. 0011intro fb
  12. 0012intro fc
  13. 0013intro tb
  14. 0014intro tc
  15. 0015intro hp
  16. 0016intro hr
  17. 0017intro hsigned
  18. 0018intro hfactor
  19. 0019intro hmul
  20. 0020intro i
  21. 0021intro v
  22. 0022intro t
  23. 0023intro hi
  24. 0024intro hv
  25. 0025intro ht
  26. 0026have hentry : ∃ gsp_value_pointwise_signed_entry. ∃ gsp_magnitude_pointwise_signed_entry. ∃ gsp_sign_pointwise_signed_entry. BetaAt(b,c,i,gsp_value_pointwise_signed_entry) ∧ (BetaAt(mb,mc,i,gsp_magnitude_pointwise_signed_entry) ∧ (BetaAt(sb,sc,i,gsp_sign_pointwise_signed_entry) ∧ (Lt(0,gsp_magnitude_pointwise_signed_entry) ∧ (Le(gsp_magnitude_pointwise_signed_entry,h) ∧ ((gsp_sign_pointwise_signed_entry = 0 ∨ gsp_sign_pointwise_signed_entry = 1) ∧ (gsp_sign_pointwise_signed_entry = 0 ∧ ModEq(p,a · gsp_value_pointwise_signed_entry,gsp_magnitude_pointwise_signed_entry) ∨ gsp_sign_pointwise_signed_entry = 1 ∧ ModEq(p,a · gsp_value_pointwise_signed_entry,2 · h · gsp_magnitude_pointwise_signed_entry)))))))
    Exact native replay linehave hentry : exists gsp_value_pointwise_signed_entry gsp_magnitude_pointwise_signed_entry gsp_sign_pointwise_signed_entry. (((exists ff_h_gsp_pointwise_signed_entry_source. ff_h_gsp_pointwise_signed_entry_source + S (gsp_value_pointwise_signed_entry) = S ((S (i)) * c)) /\ exists ff_q_gsp_pointwise_signed_entry_source. b = ff_q_gsp_pointwise_signed_entry_source * S ((S (i)) * c) + (gsp_value_pointwise_signed_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_entry_magnitude. ff_h_gsp_pointwise_signed_entry_magnitude + S (gsp_magnitude_pointwise_signed_entry) = S ((S (i)) * mc)) /\ exists ff_q_gsp_pointwise_signed_entry_magnitude. mb = ff_q_gsp_pointwise_signed_entry_magnitude * S ((S (i)) * mc) + (gsp_magnitude_pointwise_signed_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_entry_sign. ff_h_gsp_pointwise_signed_entry_sign + S (gsp_sign_pointwise_signed_entry) = S ((S (i)) * sc)) /\ exists ff_q_gsp_pointwise_signed_entry_sign. sb = ff_q_gsp_pointwise_signed_entry_sign * S ((S (i)) * sc) + (gsp_sign_pointwise_signed_entry))) /\ ((exists gsp_lt_gap_pointwise_signed_entry_positive. gsp_lt_gap_pointwise_signed_entry_positive + S 0 = gsp_magnitude_pointwise_signed_entry) /\ ((exists gsp_le_gap_pointwise_signed_entry_bounded. gsp_le_gap_pointwise_signed_entry_bounded + gsp_magnitude_pointwise_signed_entry = h) /\ ((gsp_sign_pointwise_signed_entry = 0 \/ gsp_sign_pointwise_signed_entry = 1) /\ (((gsp_sign_pointwise_signed_entry = 0 /\ (exists gsp_mod_left_pointwise_signed_entry_lower gsp_mod_right_pointwise_signed_entry_lower. (a * gsp_value_pointwise_signed_entry) + p * gsp_mod_left_pointwise_signed_entry_lower = (gsp_magnitude_pointwise_signed_entry) + p * gsp_mod_right_pointwise_signed_entry_lower)) \/ (gsp_sign_pointwise_signed_entry = 1 /\ (exists gsp_mod_left_pointwise_signed_entry_reflected gsp_mod_right_pointwise_signed_entry_reflected. (a * gsp_value_pointwise_signed_entry) + p * gsp_mod_left_pointwise_signed_entry_reflected = ((2 * h) * gsp_magnitude_pointwise_signed_entry) + p * gsp_mod_right_pointwise_signed_entry_reflected)))))))))
  27. 0027specialize hsigned i
  28. 0028apply hsigned
  29. 0029exact hi
  30. 0030cases hentry
  31. 0031cases hentry_witness
  32. 0032cases hentry_witness_witness
  33. 0033cases hentry_witness_witness_witness
  34. 0034cases hentry_witness_witness_witness_right
  35. 0035cases hentry_witness_witness_witness_right_right
  36. 0036cases hentry_witness_witness_witness_right_right_right
  37. 0037cases hentry_witness_witness_witness_right_right_right_right
  38. 0038cases hentry_witness_witness_witness_right_right_right_right_right
  39. 0039have hvx : v = x
  40. 0040specialize beta_at_unique b
  41. 0041specialize beta_at_unique c
  42. 0042specialize beta_at_unique i
  43. 0043specialize beta_at_unique v
  44. 0044specialize beta_at_unique x
  45. 0045apply beta_at_unique
  46. 0046exact hv
  47. 0047exact hentry_witness_witness_witness_left
  48. 0048have hfactor_case : x2 = 0 ∧ BetaAt(fb,fc,i,1) ∨ x2 = 1 ∧ BetaAt(fb,fc,i,r)
    Exact native replay linehave hfactor_case : (((x2 = 0) /\ (((exists gsp_beta_height_pointwise_factor_one. gsp_beta_height_pointwise_factor_one + S (1) = S ((S (i)) * fc)) /\ exists gsp_beta_quotient_pointwise_factor_one. fb = gsp_beta_quotient_pointwise_factor_one * S ((S (i)) * fc) + (1)))) \/ ((x2 = 1) /\ (((exists ff_h_pointwise_factor_r. ff_h_pointwise_factor_r + S (r) = S ((S (i)) * fc)) /\ exists ff_q_pointwise_factor_r. fb = ff_q_pointwise_factor_r * S ((S (i)) * fc) + (r)))))
  49. 0049specialize hfactor i
  50. 0050specialize hfactor x2
  51. 0051apply hfactor
  52. 0052exact hi
  53. 0053exact hentry_witness_witness_witness_right_right_left
  54. 0054cases hentry_witness_witness_witness_right_right_right_right_right_right
  55. 0055cases hentry_witness_witness_witness_right_right_right_right_right_right_left
  56. 0056cases hfactor_case
  57. 0057cases hfactor_case_left
  58. 0058have ht_one : t = x1 * 1
  59. 0059specialize hmul i
  60. 0060specialize hmul x1
  61. 0061specialize hmul 1
  62. 0062specialize hmul t
  63. 0063apply hmul
  64. 0064exact hi
  65. 0065exact hentry_witness_witness_witness_right_left
  66. 0066exact hfactor_case_left_right
  67. 0067exact ht
  68. 0068rewrite hvx
  69. 0069rewrite ht_one
  70. 0070specialize mul_one x1
  71. 0071rewrite mul_one
  72. 0072exact hentry_witness_witness_witness_right_right_right_right_right_right_left_right
  73. 0073cases hfactor_case_right
  74. 0074exfalso
  75. 0075apply PA1
  76. 0076trans x2
  77. 0077symm
  78. 0078exact hfactor_case_right_left
  79. 0079exact hentry_witness_witness_witness_right_right_right_right_right_right_left_left
  80. 0080cases hentry_witness_witness_witness_right_right_right_right_right_right_right
  81. 0081cases hfactor_case
  82. 0082cases hfactor_case_left
  83. 0083exfalso
  84. 0084apply PA1
  85. 0085trans x2
  86. 0086symm
  87. 0087exact hentry_witness_witness_witness_right_right_right_right_right_right_right_left
  88. 0088exact hfactor_case_left_left
  89. 0089cases hfactor_case_right
  90. 0090have ht_r : t = x1 * r
  91. 0091specialize hmul i
  92. 0092specialize hmul x1
  93. 0093specialize hmul r
  94. 0094specialize hmul t
  95. 0095apply hmul
  96. 0096exact hi
  97. 0097exact hentry_witness_witness_witness_right_left
  98. 0098exact hfactor_case_right_right
  99. 0099exact ht
  100. 0100have ht_reflected : t = (2 * h) * x1
  101. 0101trans x1 * r
  102. 0102exact ht_r
  103. 0103trans r * x1
  104. 0104apply mul_comm
  105. 0105congr
  106. 0106exact hr
  107. 0107refl
  108. 0108rewrite hvx
  109. 0109rewrite ht_reflected
  110. 0110exact hentry_witness_witness_witness_right_right_right_right_right_right_right_right