ZU0008

dirichlet_signed_unit_affine_solve

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

Given either actual signed unit, construct both x and its actual product y with r+y=e; no difference, product or solution witness is supplied.

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 r u e. (((u) = 2 \/ (u) = 1)) -> exists x y. ((exists sto_ap_affine_product sto_an_affine_product sto_bp_affine_product sto_bn_affine_product sto_cp_affine_product sto_cn_affine_product. (((((x) = 2 * (sto_ap_affine_product) /\ (sto_an_affine_product) = 0) \/ exists ge_signed_half_affine_productleft. (((x) = 2 * ge_signed_half_affine_productleft + 1 /\ (sto_ap_affine_product) = 0) /\ (sto_an_affine_product) = S ge_signed_half_affine_productleft))) /\ ((((((u) = 2 * (sto_bp_affine_product) /\ (sto_bn_affine_product) = 0) \/ exists ge_signed_half_affine_productright. (((u) = 2 * ge_signed_half_affine_productright + 1 /\ (sto_bp_affine_product) = 0) /\ (sto_bn_affine_product) = S ge_signed_half_affine_productright))) /\ ((((((y) = 2 * (sto_cp_affine_product) /\ (sto_cn_affine_product) = 0) \/ exists ge_signed_half_affine_productoutput. (((y) = 2 * ge_signed_half_affine_productoutput + 1 /\ (sto_cp_affine_product) = 0) /\ (sto_cn_affine_product) = S ge_signed_half_affine_productoutput))) /\ ((sto_ap_affine_product * sto_bp_affine_product + sto_an_affine_product * sto_bn_affine_product) + sto_cn_affine_product = (sto_ap_affine_product * sto_bn_affine_product + sto_an_affine_product * sto_bp_affine_product) + sto_cp_affine_product))))))) /\ (exists dsa_ap_affine_result dsa_an_affine_result dsa_bp_affine_result dsa_bn_affine_result dsa_cp_affine_result dsa_cn_affine_result. (((((r) = 2 * (dsa_ap_affine_result) /\ (dsa_an_affine_result) = 0) \/ exists ge_signed_half_affine_resultleft. (((r) = 2 * ge_signed_half_affine_resultleft + 1 /\ (dsa_ap_affine_result) = 0) /\ (dsa_an_affine_result) = S ge_signed_half_affine_resultleft))) /\ ((((((y) = 2 * (dsa_bp_affine_result) /\ (dsa_bn_affine_result) = 0) \/ exists ge_signed_half_affine_resultright. (((y) = 2 * ge_signed_half_affine_resultright + 1 /\ (dsa_bp_affine_result) = 0) /\ (dsa_bn_affine_result) = S ge_signed_half_affine_resultright))) /\ ((((((e) = 2 * (dsa_cp_affine_result) /\ (dsa_cn_affine_result) = 0) \/ exists ge_signed_half_affine_resultoutput. (((e) = 2 * ge_signed_half_affine_resultoutput + 1 /\ (dsa_cp_affine_result) = 0) /\ (dsa_cn_affine_result) = S ge_signed_half_affine_resultoutput))) /\ ((dsa_ap_affine_result + dsa_bp_affine_result) + dsa_cn_affine_result = (dsa_an_affine_result + dsa_bn_affine_result) + dsa_cp_affine_result))))))))

Constructive proof overview

Generated structural guide

Given either actual signed unit, construct both x and its actual product y with r+y=e; no difference, product or solution witness is supplied.

The unchanged tactic script uses 3 declared prerequisites and contains 24 exact native proof lines.

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

Proof neighborhood

Direct dependencies

ZU0005 dirichlet_signed_add_solve signed_mul_total Alpha theorem; checked-use authorized ZU0006 dirichlet_signed_unit_multiply_involution

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

24 script commands · 8 reading checkpoints · 2 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 (2)
dirichlet signed add solvedirichlet signed unit multiply involution

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro r
  2. L2
    intro u
  3. L3
    intro e
  4. L4
    intro hu
02Establish hyL5–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet signed add solve.

  1. L5
    have hy : ∃ y. SignedAdd(r,y,e)Definitions: SignedAdd
  2. L6
    specialize dirichlet_signed_add_solve (r)
  3. L7
    specialize dirichlet_signed_add_solve (e)
  4. L8
    apply dirichlet_signed_add_solve
03Separate the logical casesL9–9

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

  1. L9
    cases hy
04Establish hxL10–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed mul total.

  1. L10
    have hx : ∃ a. SignedMul(x,u,a)Definitions: SignedMul
  2. L11
    specialize signed_mul_total (x)
  3. L12
    specialize signed_mul_total (u)
  4. L13
    apply signed_mul_total
05Separate the logical casesL14–14

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

  1. L14
    cases hx
06Construct an explicit witnessL15–16

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

  1. L15
    exists x1
  2. L16
    exists x
