SS0002

divisor_signed_table_at_to_components

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Every lookup unpacks against any proved representation of its exact table code, with actual component witnesses.

Exact expanded first-order arithmetic statement

forall F pb pc nb nc i z. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> (exists dst_positive_code_unpack_entry dst_positive_scale_unpack_entry dst_negative_code_unpack_entry dst_negative_scale_unpack_entry dst_positive_unpack_entry dst_negative_unpack_entry. (((F) = (((((dst_positive_code_unpack_entry) + (dst_positive_scale_unpack_entry)) * S ((dst_positive_code_unpack_entry) + (dst_positive_scale_unpack_entry)) + ((dst_positive_scale_unpack_entry) + (dst_positive_scale_unpack_entry))) + (((dst_negative_code_unpack_entry) + (dst_negative_scale_unpack_entry)) * S ((dst_negative_code_unpack_entry) + (dst_negative_scale_unpack_entry)) + ((dst_negative_scale_unpack_entry) + (dst_negative_scale_unpack_entry)))) * S ((((dst_positive_code_unpack_entry) + (dst_positive_scale_unpack_entry)) * S ((dst_positive_code_unpack_entry) + (dst_positive_scale_unpack_entry)) + ((dst_positive_scale_unpack_entry) + (dst_positive_scale_unpack_entry))) + (((dst_negative_code_unpack_entry) + (dst_negative_scale_unpack_entry)) * S ((dst_negative_code_unpack_entry) + (dst_negative_scale_unpack_entry)) + ((dst_negative_scale_unpack_entry) + (dst_negative_scale_unpack_entry)))) + ((((dst_negative_code_unpack_entry) + (dst_negative_scale_unpack_entry)) * S ((dst_negative_code_unpack_entry) + (dst_negative_scale_unpack_entry)) + ((dst_negative_scale_unpack_entry) + (dst_negative_scale_unpack_entry))) + (((dst_negative_code_unpack_entry) + (dst_negative_scale_unpack_entry)) * S ((dst_negative_code_unpack_entry) + (dst_negative_scale_unpack_entry)) + ((dst_negative_scale_unpack_entry) + (dst_negative_scale_unpack_entry)))))) /\ (((((exists ff_h_pvs_unpack_entrypositive. ff_h_pvs_unpack_entrypositive + S (dst_positive_unpack_entry) = S ((S (i)) * dst_positive_scale_unpack_entry)) /\ exists ff_q_pvs_unpack_entrypositive. dst_positive_code_unpack_entry = ff_q_pvs_unpack_entrypositive * S ((S (i)) * dst_positive_scale_unpack_entry) + (dst_positive_unpack_entry))) /\ (((((exists ff_h_pvs_unpack_entrynegative. ff_h_pvs_unpack_entrynegative + S (dst_negative_unpack_entry) = S ((S (i)) * dst_negative_scale_unpack_entry)) /\ exists ff_q_pvs_unpack_entrynegative. dst_negative_code_unpack_entry = ff_q_pvs_unpack_entrynegative * S ((S (i)) * dst_negative_scale_unpack_entry) + (dst_negative_unpack_entry))) /\ (exists ge_balance_positive_unpack_entryvalue ge_balance_negative_unpack_entryvalue. (((((z) = 2 * (ge_balance_positive_unpack_entryvalue) /\ (ge_balance_negative_unpack_entryvalue) = 0) \/ exists ge_signed_half_unpack_entryvaluedecode. (((z) = 2 * ge_signed_half_unpack_entryvaluedecode + 1 /\ (ge_balance_positive_unpack_entryvalue) = 0) /\ (ge_balance_negative_unpack_entryvalue) = S ge_signed_half_unpack_entryvaluedecode))) /\ ((dst_positive_unpack_entry) + ge_balance_negative_unpack_entryvalue = (dst_negative_unpack_entry) + ge_balance_positive_unpack_entryvalue))))))))) -> exists p n. (((((exists ff_h_pvs_unpack_resultpositive. ff_h_pvs_unpack_resultpositive + S (p) = S ((S (i)) * pc)) /\ exists ff_q_pvs_unpack_resultpositive. pb = ff_q_pvs_unpack_resultpositive * S ((S (i)) * pc) + (p))) /\ (((((exists ff_h_pvs_unpack_resultnegative. ff_h_pvs_unpack_resultnegative + S (n) = S ((S (i)) * nc)) /\ exists ff_q_pvs_unpack_resultnegative. nb = ff_q_pvs_unpack_resultnegative * S ((S (i)) * nc) + (n))) /\ (exists ge_balance_positive_unpack_resultvalue ge_balance_negative_unpack_resultvalue. (((((z) = 2 * (ge_balance_positive_unpack_resultvalue) /\ (ge_balance_negative_unpack_resultvalue) = 0) \/ exists ge_signed_half_unpack_resultvaluedecode. (((z) = 2 * ge_signed_half_unpack_resultvaluedecode + 1 /\ (ge_balance_positive_unpack_resultvalue) = 0) /\ (ge_balance_negative_unpack_resultvalue) = S ge_signed_half_unpack_resultvaluedecode))) /\ ((p) + ge_balance_negative_unpack_resultvalue = (n) + ge_balance_positive_unpack_resultvalue)))))))

