SS0004

divisor_signed_table_construct

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

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

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.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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. 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

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