DU000E

dirichlet_delta_right_last_entry

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

At the final divisor n, actually read delta(1), use the quotient n=n*1, and multiply F(n) by signed one.

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 expanded first-order arithmetic statement

forall N F E n a. (((exists dst_positive_code_last_deltatable dst_positive_scale_last_deltatable dst_negative_code_last_deltatable dst_negative_scale_last_deltatable. (((E) = (((((dst_positive_code_last_deltatable) + (dst_positive_scale_last_deltatable)) * S ((dst_positive_code_last_deltatable) + (dst_positive_scale_last_deltatable)) + ((dst_positive_scale_last_deltatable) + (dst_positive_scale_last_deltatable))) + (((dst_negative_code_last_deltatable) + (dst_negative_scale_last_deltatable)) * S ((dst_negative_code_last_deltatable) + (dst_negative_scale_last_deltatable)) + ((dst_negative_scale_last_deltatable) + (dst_negative_scale_last_deltatable)))) * S ((((dst_positive_code_last_deltatable) + (dst_positive_scale_last_deltatable)) * S ((dst_positive_code_last_deltatable) + (dst_positive_scale_last_deltatable)) + ((dst_positive_scale_last_deltatable) + (dst_positive_scale_last_deltatable))) + (((dst_negative_code_last_deltatable) + (dst_negative_scale_last_deltatable)) * S ((dst_negative_code_last_deltatable) + (dst_negative_scale_last_deltatable)) + ((dst_negative_scale_last_deltatable) + (dst_negative_scale_last_deltatable)))) + ((((dst_negative_code_last_deltatable) + (dst_negative_scale_last_deltatable)) * S ((dst_negative_code_last_deltatable) + (dst_negative_scale_last_deltatable)) + ((dst_negative_scale_last_deltatable) + (dst_negative_scale_last_deltatable))) + (((dst_negative_code_last_deltatable) + (dst_negative_scale_last_deltatable)) * S ((dst_negative_code_last_deltatable) + (dst_negative_scale_last_deltatable)) + ((dst_negative_scale_last_deltatable) + (dst_negative_scale_last_deltatable)))))) /\ (forall dst_index_last_deltatable. (exists pvs_le_gap_last_deltatabledomain. pvs_le_gap_last_deltatabledomain + (dst_index_last_deltatable) = (N)) -> exists dst_positive_last_deltatable dst_negative_last_deltatable dst_value_last_deltatable. ((((exists ff_h_pvs_last_deltatableentrypositive. ff_h_pvs_last_deltatableentrypositive + S (dst_positive_last_deltatable) = S ((S (dst_index_last_deltatable)) * dst_positive_scale_last_deltatable)) /\ exists ff_q_pvs_last_deltatableentrypositive. dst_positive_code_last_deltatable = ff_q_pvs_last_deltatableentrypositive * S ((S (dst_index_last_deltatable)) * dst_positive_scale_last_deltatable) + (dst_positive_last_deltatable))) /\ (((((exists ff_h_pvs_last_deltatableentrynegative. ff_h_pvs_last_deltatableentrynegative + S (dst_negative_last_deltatable) = S ((S (dst_index_last_deltatable)) * dst_negative_scale_last_deltatable)) /\ exists ff_q_pvs_last_deltatableentrynegative. dst_negative_code_last_deltatable = ff_q_pvs_last_deltatableentrynegative * S ((S (dst_index_last_deltatable)) * dst_negative_scale_last_deltatable) + (dst_negative_last_deltatable))) /\ (exists ge_balance_positive_last_deltatableentryvalue ge_balance_negative_last_deltatableentryvalue. (((((dst_value_last_deltatable) = 2 * (ge_balance_positive_last_deltatableentryvalue) /\ (ge_balance_negative_last_deltatableentryvalue) = 0) \/ exists ge_signed_half_last_deltatableentryvaluedecode. (((dst_value_last_deltatable) = 2 * ge_signed_half_last_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_last_deltatableentryvalue) = 0) /\ (ge_balance_negative_last_deltatableentryvalue) = S ge_signed_half_last_deltatableentryvaluedecode))) /\ ((dst_positive_last_deltatable) + ge_balance_negative_last_deltatableentryvalue = (dst_negative_last_deltatable) + ge_balance_positive_last_deltatableentryvalue))))))))) /\ (forall du_index_last_delta du_value_last_delta. ~(du_index_last_delta=0) -> (exists pvs_le_gap_last_deltabound. pvs_le_gap_last_deltabound + (du_index_last_delta) = (N)) -> (exists dst_positive_code_last_deltaentry dst_positive_scale_last_deltaentry dst_negative_code_last_deltaentry dst_negative_scale_last_deltaentry dst_positive_last_deltaentry dst_negative_last_deltaentry. (((E) = (((((dst_positive_code_last_deltaentry) + (dst_positive_scale_last_deltaentry)) * S ((dst_positive_code_last_deltaentry) + (dst_positive_scale_last_deltaentry)) + ((dst_positive_scale_last_deltaentry) + (dst_positive_scale_last_deltaentry))) + (((dst_negative_code_last_deltaentry) + (dst_negative_scale_last_deltaentry)) * S ((dst_negative_code_last_deltaentry) + (dst_negative_scale_last_deltaentry)) + ((dst_negative_scale_last_deltaentry) + (dst_negative_scale_last_deltaentry)))) * S ((((dst_positive_code_last_deltaentry) + (dst_positive_scale_last_deltaentry)) * S ((dst_positive_code_last_deltaentry) + (dst_positive_scale_last_deltaentry)) + ((dst_positive_scale_last_deltaentry) + (dst_positive_scale_last_deltaentry))) + (((dst_negative_code_last_deltaentry) + (dst_negative_scale_last_deltaentry)) * S ((dst_negative_code_last_deltaentry) + (dst_negative_scale_last_deltaentry)) + ((dst_negative_scale_last_deltaentry) + (dst_negative_scale_last_deltaentry)))) + ((((dst_negative_code_last_deltaentry) + (dst_negative_scale_last_deltaentry)) * S ((dst_negative_code_last_deltaentry) + (dst_negative_scale_last_deltaentry)) + ((dst_negative_scale_last_deltaentry) + (dst_negative_scale_last_deltaentry))) + (((dst_negative_code_last_deltaentry) + (dst_negative_scale_last_deltaentry)) * S ((dst_negative_code_last_deltaentry) + (dst_negative_scale_last_deltaentry)) + ((dst_negative_scale_last_deltaentry) + (dst_negative_scale_last_deltaentry)))))) /\ (((((exists ff_h_pvs_last_deltaentrypositive. ff_h_pvs_last_deltaentrypositive + S (dst_positive_last_deltaentry) = S ((S (du_index_last_delta)) * dst_positive_scale_last_deltaentry)) /\ exists ff_q_pvs_last_deltaentrypositive. dst_positive_code_last_deltaentry = ff_q_pvs_last_deltaentrypositive * S ((S (du_index_last_delta)) * dst_positive_scale_last_deltaentry) + (dst_positive_last_deltaentry))) /\ (((((exists ff_h_pvs_last_deltaentrynegative. ff_h_pvs_last_deltaentrynegative + S (dst_negative_last_deltaentry) = S ((S (du_index_last_delta)) * dst_negative_scale_last_deltaentry)) /\ exists ff_q_pvs_last_deltaentrynegative. dst_negative_code_last_deltaentry = ff_q_pvs_last_deltaentrynegative * S ((S (du_index_last_delta)) * dst_negative_scale_last_deltaentry) + (dst_negative_last_deltaentry))) /\ (exists ge_balance_positive_last_deltaentryvalue ge_balance_negative_last_deltaentryvalue. (((((du_value_last_delta) = 2 * (ge_balance_positive_last_deltaentryvalue) /\ (ge_balance_negative_last_deltaentryvalue) = 0) \/ exists ge_signed_half_last_deltaentryvaluedecode. (((du_value_last_delta) = 2 * ge_signed_half_last_deltaentryvaluedecode + 1 /\ (ge_balance_positive_last_deltaentryvalue) = 0) /\ (ge_balance_negative_last_deltaentryvalue) = S ge_signed_half_last_deltaentryvaluedecode))) /\ ((dst_positive_last_deltaentry) + ge_balance_negative_last_deltaentryvalue = (dst_negative_last_deltaentry) + ge_balance_positive_last_deltaentryvalue))))))))) -> ((((du_index_last_delta)=1 -> (du_value_last_delta)=2) /\ (~((du_index_last_delta)=1) -> (du_value_last_delta)=0)))))) -> ~(n=0) -> (exists pvs_le_gap_last_domain. pvs_le_gap_last_domain + (n) = (N)) -> (exists dst_positive_code_last_source dst_positive_scale_last_source dst_negative_code_last_source dst_negative_scale_last_source dst_positive_last_source dst_negative_last_source. (((F) = (((((dst_positive_code_last_source) + (dst_positive_scale_last_source)) * S ((dst_positive_code_last_source) + (dst_positive_scale_last_source)) + ((dst_positive_scale_last_source) + (dst_positive_scale_last_source))) + (((dst_negative_code_last_source) + (dst_negative_scale_last_source)) * S ((dst_negative_code_last_source) + (dst_negative_scale_last_source)) + ((dst_negative_scale_last_source) + (dst_negative_scale_last_source)))) * S ((((dst_positive_code_last_source) + (dst_positive_scale_last_source)) * S ((dst_positive_code_last_source) + (dst_positive_scale_last_source)) + ((dst_positive_scale_last_source) + (dst_positive_scale_last_source))) + (((dst_negative_code_last_source) + (dst_negative_scale_last_source)) * S ((dst_negative_code_last_source) + (dst_negative_scale_last_source)) + ((dst_negative_scale_last_source) + (dst_negative_scale_last_source)))) + ((((dst_negative_code_last_source) + (dst_negative_scale_last_source)) * S ((dst_negative_code_last_source) + (dst_negative_scale_last_source)) + ((dst_negative_scale_last_source) + (dst_negative_scale_last_source))) + (((dst_negative_code_last_source) + (dst_negative_scale_last_source)) * S ((dst_negative_code_last_source) + (dst_negative_scale_last_source)) + ((dst_negative_scale_last_source) + (dst_negative_scale_last_source)))))) /\ (((((exists ff_h_pvs_last_sourcepositive. ff_h_pvs_last_sourcepositive + S (dst_positive_last_source) = S ((S (n)) * dst_positive_scale_last_source)) /\ exists ff_q_pvs_last_sourcepositive. dst_positive_code_last_source = ff_q_pvs_last_sourcepositive * S ((S (n)) * dst_positive_scale_last_source) + (dst_positive_last_source))) /\ (((((exists ff_h_pvs_last_sourcenegative. ff_h_pvs_last_sourcenegative + S (dst_negative_last_source) = S ((S (n)) * dst_negative_scale_last_source)) /\ exists ff_q_pvs_last_sourcenegative. dst_negative_code_last_source = ff_q_pvs_last_sourcenegative * S ((S (n)) * dst_negative_scale_last_source) + (dst_negative_last_source))) /\ (exists ge_balance_positive_last_sourcevalue ge_balance_negative_last_sourcevalue. (((((a) = 2 * (ge_balance_positive_last_sourcevalue) /\ (ge_balance_negative_last_sourcevalue) = 0) \/ exists ge_signed_half_last_sourcevaluedecode. (((a) = 2 * ge_signed_half_last_sourcevaluedecode + 1 /\ (ge_balance_positive_last_sourcevalue) = 0) /\ (ge_balance_negative_last_sourcevalue) = S ge_signed_half_last_sourcevaluedecode))) /\ ((dst_positive_last_source) + ge_balance_negative_last_sourcevalue = (dst_negative_last_source) + ge_balance_positive_last_sourcevalue))))))))) -> ((((~((n)=0)) /\ (exists dc_quotient_last_result dc_left_last_result dc_right_last_result. (((n)=(n)*dc_quotient_last_result) /\ (((exists dst_positive_code_last_resultleft dst_positive_scale_last_resultleft dst_negative_code_last_resultleft dst_negative_scale_last_resultleft dst_positive_last_resultleft dst_negative_last_resultleft. (((F) = (((((dst_positive_code_last_resultleft) + (dst_positive_scale_last_resultleft)) * S ((dst_positive_code_last_resultleft) + (dst_positive_scale_last_resultleft)) + ((dst_positive_scale_last_resultleft) + (dst_positive_scale_last_resultleft))) + (((dst_negative_code_last_resultleft) + (dst_negative_scale_last_resultleft)) * S ((dst_negative_code_last_resultleft) + (dst_negative_scale_last_resultleft)) + ((dst_negative_scale_last_resultleft) + (dst_negative_scale_last_resultleft)))) * S ((((dst_positive_code_last_resultleft) + (dst_positive_scale_last_resultleft)) * S ((dst_positive_code_last_resultleft) + (dst_positive_scale_last_resultleft)) + ((dst_positive_scale_last_resultleft) + (dst_positive_scale_last_resultleft))) + (((dst_negative_code_last_resultleft) + (dst_negative_scale_last_resultleft)) * S ((dst_negative_code_last_resultleft) + (dst_negative_scale_last_resultleft)) + ((dst_negative_scale_last_resultleft) + (dst_negative_scale_last_resultleft)))) + ((((dst_negative_code_last_resultleft) + (dst_negative_scale_last_resultleft)) * S ((dst_negative_code_last_resultleft) + (dst_negative_scale_last_resultleft)) + ((dst_negative_scale_last_resultleft) + (dst_negative_scale_last_resultleft))) + (((dst_negative_code_last_resultleft) + (dst_negative_scale_last_resultleft)) * S ((dst_negative_code_last_resultleft) + (dst_negative_scale_last_resultleft)) + ((dst_negative_scale_last_resultleft) + (dst_negative_scale_last_resultleft)))))) /\ (((((exists ff_h_pvs_last_resultleftpositive. ff_h_pvs_last_resultleftpositive + S (dst_positive_last_resultleft) = S ((S (n)) * dst_positive_scale_last_resultleft)) /\ exists ff_q_pvs_last_resultleftpositive. dst_positive_code_last_resultleft = ff_q_pvs_last_resultleftpositive * S ((S (n)) * dst_positive_scale_last_resultleft) + (dst_positive_last_resultleft))) /\ (((((exists ff_h_pvs_last_resultleftnegative. ff_h_pvs_last_resultleftnegative + S (dst_negative_last_resultleft) = S ((S (n)) * dst_negative_scale_last_resultleft)) /\ exists ff_q_pvs_last_resultleftnegative. dst_negative_code_last_resultleft = ff_q_pvs_last_resultleftnegative * S ((S (n)) * dst_negative_scale_last_resultleft) + (dst_negative_last_resultleft))) /\ (exists ge_balance_positive_last_resultleftvalue ge_balance_negative_last_resultleftvalue. (((((dc_left_last_result) = 2 * (ge_balance_positive_last_resultleftvalue) /\ (ge_balance_negative_last_resultleftvalue) = 0) \/ exists ge_signed_half_last_resultleftvaluedecode. (((dc_left_last_result) = 2 * ge_signed_half_last_resultleftvaluedecode + 1 /\ (ge_balance_positive_last_resultleftvalue) = 0) /\ (ge_balance_negative_last_resultleftvalue) = S ge_signed_half_last_resultleftvaluedecode))) /\ ((dst_positive_last_resultleft) + ge_balance_negative_last_resultleftvalue = (dst_negative_last_resultleft) + ge_balance_positive_last_resultleftvalue))))))))) /\ (((exists dst_positive_code_last_resultright dst_positive_scale_last_resultright dst_negative_code_last_resultright dst_negative_scale_last_resultright dst_positive_last_resultright dst_negative_last_resultright. (((E) = (((((dst_positive_code_last_resultright) + (dst_positive_scale_last_resultright)) * S ((dst_positive_code_last_resultright) + (dst_positive_scale_last_resultright)) + ((dst_positive_scale_last_resultright) + (dst_positive_scale_last_resultright))) + (((dst_negative_code_last_resultright) + (dst_negative_scale_last_resultright)) * S ((dst_negative_code_last_resultright) + (dst_negative_scale_last_resultright)) + ((dst_negative_scale_last_resultright) + (dst_negative_scale_last_resultright)))) * S ((((dst_positive_code_last_resultright) + (dst_positive_scale_last_resultright)) * S ((dst_positive_code_last_resultright) + (dst_positive_scale_last_resultright)) + ((dst_positive_scale_last_resultright) + (dst_positive_scale_last_resultright))) + (((dst_negative_code_last_resultright) + (dst_negative_scale_last_resultright)) * S ((dst_negative_code_last_resultright) + (dst_negative_scale_last_resultright)) + ((dst_negative_scale_last_resultright) + (dst_negative_scale_last_resultright)))) + ((((dst_negative_code_last_resultright) + (dst_negative_scale_last_resultright)) * S ((dst_negative_code_last_resultright) + (dst_negative_scale_last_resultright)) + ((dst_negative_scale_last_resultright) + (dst_negative_scale_last_resultright))) + (((dst_negative_code_last_resultright) + (dst_negative_scale_last_resultright)) * S ((dst_negative_code_last_resultright) + (dst_negative_scale_last_resultright)) + ((dst_negative_scale_last_resultright) + (dst_negative_scale_last_resultright)))))) /\ (((((exists ff_h_pvs_last_resultrightpositive. ff_h_pvs_last_resultrightpositive + S (dst_positive_last_resultright) = S ((S (dc_quotient_last_result)) * dst_positive_scale_last_resultright)) /\ exists ff_q_pvs_last_resultrightpositive. dst_positive_code_last_resultright = ff_q_pvs_last_resultrightpositive * S ((S (dc_quotient_last_result)) * dst_positive_scale_last_resultright) + (dst_positive_last_resultright))) /\ (((((exists ff_h_pvs_last_resultrightnegative. ff_h_pvs_last_resultrightnegative + S (dst_negative_last_resultright) = S ((S (dc_quotient_last_result)) * dst_negative_scale_last_resultright)) /\ exists ff_q_pvs_last_resultrightnegative. dst_negative_code_last_resultright = ff_q_pvs_last_resultrightnegative * S ((S (dc_quotient_last_result)) * dst_negative_scale_last_resultright) + (dst_negative_last_resultright))) /\ (exists ge_balance_positive_last_resultrightvalue ge_balance_negative_last_resultrightvalue. (((((dc_right_last_result) = 2 * (ge_balance_positive_last_resultrightvalue) /\ (ge_balance_negative_last_resultrightvalue) = 0) \/ exists ge_signed_half_last_resultrightvaluedecode. (((dc_right_last_result) = 2 * ge_signed_half_last_resultrightvaluedecode + 1 /\ (ge_balance_positive_last_resultrightvalue) = 0) /\ (ge_balance_negative_last_resultrightvalue) = S ge_signed_half_last_resultrightvaluedecode))) /\ ((dst_positive_last_resultright) + ge_balance_negative_last_resultrightvalue = (dst_negative_last_resultright) + ge_balance_positive_last_resultrightvalue))))))))) /\ (exists sto_ap_last_resultproduct sto_an_last_resultproduct sto_bp_last_resultproduct sto_bn_last_resultproduct sto_cp_last_resultproduct sto_cn_last_resultproduct. (((((dc_left_last_result) = 2 * (sto_ap_last_resultproduct) /\ (sto_an_last_resultproduct) = 0) \/ exists ge_signed_half_last_resultproductleft. (((dc_left_last_result) = 2 * ge_signed_half_last_resultproductleft + 1 /\ (sto_ap_last_resultproduct) = 0) /\ (sto_an_last_resultproduct) = S ge_signed_half_last_resultproductleft))) /\ ((((((dc_right_last_result) = 2 * (sto_bp_last_resultproduct) /\ (sto_bn_last_resultproduct) = 0) \/ exists ge_signed_half_last_resultproductright. (((dc_right_last_result) = 2 * ge_signed_half_last_resultproductright + 1 /\ (sto_bp_last_resultproduct) = 0) /\ (sto_bn_last_resultproduct) = S ge_signed_half_last_resultproductright))) /\ ((((((a) = 2 * (sto_cp_last_resultproduct) /\ (sto_cn_last_resultproduct) = 0) \/ exists ge_signed_half_last_resultproductoutput. (((a) = 2 * ge_signed_half_last_resultproductoutput + 1 /\ (sto_cp_last_resultproduct) = 0) /\ (sto_cn_last_resultproduct) = S ge_signed_half_last_resultproductoutput))) /\ ((sto_ap_last_resultproduct * sto_bp_last_resultproduct + sto_an_last_resultproduct * sto_bn_last_resultproduct) + sto_cn_last_resultproduct = (sto_ap_last_resultproduct * sto_bn_last_resultproduct + sto_an_last_resultproduct * sto_bp_last_resultproduct) + sto_cp_last_resultproduct))))))))))))))) \/ ((((n)=0 \/ ~(exists pvs_factor_last_resultnondivisor. (n) = (n) * pvs_factor_last_resultnondivisor)) /\ ((a)=0))))