Constructive proof overview

Generated structural guide

Every lookup unpacks against any proved representation of its exact table code, with actual component witnesses.

The unchanged tactic script uses 1 declared prerequisite and contains 47 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

matrix_minor_four_code_components_injective Alpha theorem; checked-use authorized

Direct dependents

SS0007 divisor_signed_table_at_functional SS0016 divisor_signed_sum_successor_intro SS001A divisor_signed_table_reindex_from_components

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

47 script commands · 12 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.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro F
  2. L2
    intro pb
  3. L3
    intro pc
  4. L4
    intro nb
  5. L5
    intro nc
  6. L6
    intro i
  7. L7
    intro z
  8. L8
    intro hrep
  9. L9
    intro hentry
02Separate the logical casesL10–18

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

  1. L10
    cases hentry
  2. L11
    cases hentry_witness
  3. L12
    cases hentry_witness_witness
  4. L13
    cases hentry_witness_witness_witness
  5. L14
    cases hentry_witness_witness_witness_witness
  6. L15
    cases hentry_witness_witness_witness_witness_witness
  7. L16
    cases hentry_witness_witness_witness_witness_witness_witness
  8. L17
    cases hentry_witness_witness_witness_witness_witness_witness_right
  9. L18
    cases hentry_witness_witness_witness_witness_witness_witness_right_right
03Establish heqL19–28

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

  1. L19
    have heq : ((x = pb) /\ (((x1 = pc) /\ (((x2 = nb) /\ (x3 = nc))))))
  2. L20
    specialize matrix_minor_four_code_components_injective (F)
  3. L21
    specialize matrix_minor_four_code_components_injective (x)
  4. L22
    specialize matrix_minor_four_code_components_injective (x1)
  5. L23
    specialize matrix_minor_four_code_components_injective (x2)
  6. L24
    specialize matrix_minor_four_code_components_injective (x3)
  7. L25
    specialize matrix_minor_four_code_components_injective (pb)
  8. L26
    specialize matrix_minor_four_code_components_injective (pc)
  9. L27
    specialize matrix_minor_four_code_components_injective (nb)
  10. L28
    specialize matrix_minor_four_code_components_injective (nc)
04Use earlier factsL29–31

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

  1. L29
    apply matrix_minor_four_code_components_injective
  2. L30
    exact hentry_witness_witness_witness_witness_witness_witness_left
  3. L31
    exact hrep
05Separate the logical casesL32–34

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

  1. L32
    cases heq
  2. L33
    cases heq_right
  3. L34
    cases heq_right_right
06Construct an explicit witnessL35–36

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

  1. L35
    exists x4
  2. L36
    exists x5
07Separate the logical casesL37–37

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

  1. L37
    split