07Separate the logical casesL17–17

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

  1. L17
    split
08Use earlier factsL18–24

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

  1. L18
    specialize dirichlet_signed_unit_multiply_involution (u)
  2. L19
    specialize dirichlet_signed_unit_multiply_involution (x)
  3. L20
    specialize dirichlet_signed_unit_multiply_involution (x1)
  4. L21
    apply dirichlet_signed_unit_multiply_involution
  5. L22
    exact hu
  6. L23
    exact hx_witness
  7. L24
    exact hy_witness

Library-wide reading audit

Original exact command ledger · 24 lines
  1. 0001intro r
  2. 0002intro u
  3. 0003intro e
  4. 0004intro hu
  5. 0005have hy : exists y. (exists dsa_ap_affine_addend dsa_an_affine_addend dsa_bp_affine_addend dsa_bn_affine_addend dsa_cp_affine_addend dsa_cn_affine_addend. (((((r) = 2 * (dsa_ap_affine_addend) /\ (dsa_an_affine_addend) = 0) \/ exists ge_signed_half_affine_addendleft. (((r) = 2 * ge_signed_half_affine_addendleft + 1 /\ (dsa_ap_affine_addend) = 0) /\ (dsa_an_affine_addend) = S ge_signed_half_affine_addendleft))) /\ ((((((y) = 2 * (dsa_bp_affine_addend) /\ (dsa_bn_affine_addend) = 0) \/ exists ge_signed_half_affine_addendright. (((y) = 2 * ge_signed_half_affine_addendright + 1 /\ (dsa_bp_affine_addend) = 0) /\ (dsa_bn_affine_addend) = S ge_signed_half_affine_addendright))) /\ ((((((e) = 2 * (dsa_cp_affine_addend) /\ (dsa_cn_affine_addend) = 0) \/ exists ge_signed_half_affine_addendoutput. (((e) = 2 * ge_signed_half_affine_addendoutput + 1 /\ (dsa_cp_affine_addend) = 0) /\ (dsa_cn_affine_addend) = S ge_signed_half_affine_addendoutput))) /\ ((dsa_ap_affine_addend + dsa_bp_affine_addend) + dsa_cn_affine_addend = (dsa_an_affine_addend + dsa_bn_affine_addend) + dsa_cp_affine_addend)))))))
  6. 0006specialize dirichlet_signed_add_solve (r)
  7. 0007specialize dirichlet_signed_add_solve (e)
  8. 0008apply dirichlet_signed_add_solve
  9. 0009cases hy
  10. 0010have hx : exists a. (exists sto_ap_affine_preimage sto_an_affine_preimage sto_bp_affine_preimage sto_bn_affine_preimage sto_cp_affine_preimage sto_cn_affine_preimage. (((((x) = 2 * (sto_ap_affine_preimage) /\ (sto_an_affine_preimage) = 0) \/ exists ge_signed_half_affine_preimageleft. (((x) = 2 * ge_signed_half_affine_preimageleft + 1 /\ (sto_ap_affine_preimage) = 0) /\ (sto_an_affine_preimage) = S ge_signed_half_affine_preimageleft))) /\ ((((((u) = 2 * (sto_bp_affine_preimage) /\ (sto_bn_affine_preimage) = 0) \/ exists ge_signed_half_affine_preimageright. (((u) = 2 * ge_signed_half_affine_preimageright + 1 /\ (sto_bp_affine_preimage) = 0) /\ (sto_bn_affine_preimage) = S ge_signed_half_affine_preimageright))) /\ ((((((a) = 2 * (sto_cp_affine_preimage) /\ (sto_cn_affine_preimage) = 0) \/ exists ge_signed_half_affine_preimageoutput. (((a) = 2 * ge_signed_half_affine_preimageoutput + 1 /\ (sto_cp_affine_preimage) = 0) /\ (sto_cn_affine_preimage) = S ge_signed_half_affine_preimageoutput))) /\ ((sto_ap_affine_preimage * sto_bp_affine_preimage + sto_an_affine_preimage * sto_bn_affine_preimage) + sto_cn_affine_preimage = (sto_ap_affine_preimage * sto_bn_affine_preimage + sto_an_affine_preimage * sto_bp_affine_preimage) + sto_cp_affine_preimage)))))))
  11. 0011specialize signed_mul_total (x)
  12. 0012specialize signed_mul_total (u)
  13. 0013apply signed_mul_total
  14. 0014cases hx
  15. 0015exists x1
  16. 0016exists x
  17. 0017split
  18. 0018specialize dirichlet_signed_unit_multiply_involution (u)
  19. 0019specialize dirichlet_signed_unit_multiply_involution (x)
  20. 0020specialize dirichlet_signed_unit_multiply_involution (x1)
  21. 0021apply dirichlet_signed_unit_multiply_involution
  22. 0022exact hu
  23. 0023exact hx_witness
  24. 0024exact hy_witness