PA00ES · theorem

eisenstein_zero_width_rectangle_sum_zero

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

Every semantic zero-width rectangle has relational outer Sum zero.

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. ∀ q. ∀ z. ∀ bb. ∀ bc. ∀ l. ∀ T. z = 0 → (∀ x. Lt(x,l) → ∃ y. BetaAt(bb,bc,x,y) ∧ (∃ n. ∃ m. (∀ k. Lt(k,z) → ∃ i. BetaAt(n,m,k,i) ∧ (i = 0 ∧ (Lt(q · S x,p · S k) ∧ ¬Lt(p · S k,q · S x)) ∨ i = 1 ∧ (Lt(p · S k,q · S x) ∧ ¬Lt(q · S x,p · S k)))) ∧ BitCount(n,m,z,y))) → Sum(bb,bc,l,T) → T = 0

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 PD0015 Sum PD0017 BitCount

10 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0017 BitCount PD0019 Repeat

13 occurrences

Exact expanded native-PA statement
forall p q z bb bc l T. z = 0 -> (forall erc_row_fubini_zero_width_prefix. (exists erc_lt_gap_fubini_zero_width_prefix_bound. erc_lt_gap_fubini_zero_width_prefix_bound + S (erc_row_fubini_zero_width_prefix) = l) -> exists erc_count_fubini_zero_width_prefix. ((((exists ff_h_erc_fubini_zero_width_prefix_decoded. ff_h_erc_fubini_zero_width_prefix_decoded + S (erc_count_fubini_zero_width_prefix) = S ((S (erc_row_fubini_zero_width_prefix)) * bc)) /\ exists ff_q_erc_fubini_zero_width_prefix_decoded. bb = ff_q_erc_fubini_zero_width_prefix_decoded * S ((S (erc_row_fubini_zero_width_prefix)) * bc) + (erc_count_fubini_zero_width_prefix))) /\ (exists erc_row_code_fubini_zero_width_prefix_witness erc_row_scale_fubini_zero_width_prefix_witness. ((forall eri_column_erc_fubini_zero_width_prefix_witness_row. (exists eri_gap_erc_fubini_zero_width_prefix_witness_row_bound. eri_gap_erc_fubini_zero_width_prefix_witness_row_bound + S (eri_column_erc_fubini_zero_width_prefix_witness_row) = z) -> exists eri_bit_erc_fubini_zero_width_prefix_witness_row. ((((exists ff_h_eri_erc_fubini_zero_width_prefix_witness_row_decoded. ff_h_eri_erc_fubini_zero_width_prefix_witness_row_decoded + S (eri_bit_erc_fubini_zero_width_prefix_witness_row) = S ((S (eri_column_erc_fubini_zero_width_prefix_witness_row)) * erc_row_scale_fubini_zero_width_prefix_witness)) /\ exists ff_q_eri_erc_fubini_zero_width_prefix_witness_row_decoded. erc_row_code_fubini_zero_width_prefix_witness = ff_q_eri_erc_fubini_zero_width_prefix_witness_row_decoded * S ((S (eri_column_erc_fubini_zero_width_prefix_witness_row)) * erc_row_scale_fubini_zero_width_prefix_witness) + (eri_bit_erc_fubini_zero_width_prefix_witness_row))) /\ (((eri_bit_erc_fubini_zero_width_prefix_witness_row = 0 /\ ((exists eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_left. eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_left + S (q * S erc_row_fubini_zero_width_prefix) = p * S eri_column_erc_fubini_zero_width_prefix_witness_row) /\ ~(exists eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_right. eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_right + S (p * S eri_column_erc_fubini_zero_width_prefix_witness_row) = q * S erc_row_fubini_zero_width_prefix))) \/ (eri_bit_erc_fubini_zero_width_prefix_witness_row = 1 /\ ((exists eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_right. eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_right + S (p * S eri_column_erc_fubini_zero_width_prefix_witness_row) = q * S erc_row_fubini_zero_width_prefix) /\ ~(exists eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_left. eri_gap_erc_fubini_zero_width_prefix_witness_row_choice_left + S (q * S erc_row_fubini_zero_width_prefix) = p * S eri_column_erc_fubini_zero_width_prefix_witness_row))))))) /\ (((exists ff_u_erc_fubini_zero_width_prefix_witness_count_sum ff_v_erc_fubini_zero_width_prefix_witness_count_sum. ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_start. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_start. ff_u_erc_fubini_zero_width_prefix_witness_count_sum = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_terminal. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_terminal + S (erc_count_fubini_zero_width_prefix) = S ((S (z)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_terminal. ff_u_erc_fubini_zero_width_prefix_witness_count_sum = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_terminal * S ((S (z)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum) + (erc_count_fubini_zero_width_prefix))) /\ forall ff_i_erc_fubini_zero_width_prefix_witness_count_sum. (exists ff_lt_erc_fubini_zero_width_prefix_witness_count_sum_bound. ff_lt_erc_fubini_zero_width_prefix_witness_count_sum_bound + S ff_i_erc_fubini_zero_width_prefix_witness_count_sum = z) -> exists ff_a_erc_fubini_zero_width_prefix_witness_count_sum ff_r_erc_fubini_zero_width_prefix_witness_count_sum ff_s_erc_fubini_zero_width_prefix_witness_count_sum. ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_summand. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_summand + S (ff_a_erc_fubini_zero_width_prefix_witness_count_sum) = S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * erc_row_scale_fubini_zero_width_prefix_witness)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_summand. erc_row_code_fubini_zero_width_prefix_witness = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_summand * S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * erc_row_scale_fubini_zero_width_prefix_witness) + (ff_a_erc_fubini_zero_width_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_partial. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_partial + S (ff_r_erc_fubini_zero_width_prefix_witness_count_sum) = S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_partial. ff_u_erc_fubini_zero_width_prefix_witness_count_sum = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_partial * S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum) + (ff_r_erc_fubini_zero_width_prefix_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_sum_successor. ff_h_erc_fubini_zero_width_prefix_witness_count_sum_successor + S (ff_s_erc_fubini_zero_width_prefix_witness_count_sum) = S ((S (S ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_sum_successor. ff_u_erc_fubini_zero_width_prefix_witness_count_sum = ff_q_erc_fubini_zero_width_prefix_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_zero_width_prefix_witness_count_sum)) * ff_v_erc_fubini_zero_width_prefix_witness_count_sum) + (ff_s_erc_fubini_zero_width_prefix_witness_count_sum))) /\ ff_s_erc_fubini_zero_width_prefix_witness_count_sum = ff_r_erc_fubini_zero_width_prefix_witness_count_sum + ff_a_erc_fubini_zero_width_prefix_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_zero_width_prefix_witness_count_bits. (exists ff_lt_erc_fubini_zero_width_prefix_witness_count_bits_bound. ff_lt_erc_fubini_zero_width_prefix_witness_count_bits_bound + S ff_i_erc_fubini_zero_width_prefix_witness_count_bits = z) -> exists ff_bit_erc_fubini_zero_width_prefix_witness_count_bits. ((((exists ff_h_erc_fubini_zero_width_prefix_witness_count_bits_decoded. ff_h_erc_fubini_zero_width_prefix_witness_count_bits_decoded + S (ff_bit_erc_fubini_zero_width_prefix_witness_count_bits) = S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_bits)) * erc_row_scale_fubini_zero_width_prefix_witness)) /\ exists ff_q_erc_fubini_zero_width_prefix_witness_count_bits_decoded. erc_row_code_fubini_zero_width_prefix_witness = ff_q_erc_fubini_zero_width_prefix_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_zero_width_prefix_witness_count_bits)) * erc_row_scale_fubini_zero_width_prefix_witness) + (ff_bit_erc_fubini_zero_width_prefix_witness_count_bits))) /\ (ff_bit_erc_fubini_zero_width_prefix_witness_count_bits = 0 \/ ff_bit_erc_fubini_zero_width_prefix_witness_count_bits = 1))))))))) -> (exists ff_u_fubini_zero_width_sum ff_v_fubini_zero_width_sum. ((((exists ff_h_fubini_zero_width_sum_start. ff_h_fubini_zero_width_sum_start + S (0) = S ((S (0)) * ff_v_fubini_zero_width_sum)) /\ exists ff_q_fubini_zero_width_sum_start. ff_u_fubini_zero_width_sum = ff_q_fubini_zero_width_sum_start * S ((S (0)) * ff_v_fubini_zero_width_sum) + (0))) /\ ((((exists ff_h_fubini_zero_width_sum_terminal. ff_h_fubini_zero_width_sum_terminal + S (T) = S ((S (l)) * ff_v_fubini_zero_width_sum)) /\ exists ff_q_fubini_zero_width_sum_terminal. ff_u_fubini_zero_width_sum = ff_q_fubini_zero_width_sum_terminal * S ((S (l)) * ff_v_fubini_zero_width_sum) + (T))) /\ forall ff_i_fubini_zero_width_sum. (exists ff_lt_fubini_zero_width_sum_bound. ff_lt_fubini_zero_width_sum_bound + S ff_i_fubini_zero_width_sum = l) -> exists ff_a_fubini_zero_width_sum ff_r_fubini_zero_width_sum ff_s_fubini_zero_width_sum. ((((exists ff_h_fubini_zero_width_sum_summand. ff_h_fubini_zero_width_sum_summand + S (ff_a_fubini_zero_width_sum) = S ((S (ff_i_fubini_zero_width_sum)) * bc)) /\ exists ff_q_fubini_zero_width_sum_summand. bb = ff_q_fubini_zero_width_sum_summand * S ((S (ff_i_fubini_zero_width_sum)) * bc) + (ff_a_fubini_zero_width_sum))) /\ ((((exists ff_h_fubini_zero_width_sum_partial. ff_h_fubini_zero_width_sum_partial + S (ff_r_fubini_zero_width_sum) = S ((S (ff_i_fubini_zero_width_sum)) * ff_v_fubini_zero_width_sum)) /\ exists ff_q_fubini_zero_width_sum_partial. ff_u_fubini_zero_width_sum = ff_q_fubini_zero_width_sum_partial * S ((S (ff_i_fubini_zero_width_sum)) * ff_v_fubini_zero_width_sum) + (ff_r_fubini_zero_width_sum))) /\ ((((exists ff_h_fubini_zero_width_sum_successor. ff_h_fubini_zero_width_sum_successor + S (ff_s_fubini_zero_width_sum) = S ((S (S ff_i_fubini_zero_width_sum)) * ff_v_fubini_zero_width_sum)) /\ exists ff_q_fubini_zero_width_sum_successor. ff_u_fubini_zero_width_sum = ff_q_fubini_zero_width_sum_successor * S ((S (S ff_i_fubini_zero_width_sum)) * ff_v_fubini_zero_width_sum) + (ff_s_fubini_zero_width_sum))) /\ ff_s_fubini_zero_width_sum = ff_r_fubini_zero_width_sum + ff_a_fubini_zero_width_sum)))))) -> T = 0

