MX0039

signed_support_incidence_entry_functional

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

The actual incidence value is unique, independent of witnesses and component representations.

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 A r s i j z w. (exists ssr_entry_value_functional_first ssr_entry_image_functional_first. ((exists dst_positive_code_functional_firstsource dst_positive_scale_functional_firstsource dst_negative_code_functional_firstsource dst_negative_scale_functional_firstsource dst_positive_functional_firstsource dst_negative_functional_firstsource. (((A) = (((((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) * S ((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) + ((dst_positive_scale_functional_firstsource) + (dst_positive_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))) * S ((((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) * S ((dst_positive_code_functional_firstsource) + (dst_positive_scale_functional_firstsource)) + ((dst_positive_scale_functional_firstsource) + (dst_positive_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))) + ((((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource))) + (((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) * S ((dst_negative_code_functional_firstsource) + (dst_negative_scale_functional_firstsource)) + ((dst_negative_scale_functional_firstsource) + (dst_negative_scale_functional_firstsource)))))) /\ (((((exists ff_h_pvs_functional_firstsourcepositive. ff_h_pvs_functional_firstsourcepositive + S (dst_positive_functional_firstsource) = S ((S (i)) * dst_positive_scale_functional_firstsource)) /\ exists ff_q_pvs_functional_firstsourcepositive. dst_positive_code_functional_firstsource = ff_q_pvs_functional_firstsourcepositive * S ((S (i)) * dst_positive_scale_functional_firstsource) + (dst_positive_functional_firstsource))) /\ (((((exists ff_h_pvs_functional_firstsourcenegative. ff_h_pvs_functional_firstsourcenegative + S (dst_negative_functional_firstsource) = S ((S (i)) * dst_negative_scale_functional_firstsource)) /\ exists ff_q_pvs_functional_firstsourcenegative. dst_negative_code_functional_firstsource = ff_q_pvs_functional_firstsourcenegative * S ((S (i)) * dst_negative_scale_functional_firstsource) + (dst_negative_functional_firstsource))) /\ (exists ge_balance_positive_functional_firstsourcevalue ge_balance_negative_functional_firstsourcevalue. (((((ssr_entry_value_functional_first) = 2 * (ge_balance_positive_functional_firstsourcevalue) /\ (ge_balance_negative_functional_firstsourcevalue) = 0) \/ exists ge_signed_half_functional_firstsourcevaluedecode. (((ssr_entry_value_functional_first) = 2 * ge_signed_half_functional_firstsourcevaluedecode + 1 /\ (ge_balance_positive_functional_firstsourcevalue) = 0) /\ (ge_balance_negative_functional_firstsourcevalue) = S ge_signed_half_functional_firstsourcevaluedecode))) /\ ((dst_positive_functional_firstsource) + ge_balance_negative_functional_firstsourcevalue = (dst_negative_functional_firstsource) + ge_balance_positive_functional_firstsourcevalue))))))))) /\ (((((exists ff_h_pvs_functional_firstmap. ff_h_pvs_functional_firstmap + S (ssr_entry_image_functional_first) = S ((S (i)) * s)) /\ exists ff_q_pvs_functional_firstmap. r = ff_q_pvs_functional_firstmap * S ((S (i)) * s) + (ssr_entry_image_functional_first))) /\ (((((j)=(ssr_entry_image_functional_first)) /\ ((z)=(ssr_entry_value_functional_first)))) \/ (((~((j)=(ssr_entry_image_functional_first))) /\ ((z)=0)))))))) -> (exists ssr_entry_value_functional_second ssr_entry_image_functional_second. ((exists dst_positive_code_functional_secondsource dst_positive_scale_functional_secondsource dst_negative_code_functional_secondsource dst_negative_scale_functional_secondsource dst_positive_functional_secondsource dst_negative_functional_secondsource. (((A) = (((((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) * S ((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) + ((dst_positive_scale_functional_secondsource) + (dst_positive_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))) * S ((((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) * S ((dst_positive_code_functional_secondsource) + (dst_positive_scale_functional_secondsource)) + ((dst_positive_scale_functional_secondsource) + (dst_positive_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))) + ((((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource))) + (((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) * S ((dst_negative_code_functional_secondsource) + (dst_negative_scale_functional_secondsource)) + ((dst_negative_scale_functional_secondsource) + (dst_negative_scale_functional_secondsource)))))) /\ (((((exists ff_h_pvs_functional_secondsourcepositive. ff_h_pvs_functional_secondsourcepositive + S (dst_positive_functional_secondsource) = S ((S (i)) * dst_positive_scale_functional_secondsource)) /\ exists ff_q_pvs_functional_secondsourcepositive. dst_positive_code_functional_secondsource = ff_q_pvs_functional_secondsourcepositive * S ((S (i)) * dst_positive_scale_functional_secondsource) + (dst_positive_functional_secondsource))) /\ (((((exists ff_h_pvs_functional_secondsourcenegative. ff_h_pvs_functional_secondsourcenegative + S (dst_negative_functional_secondsource) = S ((S (i)) * dst_negative_scale_functional_secondsource)) /\ exists ff_q_pvs_functional_secondsourcenegative. dst_negative_code_functional_secondsource = ff_q_pvs_functional_secondsourcenegative * S ((S (i)) * dst_negative_scale_functional_secondsource) + (dst_negative_functional_secondsource))) /\ (exists ge_balance_positive_functional_secondsourcevalue ge_balance_negative_functional_secondsourcevalue. (((((ssr_entry_value_functional_second) = 2 * (ge_balance_positive_functional_secondsourcevalue) /\ (ge_balance_negative_functional_secondsourcevalue) = 0) \/ exists ge_signed_half_functional_secondsourcevaluedecode. (((ssr_entry_value_functional_second) = 2 * ge_signed_half_functional_secondsourcevaluedecode + 1 /\ (ge_balance_positive_functional_secondsourcevalue) = 0) /\ (ge_balance_negative_functional_secondsourcevalue) = S ge_signed_half_functional_secondsourcevaluedecode))) /\ ((dst_positive_functional_secondsource) + ge_balance_negative_functional_secondsourcevalue = (dst_negative_functional_secondsource) + ge_balance_positive_functional_secondsourcevalue))))))))) /\ (((((exists ff_h_pvs_functional_secondmap. ff_h_pvs_functional_secondmap + S (ssr_entry_image_functional_second) = S ((S (i)) * s)) /\ exists ff_q_pvs_functional_secondmap. r = ff_q_pvs_functional_secondmap * S ((S (i)) * s) + (ssr_entry_image_functional_second))) /\ (((((j)=(ssr_entry_image_functional_second)) /\ ((w)=(ssr_entry_value_functional_second)))) \/ (((~((j)=(ssr_entry_image_functional_second))) /\ ((w)=0)))))))) -> z=w

Constructive proof overview

Generated structural guide

The actual incidence value is unique, independent of witnesses and component representations.

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

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

Proof neighborhood

Direct dependencies

MX0038 signed_support_incidence_entry_decode

Direct dependents

MX0046 signed_support_incidence_row_sum_value MX0047 signed_support_incidence_column_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

49 script commands · 18 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.

Named ingredients (1)
signed support incidence entry decode
01Fix variables and assumptionsL1–9

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

  1. L1
    intro A
  2. L2
    intro r
  3. L3
    intro s
  4. L4
    intro i
  5. L5
    intro j
  6. L6
    intro z
  7. L7
    intro w
  8. L8
    intro hz
  9. L9
    intro hw
02Separate the logical casesL10–13

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

  1. L10
    cases hz
  2. L11
    cases hz_witness
  3. L12
    cases hz_witness_witness
  4. L13
    cases hz_witness_witness_right
03Establish hdL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed support incidence entry decode.

  1. L14
    have hd : ((((j)=(x1)) /\ ((w)=(x)))) \/ (((~((j)=(x1))) /\ ((w)=0)))
  2. L15
    specialize signed_support_incidence_entry_decode (A)
  3. L16
    specialize signed_support_incidence_entry_decode (r)
  4. L17
    specialize signed_support_incidence_entry_decode (s)
  5. L18
    specialize signed_support_incidence_entry_decode (i)
  6. L19
    specialize signed_support_incidence_entry_decode (j)
  7. L20
    specialize signed_support_incidence_entry_decode (x)
  8. L21
    specialize signed_support_incidence_entry_decode (x1)
  9. L22
    specialize signed_support_incidence_entry_decode (w)
  10. L23
    apply signed_support_incidence_entry_decode
04Use earlier factsL24–26

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

  1. L24
    exact hz_witness_witness_left
  2. L25
    exact hz_witness_witness_right_left
  3. L26
    exact hw
05Separate the logical casesL27–30

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

  1. L27
    cases hz_witness_witness_right_right
  2. L28
    cases hz_witness_witness_right_right_left
  3. L29
    cases hd
  4. L30
    cases hd_left
06Calculate and transport equalitiesL31–31

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

  1. L31
    trans x
07Use earlier factsL32–32

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

  1. L32
    exact hz_witness_witness_right_right_left_right
08Calculate and transport equalitiesL33–33

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

  1. L33
    symm
09Use earlier factsL34–34

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

  1. L34
    exact hd_left_right
10Separate the logical casesL35–36

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

  1. L35
    cases hd_right
  2. L36
    exfalso
11Use earlier factsL37–38

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

  1. L37
    apply hd_right_left
  2. L38
    exact hz_witness_witness_right_right_left_left
12Separate the logical casesL39–42

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

  1. L39
    cases hz_witness_witness_right_right_right
  2. L40
    cases hd
  3. L41
    cases hd_left
  4. L42
    exfalso
13Use earlier factsL43–44

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

  1. L43
    apply hz_witness_witness_right_right_right_left
  2. L44
    exact hd_left_left
14Separate the logical casesL45–45

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

  1. L45
    cases hd_right
15Calculate and transport equalitiesL46–46

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

  1. L46
    trans 0
16Use earlier factsL47–47

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

  1. L47
    exact hz_witness_witness_right_right_right_right
17Calculate and transport equalitiesL48–48

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

  1. L48
    symm
18Use earlier factsL49–49

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

  1. L49
    exact hd_right_right

Library-wide reading audit

Original exact command ledger · 49 lines
  1. 0001intro A
  2. 0002intro r
  3. 0003intro s
  4. 0004intro i
  5. 0005intro j
  6. 0006intro z
  7. 0007intro w
  8. 0008intro hz
  9. 0009intro hw
  10. 0010cases hz
  11. 0011cases hz_witness
  12. 0012cases hz_witness_witness
  13. 0013cases hz_witness_witness_right
  14. 0014have hd : ((((j)=(x1)) /\ ((w)=(x)))) \/ (((~((j)=(x1))) /\ ((w)=0)))
  15. 0015specialize signed_support_incidence_entry_decode (A)
  16. 0016specialize signed_support_incidence_entry_decode (r)
  17. 0017specialize signed_support_incidence_entry_decode (s)
  18. 0018specialize signed_support_incidence_entry_decode (i)
  19. 0019specialize signed_support_incidence_entry_decode (j)
  20. 0020specialize signed_support_incidence_entry_decode (x)
  21. 0021specialize signed_support_incidence_entry_decode (x1)
  22. 0022specialize signed_support_incidence_entry_decode (w)
  23. 0023apply signed_support_incidence_entry_decode
  24. 0024exact hz_witness_witness_left
  25. 0025exact hz_witness_witness_right_left
  26. 0026exact hw
  27. 0027cases hz_witness_witness_right_right
  28. 0028cases hz_witness_witness_right_right_left
  29. 0029cases hd
  30. 0030cases hd_left
  31. 0031trans x
  32. 0032exact hz_witness_witness_right_right_left_right
  33. 0033symm
  34. 0034exact hd_left_right
  35. 0035cases hd_right
  36. 0036exfalso
  37. 0037apply hd_right_left
  38. 0038exact hz_witness_witness_right_right_left_left
  39. 0039cases hz_witness_witness_right_right_right
  40. 0040cases hd
  41. 0041cases hd_left
  42. 0042exfalso
  43. 0043apply hz_witness_witness_right_right_right_left
  44. 0044exact hd_left_left
  45. 0045cases hd_right
  46. 0046trans 0
  47. 0047exact hz_witness_witness_right_right_right_right
  48. 0048symm
  49. 0049exact hd_right_right