Constructive proof overview

Generated structural guide

At the final divisor n, actually read delta(1), use the quotient n=n*1, and multiply F(n) by signed one.

The unchanged tactic script uses 7 declared prerequisites and contains 53 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

le_trans Stable theorem; checked-use authorized one_le_of_ne_zero Stable theorem; checked-use authorized divisor_signed_table_lookup Alpha theorem; checked-use authorized DU0002 dirichlet_kronecker_delta_table_one_value dirichlet_convolution_entry_from_quotient Alpha theorem; checked-use authorized mul_one Stable theorem; checked-use authorized signed_mul_one_right Alpha theorem; checked-use authorized

Direct dependents

DU000F dirichlet_delta_right_sum_value

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

53 script commands · 9 reading checkpoints · 3 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.

Named ingredients (1)
dirichlet kronecker delta table one value

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro E
  4. L4
    intro n
  5. L5
    intro a
  6. L6
    intro hd
  7. L7
    intro hn
  8. L8
    intro hb
  9. L9
    intro ha
02Separate the logical casesL10–10

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

  1. L10
    cases hd
03Establish hboundL11–19

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

  1. L11
    have hbound : exists pvs_le_gap_last_one_bound. pvs_le_gap_last_one_bound + (1) = (N)
  2. L12
    specialize le_trans (1)
  3. L13
    specialize le_trans (n)
  4. L14
    specialize le_trans (N)
  5. L15
    apply le_trans
  6. L16
    specialize one_le_of_ne_zero (n)
  7. L17
    apply one_le_of_ne_zero
  8. L18
    exact hn
  9. L19
    exact hb