Proof neighborhood

Direct theorem prerequisites

PA0045 beta_repeat_exists PA00E6 eisenstein_rectangle_decoded_row_count PA0048 bit_count_zero PA00CT beta_sum_transport_prefix PA00EK beta_repeat_sum_exact PA000H mul_comm PA000D mul_zero_left

Direct theorem dependents

PA00FC eisenstein_fubini_universal

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

82 script commands · 15 reading checkpoints · 7 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 (7)
beta repeat existseisenstein rectangle decoded row countbit count zerobeta sum transport prefixbeta repeat sum exactmul commmul zero left
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro z
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro l
  7. L7
    intro T
  8. L8
    intro hz
  9. L9
    intro hprefix
  10. L10
    intro hsum
02Establish hrepeatL11–14

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

  1. L11
    have hrepeat : ∃ rb. ∃ rc. Repeat(rb,rc,z,l)Definitions: Repeat(rb,rc,z,l)Original native command in the exact edition
  2. L12
    specialize beta_repeat_exists z
  3. L13
    specialize beta_repeat_exists l
  4. L14
    exact beta_repeat_exists
03Separate the logical casesL15–16

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

  1. L15
    cases hrepeat
  2. L16
    cases hrepeat_witness
04Establish hpreserveL17–21

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

  1. L17
    have hpreserve : ∀ i. ∀ n. Lt(i,l) → BetaAt(bb,bc,i,n) → BetaAt(x,x1,i,n)Definitions: Lt(i,l)BetaAt(bb,bc,i,n)BetaAt(x,x1,i,n)Original native command in the exact edition
  2. L18
    intro i
  3. L19
    intro n
  4. L20
    intro hi
  5. L21
    intro hn
