DV0005

arithmetic_signed_table_singleton

The base table contains an arbitrary prescribed signed value at index zero, with actual beta and packing witnesses.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

A genuine divisor mask has S n entries, indexed zero through n, and forces its zeroth entry to zero regardless of F(0). Möbius values remain positive-domain only. This family constructs divisor sums and Möbius tables; cancellation and the full G007 endpoint are separately proved later in the same release.

Exact theorem in conservative defined notation

∀ z. ∃ F. ArithTable(0,F) ∧ ArithAt(F,0,z)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ArithTable(N,F) · 1ArithAt(F,i,z) · 1ArithExtend(F,G,l,z) · 1

Actual proof prerequisites

arithmetic_signed_table_extend_atdivisor_signed_table_from_components · checked external prerequisite
Original expanded first-order statement 
forall z. exists F. (exists dst_positive_code_singleton_valid dst_positive_scale_singleton_valid dst_negative_code_singleton_valid dst_negative_scale_singleton_valid. (((F) = (((((dst_positive_code_singleton_valid) + (dst_positive_scale_singleton_valid)) * S ((dst_positive_code_singleton_valid) + (dst_positive_scale_singleton_valid)) + ((dst_positive_scale_singleton_valid) + (dst_positive_scale_singleton_valid))) + (((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) * S ((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) + ((dst_negative_scale_singleton_valid) + (dst_negative_scale_singleton_valid)))) * S ((((dst_positive_code_singleton_valid) + (dst_positive_scale_singleton_valid)) * S ((dst_positive_code_singleton_valid) + (dst_positive_scale_singleton_valid)) + ((dst_positive_scale_singleton_valid) + (dst_positive_scale_singleton_valid))) + (((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) * S ((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) + ((dst_negative_scale_singleton_valid) + (dst_negative_scale_singleton_valid)))) + ((((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) * S ((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) + ((dst_negative_scale_singleton_valid) + (dst_negative_scale_singleton_valid))) + (((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) * S ((dst_negative_code_singleton_valid) + (dst_negative_scale_singleton_valid)) + ((dst_negative_scale_singleton_valid) + (dst_negative_scale_singleton_valid)))))) /\ (forall dst_index_singleton_valid. (exists pvs_le_gap_singleton_validdomain. pvs_le_gap_singleton_validdomain + (dst_index_singleton_valid) = (0)) -> exists dst_positive_singleton_valid dst_negative_singleton_valid dst_value_singleton_valid. ((((exists ff_h_pvs_singleton_validentrypositive. ff_h_pvs_singleton_validentrypositive + S (dst_positive_singleton_valid) = S ((S (dst_index_singleton_valid)) * dst_positive_scale_singleton_valid)) /\ exists ff_q_pvs_singleton_validentrypositive. dst_positive_code_singleton_valid = ff_q_pvs_singleton_validentrypositive * S ((S (dst_index_singleton_valid)) * dst_positive_scale_singleton_valid) + (dst_positive_singleton_valid))) /\ (((((exists ff_h_pvs_singleton_validentrynegative. ff_h_pvs_singleton_validentrynegative + S (dst_negative_singleton_valid) = S ((S (dst_index_singleton_valid)) * dst_negative_scale_singleton_valid)) /\ exists ff_q_pvs_singleton_validentrynegative. dst_negative_code_singleton_valid = ff_q_pvs_singleton_validentrynegative * S ((S (dst_index_singleton_valid)) * dst_negative_scale_singleton_valid) + (dst_negative_singleton_valid))) /\ (exists ge_balance_positive_singleton_validentryvalue ge_balance_negative_singleton_validentryvalue. (((((dst_value_singleton_valid) = 2 * (ge_balance_positive_singleton_validentryvalue) /\ (ge_balance_negative_singleton_validentryvalue) = 0) \/ exists ge_signed_half_singleton_validentryvaluedecode. (((dst_value_singleton_valid) = 2 * ge_signed_half_singleton_validentryvaluedecode + 1 /\ (ge_balance_positive_singleton_validentryvalue) = 0) /\ (ge_balance_negative_singleton_validentryvalue) = S ge_signed_half_singleton_validentryvaluedecode))) /\ ((dst_positive_singleton_valid) + ge_balance_negative_singleton_validentryvalue = (dst_negative_singleton_valid) + ge_balance_positive_singleton_validentryvalue))))))))) /\ (exists dst_positive_code_singleton_value dst_positive_scale_singleton_value dst_negative_code_singleton_value dst_negative_scale_singleton_value dst_positive_singleton_value dst_negative_singleton_value. (((F) = (((((dst_positive_code_singleton_value) + (dst_positive_scale_singleton_value)) * S ((dst_positive_code_singleton_value) + (dst_positive_scale_singleton_value)) + ((dst_positive_scale_singleton_value) + (dst_positive_scale_singleton_value))) + (((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) * S ((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) + ((dst_negative_scale_singleton_value) + (dst_negative_scale_singleton_value)))) * S ((((dst_positive_code_singleton_value) + (dst_positive_scale_singleton_value)) * S ((dst_positive_code_singleton_value) + (dst_positive_scale_singleton_value)) + ((dst_positive_scale_singleton_value) + (dst_positive_scale_singleton_value))) + (((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) * S ((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) + ((dst_negative_scale_singleton_value) + (dst_negative_scale_singleton_value)))) + ((((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) * S ((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) + ((dst_negative_scale_singleton_value) + (dst_negative_scale_singleton_value))) + (((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) * S ((dst_negative_code_singleton_value) + (dst_negative_scale_singleton_value)) + ((dst_negative_scale_singleton_value) + (dst_negative_scale_singleton_value)))))) /\ (((((exists ff_h_pvs_singleton_valuepositive. ff_h_pvs_singleton_valuepositive + S (dst_positive_singleton_value) = S ((S (0)) * dst_positive_scale_singleton_value)) /\ exists ff_q_pvs_singleton_valuepositive. dst_positive_code_singleton_value = ff_q_pvs_singleton_valuepositive * S ((S (0)) * dst_positive_scale_singleton_value) + (dst_positive_singleton_value))) /\ (((((exists ff_h_pvs_singleton_valuenegative. ff_h_pvs_singleton_valuenegative + S (dst_negative_singleton_value) = S ((S (0)) * dst_negative_scale_singleton_value)) /\ exists ff_q_pvs_singleton_valuenegative. dst_negative_code_singleton_value = ff_q_pvs_singleton_valuenegative * S ((S (0)) * dst_negative_scale_singleton_value) + (dst_negative_singleton_value))) /\ (exists ge_balance_positive_singleton_valuevalue ge_balance_negative_singleton_valuevalue. (((((z) = 2 * (ge_balance_positive_singleton_valuevalue) /\ (ge_balance_negative_singleton_valuevalue) = 0) \/ exists ge_signed_half_singleton_valuevaluedecode. (((z) = 2 * ge_signed_half_singleton_valuevaluedecode + 1 /\ (ge_balance_positive_singleton_valuevalue) = 0) /\ (ge_balance_negative_singleton_valuevalue) = S ge_signed_half_singleton_valuevaluedecode))) /\ ((dst_positive_singleton_value) + ge_balance_negative_singleton_valuevalue = (dst_negative_singleton_value) + ge_balance_positive_singleton_valuevalue)))))))))

Complete tactic proof in conservative notation

All 22 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

22 script commands · 8 reading checkpoints · 1 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 (1)
arithmetic signed table extend at
01Fix variables and assumptionsL1–1

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

  1. L1
    intro z
02Establish heL2–11

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

  1. L2
    have he : ∃ G. ArithExtend(((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))) · S ((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))) + ((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))),G,0,z)Definitions: ArithExtend(((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))) · S ((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))) + ((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))),G,0,z)Original native command in the exact edition
  2. L3
    specialize arithmetic_signed_table_extend_at (0)
  3. L4
    specialize arithmetic_signed_table_extend_at (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  4. L5
    specialize arithmetic_signed_table_extend_at (0)
  5. L6
    specialize arithmetic_signed_table_extend_at (z)
  6. L7
    apply arithmetic_signed_table_extend_at
  7. L8
    specialize divisor_signed_table_from_components (0)
  8. L9
    specialize divisor_signed_table_from_components (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  9. L10
    specialize divisor_signed_table_from_components (0)
  10. L11
    specialize divisor_signed_table_from_components (0)
03Use earlier factsL12–14

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

  1. L12
    specialize divisor_signed_table_from_components (0)
  2. L13
    specialize divisor_signed_table_from_components (0)
  3. L14
    apply divisor_signed_table_from_components
04Calculate and transport equalitiesL15–15

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

  1. L15
    refl
05Separate the logical casesL16–18

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

  1. L16
    cases he
  2. L17
    cases he_witness
  3. L18
    cases he_witness_right
06Construct an explicit witnessL19–19

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

  1. L19
    exists x
07Separate the logical casesL20–20

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

  1. L20
    split
08Use earlier factsL21–22

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

  1. L21
    exact he_witness_left
  2. L22
    exact he_witness_right_right

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro z
  2. 0002have he : ∃ G. ArithExtend(((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))) · S ((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))) + ((0 + 0) · S (0 + 0) + (0 + 0) + ((0 + 0) · S (0 + 0) + (0 + 0))),G,0,z)
  3. 0003specialize arithmetic_signed_table_extend_at (0)
  4. 0004specialize arithmetic_signed_table_extend_at (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  5. 0005specialize arithmetic_signed_table_extend_at (0)
  6. 0006specialize arithmetic_signed_table_extend_at (z)
  7. 0007apply arithmetic_signed_table_extend_at
  8. 0008specialize divisor_signed_table_from_components (0)
  9. 0009specialize divisor_signed_table_from_components (((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))))
  10. 0010specialize divisor_signed_table_from_components (0)
  11. 0011specialize divisor_signed_table_from_components (0)
  12. 0012specialize divisor_signed_table_from_components (0)
  13. 0013specialize divisor_signed_table_from_components (0)
  14. 0014apply divisor_signed_table_from_components
  15. 0015refl
  16. 0016cases he
  17. 0017cases he_witness
  18. 0018cases he_witness_right
  19. 0019exists x
  20. 0020split
  21. 0021exact he_witness_left
  22. 0022exact he_witness_right_right