SS0004

divisor_signed_table_construct

Natural pairing constructs the table code itself, not merely an opaque validity witness.

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.

These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.

Exact theorem in conservative defined notation

∀ N. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∃ F. ArithTable(N,F) ∧ MatrixMinorFourCode(F,pb,pc,nb,nc)

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

Definition DAG

MatrixMinorFourCode(z,up,us,un,ut) · 1ArithTable(N,F) · 1

Actual proof prerequisites

divisor_signed_table_from_components
Original expanded first-order statement 
forall N pb pc nb nc. exists F. (exists dst_positive_code_constructed dst_positive_scale_constructed dst_negative_code_constructed dst_negative_scale_constructed. (((F) = (((((dst_positive_code_constructed) + (dst_positive_scale_constructed)) * S ((dst_positive_code_constructed) + (dst_positive_scale_constructed)) + ((dst_positive_scale_constructed) + (dst_positive_scale_constructed))) + (((dst_negative_code_constructed) + (dst_negative_scale_constructed)) * S ((dst_negative_code_constructed) + (dst_negative_scale_constructed)) + ((dst_negative_scale_constructed) + (dst_negative_scale_constructed)))) * S ((((dst_positive_code_constructed) + (dst_positive_scale_constructed)) * S ((dst_positive_code_constructed) + (dst_positive_scale_constructed)) + ((dst_positive_scale_constructed) + (dst_positive_scale_constructed))) + (((dst_negative_code_constructed) + (dst_negative_scale_constructed)) * S ((dst_negative_code_constructed) + (dst_negative_scale_constructed)) + ((dst_negative_scale_constructed) + (dst_negative_scale_constructed)))) + ((((dst_negative_code_constructed) + (dst_negative_scale_constructed)) * S ((dst_negative_code_constructed) + (dst_negative_scale_constructed)) + ((dst_negative_scale_constructed) + (dst_negative_scale_constructed))) + (((dst_negative_code_constructed) + (dst_negative_scale_constructed)) * S ((dst_negative_code_constructed) + (dst_negative_scale_constructed)) + ((dst_negative_scale_constructed) + (dst_negative_scale_constructed)))))) /\ (forall dst_index_constructed. (exists pvs_le_gap_constructeddomain. pvs_le_gap_constructeddomain + (dst_index_constructed) = (N)) -> exists dst_positive_constructed dst_negative_constructed dst_value_constructed. ((((exists ff_h_pvs_constructedentrypositive. ff_h_pvs_constructedentrypositive + S (dst_positive_constructed) = S ((S (dst_index_constructed)) * dst_positive_scale_constructed)) /\ exists ff_q_pvs_constructedentrypositive. dst_positive_code_constructed = ff_q_pvs_constructedentrypositive * S ((S (dst_index_constructed)) * dst_positive_scale_constructed) + (dst_positive_constructed))) /\ (((((exists ff_h_pvs_constructedentrynegative. ff_h_pvs_constructedentrynegative + S (dst_negative_constructed) = S ((S (dst_index_constructed)) * dst_negative_scale_constructed)) /\ exists ff_q_pvs_constructedentrynegative. dst_negative_code_constructed = ff_q_pvs_constructedentrynegative * S ((S (dst_index_constructed)) * dst_negative_scale_constructed) + (dst_negative_constructed))) /\ (exists ge_balance_positive_constructedentryvalue ge_balance_negative_constructedentryvalue. (((((dst_value_constructed) = 2 * (ge_balance_positive_constructedentryvalue) /\ (ge_balance_negative_constructedentryvalue) = 0) \/ exists ge_signed_half_constructedentryvaluedecode. (((dst_value_constructed) = 2 * ge_signed_half_constructedentryvaluedecode + 1 /\ (ge_balance_positive_constructedentryvalue) = 0) /\ (ge_balance_negative_constructedentryvalue) = S ge_signed_half_constructedentryvaluedecode))) /\ ((dst_positive_constructed) + ge_balance_negative_constructedentryvalue = (dst_negative_constructed) + ge_balance_positive_constructedentryvalue))))))))) /\ ((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))))))

Complete tactic proof in conservative notation

All 16 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

16 script commands · 5 reading checkpoints · 0 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)
divisor signed table from components
01Fix variables and assumptionsL1–5

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

  1. L1
    intro N
  2. L2
    intro pb
  3. L3
    intro pc
  4. L4
    intro nb
  5. L5
    intro nc
02Construct an explicit witnessL6–6

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

  1. L6
    exists ((((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))))
03Separate the logical casesL7–7

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

  1. L7
    split
04Use earlier factsL8–14

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

  1. L8
    specialize divisor_signed_table_from_components (N)
  2. L9
    specialize divisor_signed_table_from_components (((((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)))))
  3. L10
    specialize divisor_signed_table_from_components (pb)
  4. L11
    specialize divisor_signed_table_from_components (pc)
  5. L12
    specialize divisor_signed_table_from_components (nb)
  6. L13
    specialize divisor_signed_table_from_components (nc)
  7. L14
    apply divisor_signed_table_from_components
05Calculate and transport equalitiesL15–16

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

  1. L15
    refl
  2. L16
    refl

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro N
  2. 0002intro pb
  3. 0003intro pc
  4. 0004intro nb
  5. 0005intro nc
  6. 0006exists ((((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))))
  7. 0007split
  8. 0008specialize divisor_signed_table_from_components (N)
  9. 0009specialize divisor_signed_table_from_components (((((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)))))
  10. 0010specialize divisor_signed_table_from_components (pb)
  11. 0011specialize divisor_signed_table_from_components (pc)
  12. 0012specialize divisor_signed_table_from_components (nb)
  13. 0013specialize divisor_signed_table_from_components (nc)
  14. 0014apply divisor_signed_table_from_components
  15. 0015refl
  16. 0016refl