05Establish hwitnessL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein rectangle decoded row count.

  1. L22
    have hwitness : ∃ erc_row_code_fubini_zero_width_decoded_witness. ∃ erc_row_scale_fubini_zero_width_decoded_witness. (∀ x. Lt(x,z) → ∃ y. BetaAt(erc_row_code_fubini_zero_width_decoded_witness,erc_row_scale_fubini_zero_width_decoded_witness,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))) ∧ BitCount(erc_row_code_fubini_zero_width_decoded_witness,erc_row_scale_fubini_zero_width_decoded_witness,z,n)Definitions: Lt(x,z)BetaAt(erc_row_code_fubini_zero_width_decoded_witness,erc_row_scale_fubini_zero_width_decoded_witness,x,y)Lt(q · S i,p · S x)Lt(p · S x,q · S i)BitCount(erc_row_code_fubini_zero_width_decoded_witness,erc_row_scale_fubini_zero_width_decoded_witness,z,n)Original native command in the exact edition
  2. L23
    specialize eisenstein_rectangle_decoded_row_count p
  3. L24
    specialize eisenstein_rectangle_decoded_row_count q
  4. L25
    specialize eisenstein_rectangle_decoded_row_count z
  5. L26
    specialize eisenstein_rectangle_decoded_row_count bb
  6. L27
    specialize eisenstein_rectangle_decoded_row_count bc
  7. L28
    specialize eisenstein_rectangle_decoded_row_count l
  8. L29
    specialize eisenstein_rectangle_decoded_row_count i
  9. L30
    specialize eisenstein_rectangle_decoded_row_count n
  10. L31
    apply eisenstein_rectangle_decoded_row_count
