SS0004

divisor_signed_table_construct

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

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

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 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))))))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

SS0003 divisor_signed_table_from_components

Direct dependents

none

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

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.

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 exact 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