08Calculate and transport equalitiesL38–40

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

  1. L38
    rewrite heq_left at hentry_witness_witness_witness_witness_witness_witness_right_left
  2. L39
    rewrite heq_right_left at hentry_witness_witness_witness_witness_witness_witness_right_left
  3. L40
    rewrite heq_right_left at hentry_witness_witness_witness_witness_witness_witness_right_left
09Use earlier factsL41–41

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

  1. L41
    exact hentry_witness_witness_witness_witness_witness_witness_right_left
10Separate the logical casesL42–42

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

  1. L42
    split
11Calculate and transport equalitiesL43–45

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

  1. L43
    rewrite heq_right_right_left at hentry_witness_witness_witness_witness_witness_witness_right_right_left
  2. L44
    rewrite heq_right_right_right at hentry_witness_witness_witness_witness_witness_witness_right_right_left
  3. L45
    rewrite heq_right_right_right at hentry_witness_witness_witness_witness_witness_witness_right_right_left
12Use earlier factsL46–47

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

  1. L46
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_left
  2. L47
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 47 lines
  1. 0001intro F
  2. 0002intro pb
  3. 0003intro pc
  4. 0004intro nb
  5. 0005intro nc
  6. 0006intro i
  7. 0007intro z
  8. 0008intro hrep
  9. 0009intro hentry
  10. 0010cases hentry
  11. 0011cases hentry_witness
  12. 0012cases hentry_witness_witness
  13. 0013cases hentry_witness_witness_witness
  14. 0014cases hentry_witness_witness_witness_witness
  15. 0015cases hentry_witness_witness_witness_witness_witness
  16. 0016cases hentry_witness_witness_witness_witness_witness_witness
  17. 0017cases hentry_witness_witness_witness_witness_witness_witness_right
  18. 0018cases hentry_witness_witness_witness_witness_witness_witness_right_right
  19. 0019have heq : ((x = pb) /\ (((x1 = pc) /\ (((x2 = nb) /\ (x3 = nc))))))
  20. 0020specialize matrix_minor_four_code_components_injective (F)
  21. 0021specialize matrix_minor_four_code_components_injective (x)
  22. 0022specialize matrix_minor_four_code_components_injective (x1)
  23. 0023specialize matrix_minor_four_code_components_injective (x2)
  24. 0024specialize matrix_minor_four_code_components_injective (x3)
  25. 0025specialize matrix_minor_four_code_components_injective (pb)
  26. 0026specialize matrix_minor_four_code_components_injective (pc)
  27. 0027specialize matrix_minor_four_code_components_injective (nb)
  28. 0028specialize matrix_minor_four_code_components_injective (nc)
  29. 0029apply matrix_minor_four_code_components_injective
  30. 0030exact hentry_witness_witness_witness_witness_witness_witness_left
  31. 0031exact hrep
  32. 0032cases heq
  33. 0033cases heq_right
  34. 0034cases heq_right_right
  35. 0035exists x4
  36. 0036exists x5
  37. 0037split
  38. 0038rewrite heq_left at hentry_witness_witness_witness_witness_witness_witness_right_left
  39. 0039rewrite heq_right_left at hentry_witness_witness_witness_witness_witness_witness_right_left
  40. 0040rewrite heq_right_left at hentry_witness_witness_witness_witness_witness_witness_right_left
  41. 0041exact hentry_witness_witness_witness_witness_witness_witness_right_left
  42. 0042split
  43. 0043rewrite heq_right_right_left at hentry_witness_witness_witness_witness_witness_witness_right_right_left
  44. 0044rewrite heq_right_right_right at hentry_witness_witness_witness_witness_witness_witness_right_right_left
  45. 0045rewrite heq_right_right_right at hentry_witness_witness_witness_witness_witness_witness_right_right_left
  46. 0046exact hentry_witness_witness_witness_witness_witness_witness_right_right_left
  47. 0047exact hentry_witness_witness_witness_witness_witness_witness_right_right_right