06Use earlier factsL32–34

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

  1. L32
    exact hprefix
  2. L33
    exact hi
  3. L34
    exact hn
07Separate the logical casesL35–37

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

  1. L35
    cases hwitness
  2. L36
    cases hwitness_witness
  3. L37
    cases hwitness_witness_witness
08Establish hnzeroL38–45

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

  1. L38
    have hnzero : n = 0
  2. L39
    specialize bit_count_zero x2
  3. L40
    specialize bit_count_zero x3
  4. L41
    specialize bit_count_zero z
  5. L42
    specialize bit_count_zero n
  6. L43
    apply bit_count_zero
  7. L44
    exact hz
  8. L45
    exact hwitness_witness_witness_right
09Establish hzero_entryL46–54

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

  1. L46
    have hzero_entry : BetaAt(x,x1,i,z)Definitions: BetaAt(x,x1,i,z)Original native command in the exact edition
  2. L47
    specialize hrepeat_witness_witness i
  3. L48
    apply hrepeat_witness_witness
  4. L49
    exact hi
  5. L50
    rewrite hz at hzero_entry
  6. L51
    rewrite hz at hzero_entry
  7. L52
    rewrite hnzero
  8. L53
    rewrite hnzero
  9. L54
    exact hzero_entry
10Establish hrepeat_sumL55–64

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

  1. L55
    have hrepeat_sum : Sum(x,x1,l,T)Definitions: Sum(x,x1,l,T)Original native command in the exact edition
  2. L56
    specialize beta_sum_transport_prefix bb
  3. L57
    specialize beta_sum_transport_prefix bc
  4. L58
    specialize beta_sum_transport_prefix x
  5. L59
    specialize beta_sum_transport_prefix x1
  6. L60
    specialize beta_sum_transport_prefix l
  7. L61
    specialize beta_sum_transport_prefix T
  8. L62
    apply beta_sum_transport_prefix
  9. L63
    exact hsum
  10. L64
    exact hpreserve