04Establish hxL20–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.

  1. L20
    have hx : ∃ x. ArithAt(E,1,x)Definitions: ArithAt
  2. L21
    specialize divisor_signed_table_lookup (N)
  3. L22
    specialize divisor_signed_table_lookup (E)
  4. L23
    specialize divisor_signed_table_lookup (1)
  5. L24
    apply divisor_signed_table_lookup
  6. L25
    exact hd_left
  7. L26
    exact hbound
05Separate the logical casesL27–27

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

  1. L27
    cases hx
06Establish hvL28–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet kronecker delta table one value.

  1. L28
    have hv : x=2
  2. L29
    specialize dirichlet_kronecker_delta_table_one_value (N)
  3. L30
    specialize dirichlet_kronecker_delta_table_one_value (E)
  4. L31
    specialize dirichlet_kronecker_delta_table_one_value (x)
  5. L32
    apply dirichlet_kronecker_delta_table_one_value
  6. L33
    exact hd
  7. L34
    exact hbound
  8. L35
    exact hx_witness
  9. L36
    rewrite hv at hx_witness
  10. L37
    rewrite hv at hx_witness
07Use earlier factsL38–47

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

  1. L38
    specialize dirichlet_convolution_entry_from_quotient (F)
  2. L39
    specialize dirichlet_convolution_entry_from_quotient (E)
  3. L40
    specialize dirichlet_convolution_entry_from_quotient (n)
  4. L41
    specialize dirichlet_convolution_entry_from_quotient (n)
  5. L42
    specialize dirichlet_convolution_entry_from_quotient (1)
  6. L43
    specialize dirichlet_convolution_entry_from_quotient (a)
  7. L44
    specialize dirichlet_convolution_entry_from_quotient (2)
  8. L45
    specialize dirichlet_convolution_entry_from_quotient (a)
  9. L46
    apply dirichlet_convolution_entry_from_quotient
  10. L47
    exact hn