11Establish hproductL65–74

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

  1. L65
    have hproduct : T = l * z
  2. L66
    specialize beta_repeat_sum_exact x
  3. L67
    specialize beta_repeat_sum_exact x1
  4. L68
    specialize beta_repeat_sum_exact z
  5. L69
    specialize beta_repeat_sum_exact l
  6. L70
    specialize beta_repeat_sum_exact T
  7. L71
    apply beta_repeat_sum_exact
  8. L72
    exact hrepeat_witness_witness
  9. L73
    exact hrepeat_sum
  10. L74
    rewrite hz at hproduct
12Calculate and transport equalitiesL75–75

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

  1. L75
    trans l * 0
13Use earlier factsL76–76

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

  1. L76
    exact hproduct
14Calculate and transport equalitiesL77–77

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

  1. L77
    trans 0 * l
15Use earlier factsL78–82

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

  1. L78
    specialize mul_comm l
  2. L79
    specialize mul_comm 0
  3. L80
    exact mul_comm
  4. L81
    specialize mul_zero_left l
  5. L82
    exact mul_zero_left

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro z
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro l
  7. 0007intro T
  8. 0008intro hz
  9. 0009intro hprefix
  10. 0010intro hsum
  11. 0011have hrepeat : ∃ rb. ∃ rc. Repeat(rb,rc,z,l)
    Exact native replay linehave hrepeat : exists rb rc. (forall ff_i_fubini_zero_width_repeat. (exists ff_lt_fubini_zero_width_repeat_bound. ff_lt_fubini_zero_width_repeat_bound + S ff_i_fubini_zero_width_repeat = l) -> (((exists ff_h_fubini_zero_width_repeat_decoded. ff_h_fubini_zero_width_repeat_decoded + S (z) = S ((S (ff_i_fubini_zero_width_repeat)) * rc)) /\ exists ff_q_fubini_zero_width_repeat_decoded. rb = ff_q_fubini_zero_width_repeat_decoded * S ((S (ff_i_fubini_zero_width_repeat)) * rc) + (z))))
  12. 0012specialize beta_repeat_exists z
  13. 0013specialize beta_repeat_exists l
  14. 0014exact beta_repeat_exists
  15. 0015cases hrepeat
  16. 0016cases hrepeat_witness
  17. 0017have hpreserve : ∀ i. ∀ n. Lt(i,l) → BetaAt(bb,bc,i,n) → BetaAt(x,x1,i,n)
    Exact native replay linehave hpreserve : forall i n. (exists efrd_lt_gap_fubini_zero_width_preserve_bound. efrd_lt_gap_fubini_zero_width_preserve_bound + S (i) = l) -> (((exists ff_h_fubini_zero_width_preserve_source. ff_h_fubini_zero_width_preserve_source + S (n) = S ((S (i)) * bc)) /\ exists ff_q_fubini_zero_width_preserve_source. bb = ff_q_fubini_zero_width_preserve_source * S ((S (i)) * bc) + (n))) -> (((exists ff_h_fubini_zero_width_preserve_target. ff_h_fubini_zero_width_preserve_target + S (n) = S ((S (i)) * x1)) /\ exists ff_q_fubini_zero_width_preserve_target. x = ff_q_fubini_zero_width_preserve_target * S ((S (i)) * x1) + (n)))
  18. 0018intro i
  19. 0019intro n
  20. 0020intro hi
  21. 0021intro hn
  22. 0022have hwitness : ∃ erc_row_code_fubini_zero_width_decoded_witness. ∃ erc_row_scale_fubini_zero_width_decoded_witness. (∀ x. Lt(x,z) → ∃ y. BetaAt(erc_row_code_fubini_zero_width_decoded_witness,erc_row_scale_fubini_zero_width_decoded_witness,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))) ∧ BitCount(erc_row_code_fubini_zero_width_decoded_witness,erc_row_scale_fubini_zero_width_decoded_witness,z,n)
    Exact native replay linehave hwitness : exists erc_row_code_fubini_zero_width_decoded_witness erc_row_scale_fubini_zero_width_decoded_witness. ((forall eri_column_erc_fubini_zero_width_decoded_witness_row. (exists eri_gap_erc_fubini_zero_width_decoded_witness_row_bound. eri_gap_erc_fubini_zero_width_decoded_witness_row_bound + S (eri_column_erc_fubini_zero_width_decoded_witness_row) = z) -> exists eri_bit_erc_fubini_zero_width_decoded_witness_row. ((((exists ff_h_eri_erc_fubini_zero_width_decoded_witness_row_decoded. ff_h_eri_erc_fubini_zero_width_decoded_witness_row_decoded + S (eri_bit_erc_fubini_zero_width_decoded_witness_row) = S ((S (eri_column_erc_fubini_zero_width_decoded_witness_row)) * erc_row_scale_fubini_zero_width_decoded_witness)) /\ exists ff_q_eri_erc_fubini_zero_width_decoded_witness_row_decoded. erc_row_code_fubini_zero_width_decoded_witness = ff_q_eri_erc_fubini_zero_width_decoded_witness_row_decoded * S ((S (eri_column_erc_fubini_zero_width_decoded_witness_row)) * erc_row_scale_fubini_zero_width_decoded_witness) + (eri_bit_erc_fubini_zero_width_decoded_witness_row))) /\ (((eri_bit_erc_fubini_zero_width_decoded_witness_row = 0 /\ ((exists eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_left. eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_fubini_zero_width_decoded_witness_row) /\ ~(exists eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_right. eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_right + S (p * S eri_column_erc_fubini_zero_width_decoded_witness_row) = q * S i))) \/ (eri_bit_erc_fubini_zero_width_decoded_witness_row = 1 /\ ((exists eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_right. eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_right + S (p * S eri_column_erc_fubini_zero_width_decoded_witness_row) = q * S i) /\ ~(exists eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_left. eri_gap_erc_fubini_zero_width_decoded_witness_row_choice_left + S (q * S i) = p * S eri_column_erc_fubini_zero_width_decoded_witness_row))))))) /\ (((exists ff_u_erc_fubini_zero_width_decoded_witness_count_sum ff_v_erc_fubini_zero_width_decoded_witness_count_sum. ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_start. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_start. ff_u_erc_fubini_zero_width_decoded_witness_count_sum = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_start * S ((S (0)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_terminal. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_terminal + S (n) = S ((S (z)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_terminal. ff_u_erc_fubini_zero_width_decoded_witness_count_sum = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_terminal * S ((S (z)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum) + (n))) /\ forall ff_i_erc_fubini_zero_width_decoded_witness_count_sum. (exists ff_lt_erc_fubini_zero_width_decoded_witness_count_sum_bound. ff_lt_erc_fubini_zero_width_decoded_witness_count_sum_bound + S ff_i_erc_fubini_zero_width_decoded_witness_count_sum = z) -> exists ff_a_erc_fubini_zero_width_decoded_witness_count_sum ff_r_erc_fubini_zero_width_decoded_witness_count_sum ff_s_erc_fubini_zero_width_decoded_witness_count_sum. ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_summand. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_summand + S (ff_a_erc_fubini_zero_width_decoded_witness_count_sum) = S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * erc_row_scale_fubini_zero_width_decoded_witness)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_summand. erc_row_code_fubini_zero_width_decoded_witness = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_summand * S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * erc_row_scale_fubini_zero_width_decoded_witness) + (ff_a_erc_fubini_zero_width_decoded_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_partial. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_partial + S (ff_r_erc_fubini_zero_width_decoded_witness_count_sum) = S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_partial. ff_u_erc_fubini_zero_width_decoded_witness_count_sum = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_partial * S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum) + (ff_r_erc_fubini_zero_width_decoded_witness_count_sum))) /\ ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_sum_successor. ff_h_erc_fubini_zero_width_decoded_witness_count_sum_successor + S (ff_s_erc_fubini_zero_width_decoded_witness_count_sum) = S ((S (S ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_sum_successor. ff_u_erc_fubini_zero_width_decoded_witness_count_sum = ff_q_erc_fubini_zero_width_decoded_witness_count_sum_successor * S ((S (S ff_i_erc_fubini_zero_width_decoded_witness_count_sum)) * ff_v_erc_fubini_zero_width_decoded_witness_count_sum) + (ff_s_erc_fubini_zero_width_decoded_witness_count_sum))) /\ ff_s_erc_fubini_zero_width_decoded_witness_count_sum = ff_r_erc_fubini_zero_width_decoded_witness_count_sum + ff_a_erc_fubini_zero_width_decoded_witness_count_sum)))))) /\ (forall ff_i_erc_fubini_zero_width_decoded_witness_count_bits. (exists ff_lt_erc_fubini_zero_width_decoded_witness_count_bits_bound. ff_lt_erc_fubini_zero_width_decoded_witness_count_bits_bound + S ff_i_erc_fubini_zero_width_decoded_witness_count_bits = z) -> exists ff_bit_erc_fubini_zero_width_decoded_witness_count_bits. ((((exists ff_h_erc_fubini_zero_width_decoded_witness_count_bits_decoded. ff_h_erc_fubini_zero_width_decoded_witness_count_bits_decoded + S (ff_bit_erc_fubini_zero_width_decoded_witness_count_bits) = S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_bits)) * erc_row_scale_fubini_zero_width_decoded_witness)) /\ exists ff_q_erc_fubini_zero_width_decoded_witness_count_bits_decoded. erc_row_code_fubini_zero_width_decoded_witness = ff_q_erc_fubini_zero_width_decoded_witness_count_bits_decoded * S ((S (ff_i_erc_fubini_zero_width_decoded_witness_count_bits)) * erc_row_scale_fubini_zero_width_decoded_witness) + (ff_bit_erc_fubini_zero_width_decoded_witness_count_bits))) /\ (ff_bit_erc_fubini_zero_width_decoded_witness_count_bits = 0 \/ ff_bit_erc_fubini_zero_width_decoded_witness_count_bits = 1))))))
  23. 0023specialize eisenstein_rectangle_decoded_row_count p
  24. 0024specialize eisenstein_rectangle_decoded_row_count q
  25. 0025specialize eisenstein_rectangle_decoded_row_count z
  26. 0026specialize eisenstein_rectangle_decoded_row_count bb
  27. 0027specialize eisenstein_rectangle_decoded_row_count bc
  28. 0028specialize eisenstein_rectangle_decoded_row_count l
  29. 0029specialize eisenstein_rectangle_decoded_row_count i
  30. 0030specialize eisenstein_rectangle_decoded_row_count n
  31. 0031apply eisenstein_rectangle_decoded_row_count
  32. 0032exact hprefix
  33. 0033exact hi
  34. 0034exact hn
  35. 0035cases hwitness
  36. 0036cases hwitness_witness
  37. 0037cases hwitness_witness_witness
  38. 0038have hnzero : n = 0
  39. 0039specialize bit_count_zero x2
  40. 0040specialize bit_count_zero x3
  41. 0041specialize bit_count_zero z
  42. 0042specialize bit_count_zero n
  43. 0043apply bit_count_zero
  44. 0044exact hz
  45. 0045exact hwitness_witness_witness_right
  46. 0046have hzero_entry : BetaAt(x,x1,i,z)
    Exact native replay linehave hzero_entry : ((exists ff_h_fubini_zero_width_repeat_entry. ff_h_fubini_zero_width_repeat_entry + S (z) = S ((S (i)) * x1)) /\ exists ff_q_fubini_zero_width_repeat_entry. x = ff_q_fubini_zero_width_repeat_entry * S ((S (i)) * x1) + (z))
  47. 0047specialize hrepeat_witness_witness i
  48. 0048apply hrepeat_witness_witness
  49. 0049exact hi
  50. 0050rewrite hz at hzero_entry
  51. 0051rewrite hz at hzero_entry
  52. 0052rewrite hnzero
  53. 0053rewrite hnzero
  54. 0054exact hzero_entry
  55. 0055have hrepeat_sum : Sum(x,x1,l,T)
    Exact native replay linehave hrepeat_sum : exists ff_u_fubini_zero_width_transport_sum ff_v_fubini_zero_width_transport_sum. ((((exists ff_h_fubini_zero_width_transport_sum_start. ff_h_fubini_zero_width_transport_sum_start + S (0) = S ((S (0)) * ff_v_fubini_zero_width_transport_sum)) /\ exists ff_q_fubini_zero_width_transport_sum_start. ff_u_fubini_zero_width_transport_sum = ff_q_fubini_zero_width_transport_sum_start * S ((S (0)) * ff_v_fubini_zero_width_transport_sum) + (0))) /\ ((((exists ff_h_fubini_zero_width_transport_sum_terminal. ff_h_fubini_zero_width_transport_sum_terminal + S (T) = S ((S (l)) * ff_v_fubini_zero_width_transport_sum)) /\ exists ff_q_fubini_zero_width_transport_sum_terminal. ff_u_fubini_zero_width_transport_sum = ff_q_fubini_zero_width_transport_sum_terminal * S ((S (l)) * ff_v_fubini_zero_width_transport_sum) + (T))) /\ forall ff_i_fubini_zero_width_transport_sum. (exists ff_lt_fubini_zero_width_transport_sum_bound. ff_lt_fubini_zero_width_transport_sum_bound + S ff_i_fubini_zero_width_transport_sum = l) -> exists ff_a_fubini_zero_width_transport_sum ff_r_fubini_zero_width_transport_sum ff_s_fubini_zero_width_transport_sum. ((((exists ff_h_fubini_zero_width_transport_sum_summand. ff_h_fubini_zero_width_transport_sum_summand + S (ff_a_fubini_zero_width_transport_sum) = S ((S (ff_i_fubini_zero_width_transport_sum)) * x1)) /\ exists ff_q_fubini_zero_width_transport_sum_summand. x = ff_q_fubini_zero_width_transport_sum_summand * S ((S (ff_i_fubini_zero_width_transport_sum)) * x1) + (ff_a_fubini_zero_width_transport_sum))) /\ ((((exists ff_h_fubini_zero_width_transport_sum_partial. ff_h_fubini_zero_width_transport_sum_partial + S (ff_r_fubini_zero_width_transport_sum) = S ((S (ff_i_fubini_zero_width_transport_sum)) * ff_v_fubini_zero_width_transport_sum)) /\ exists ff_q_fubini_zero_width_transport_sum_partial. ff_u_fubini_zero_width_transport_sum = ff_q_fubini_zero_width_transport_sum_partial * S ((S (ff_i_fubini_zero_width_transport_sum)) * ff_v_fubini_zero_width_transport_sum) + (ff_r_fubini_zero_width_transport_sum))) /\ ((((exists ff_h_fubini_zero_width_transport_sum_successor. ff_h_fubini_zero_width_transport_sum_successor + S (ff_s_fubini_zero_width_transport_sum) = S ((S (S ff_i_fubini_zero_width_transport_sum)) * ff_v_fubini_zero_width_transport_sum)) /\ exists ff_q_fubini_zero_width_transport_sum_successor. ff_u_fubini_zero_width_transport_sum = ff_q_fubini_zero_width_transport_sum_successor * S ((S (S ff_i_fubini_zero_width_transport_sum)) * ff_v_fubini_zero_width_transport_sum) + (ff_s_fubini_zero_width_transport_sum))) /\ ff_s_fubini_zero_width_transport_sum = ff_r_fubini_zero_width_transport_sum + ff_a_fubini_zero_width_transport_sum)))))
  56. 0056specialize beta_sum_transport_prefix bb
  57. 0057specialize beta_sum_transport_prefix bc
  58. 0058specialize beta_sum_transport_prefix x
  59. 0059specialize beta_sum_transport_prefix x1
  60. 0060specialize beta_sum_transport_prefix l
  61. 0061specialize beta_sum_transport_prefix T
  62. 0062apply beta_sum_transport_prefix
  63. 0063exact hsum
  64. 0064exact hpreserve
  65. 0065have hproduct : T = l * z
  66. 0066specialize beta_repeat_sum_exact x
  67. 0067specialize beta_repeat_sum_exact x1
  68. 0068specialize beta_repeat_sum_exact z
  69. 0069specialize beta_repeat_sum_exact l
  70. 0070specialize beta_repeat_sum_exact T
  71. 0071apply beta_repeat_sum_exact
  72. 0072exact hrepeat_witness_witness
  73. 0073exact hrepeat_sum
  74. 0074rewrite hz at hproduct
  75. 0075trans l * 0
  76. 0076exact hproduct
  77. 0077trans 0 * l
  78. 0078specialize mul_comm l
  79. 0079specialize mul_comm 0
  80. 0080exact mul_comm
  81. 0081specialize mul_zero_left l
  82. 0082exact mul_zero_left