08Calculate and transport equalitiesL48–48

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

  1. L48
    symm
09Use earlier factsL49–53

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

  1. L49
    apply mul_one
  2. L50
    exact ha
  3. L51
    exact hx_witness
  4. L52
    specialize signed_mul_one_right (a)
  5. L53
    apply signed_mul_one_right

Library-wide reading audit

Original exact command ledger · 53 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro E
  4. 0004intro n
  5. 0005intro a
  6. 0006intro hd
  7. 0007intro hn
  8. 0008intro hb
  9. 0009intro ha
  10. 0010cases hd
  11. 0011have hbound : exists pvs_le_gap_last_one_bound. pvs_le_gap_last_one_bound + (1) = (N)
  12. 0012specialize le_trans (1)
  13. 0013specialize le_trans (n)
  14. 0014specialize le_trans (N)
  15. 0015apply le_trans
  16. 0016specialize one_le_of_ne_zero (n)
  17. 0017apply one_le_of_ne_zero
  18. 0018exact hn
  19. 0019exact hb
  20. 0020have hx : exists x. (exists dst_positive_code_last_one_lookup dst_positive_scale_last_one_lookup dst_negative_code_last_one_lookup dst_negative_scale_last_one_lookup dst_positive_last_one_lookup dst_negative_last_one_lookup. (((E) = (((((dst_positive_code_last_one_lookup) + (dst_positive_scale_last_one_lookup)) * S ((dst_positive_code_last_one_lookup) + (dst_positive_scale_last_one_lookup)) + ((dst_positive_scale_last_one_lookup) + (dst_positive_scale_last_one_lookup))) + (((dst_negative_code_last_one_lookup) + (dst_negative_scale_last_one_lookup)) * S ((dst_negative_code_last_one_lookup) + (dst_negative_scale_last_one_lookup)) + ((dst_negative_scale_last_one_lookup) + (dst_negative_scale_last_one_lookup)))) * S ((((dst_positive_code_last_one_lookup) + (dst_positive_scale_last_one_lookup)) * S ((dst_positive_code_last_one_lookup) + (dst_positive_scale_last_one_lookup)) + ((dst_positive_scale_last_one_lookup) + (dst_positive_scale_last_one_lookup))) + (((dst_negative_code_last_one_lookup) + (dst_negative_scale_last_one_lookup)) * S ((dst_negative_code_last_one_lookup) + (dst_negative_scale_last_one_lookup)) + ((dst_negative_scale_last_one_lookup) + (dst_negative_scale_last_one_lookup)))) + ((((dst_negative_code_last_one_lookup) + (dst_negative_scale_last_one_lookup)) * S ((dst_negative_code_last_one_lookup) + (dst_negative_scale_last_one_lookup)) + ((dst_negative_scale_last_one_lookup) + (dst_negative_scale_last_one_lookup))) + (((dst_negative_code_last_one_lookup) + (dst_negative_scale_last_one_lookup)) * S ((dst_negative_code_last_one_lookup) + (dst_negative_scale_last_one_lookup)) + ((dst_negative_scale_last_one_lookup) + (dst_negative_scale_last_one_lookup)))))) /\ (((((exists ff_h_pvs_last_one_lookuppositive. ff_h_pvs_last_one_lookuppositive + S (dst_positive_last_one_lookup) = S ((S (1)) * dst_positive_scale_last_one_lookup)) /\ exists ff_q_pvs_last_one_lookuppositive. dst_positive_code_last_one_lookup = ff_q_pvs_last_one_lookuppositive * S ((S (1)) * dst_positive_scale_last_one_lookup) + (dst_positive_last_one_lookup))) /\ (((((exists ff_h_pvs_last_one_lookupnegative. ff_h_pvs_last_one_lookupnegative + S (dst_negative_last_one_lookup) = S ((S (1)) * dst_negative_scale_last_one_lookup)) /\ exists ff_q_pvs_last_one_lookupnegative. dst_negative_code_last_one_lookup = ff_q_pvs_last_one_lookupnegative * S ((S (1)) * dst_negative_scale_last_one_lookup) + (dst_negative_last_one_lookup))) /\ (exists ge_balance_positive_last_one_lookupvalue ge_balance_negative_last_one_lookupvalue. (((((x) = 2 * (ge_balance_positive_last_one_lookupvalue) /\ (ge_balance_negative_last_one_lookupvalue) = 0) \/ exists ge_signed_half_last_one_lookupvaluedecode. (((x) = 2 * ge_signed_half_last_one_lookupvaluedecode + 1 /\ (ge_balance_positive_last_one_lookupvalue) = 0) /\ (ge_balance_negative_last_one_lookupvalue) = S ge_signed_half_last_one_lookupvaluedecode))) /\ ((dst_positive_last_one_lookup) + ge_balance_negative_last_one_lookupvalue = (dst_negative_last_one_lookup) + ge_balance_positive_last_one_lookupvalue)))))))))
  21. 0021specialize divisor_signed_table_lookup (N)
  22. 0022specialize divisor_signed_table_lookup (E)
  23. 0023specialize divisor_signed_table_lookup (1)
  24. 0024apply divisor_signed_table_lookup
  25. 0025exact hd_left
  26. 0026exact hbound
  27. 0027cases hx
  28. 0028have hv : x=2
  29. 0029specialize dirichlet_kronecker_delta_table_one_value (N)
  30. 0030specialize dirichlet_kronecker_delta_table_one_value (E)
  31. 0031specialize dirichlet_kronecker_delta_table_one_value (x)
  32. 0032apply dirichlet_kronecker_delta_table_one_value
  33. 0033exact hd
  34. 0034exact hbound
  35. 0035exact hx_witness
  36. 0036rewrite hv at hx_witness
  37. 0037rewrite hv at hx_witness
  38. 0038specialize dirichlet_convolution_entry_from_quotient (F)
  39. 0039specialize dirichlet_convolution_entry_from_quotient (E)
  40. 0040specialize dirichlet_convolution_entry_from_quotient (n)
  41. 0041specialize dirichlet_convolution_entry_from_quotient (n)
  42. 0042specialize dirichlet_convolution_entry_from_quotient (1)
  43. 0043specialize dirichlet_convolution_entry_from_quotient (a)
  44. 0044specialize dirichlet_convolution_entry_from_quotient (2)
  45. 0045specialize dirichlet_convolution_entry_from_quotient (a)
  46. 0046apply dirichlet_convolution_entry_from_quotient
  47. 0047exact hn
  48. 0048symm
  49. 0049apply mul_one
  50. 0050exact ha
  51. 0051exact hx_witness
  52. 0052specialize signed_mul_one_right (a)
  53. 0053apply signed_mul_one_right