ZU0003

dirichlet_signed_unit_inverse_iff

The finite signed-unit predicate is equivalent to existence of an actual signed multiplicative inverse, not defined by an inverse oracle.

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.

Canonical signed +1 is code 2 and -1 is code 1. The two-case unit graph does not assume an inverse or cancellation law: its actual product characterization and affine existence and uniqueness are proved. These scalar lemmas support the separately checked finite inverse criterion; full G009 remains broader.

Exact theorem in conservative defined notation

∀ u. ((∃ x. SignedMul(u,x,2)) → SignedUnit(u)) ∧ (SignedUnit(u) → ∃ x. SignedMul(u,x,2))

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

Definition DAG

SignedMul(a,b,c) · 2SignedUnit(u) · 2

Actual proof prerequisites

dirichlet_signed_unit_product_classificationdirichlet_signed_unit_self_product
Original expanded first-order statement 
forall u. ((exists v. (exists sto_ap_inverse_forward sto_an_inverse_forward sto_bp_inverse_forward sto_bn_inverse_forward sto_cp_inverse_forward sto_cn_inverse_forward. (((((u) = 2 * (sto_ap_inverse_forward) /\ (sto_an_inverse_forward) = 0) \/ exists ge_signed_half_inverse_forwardleft. (((u) = 2 * ge_signed_half_inverse_forwardleft + 1 /\ (sto_ap_inverse_forward) = 0) /\ (sto_an_inverse_forward) = S ge_signed_half_inverse_forwardleft))) /\ ((((((v) = 2 * (sto_bp_inverse_forward) /\ (sto_bn_inverse_forward) = 0) \/ exists ge_signed_half_inverse_forwardright. (((v) = 2 * ge_signed_half_inverse_forwardright + 1 /\ (sto_bp_inverse_forward) = 0) /\ (sto_bn_inverse_forward) = S ge_signed_half_inverse_forwardright))) /\ ((((((2) = 2 * (sto_cp_inverse_forward) /\ (sto_cn_inverse_forward) = 0) \/ exists ge_signed_half_inverse_forwardoutput. (((2) = 2 * ge_signed_half_inverse_forwardoutput + 1 /\ (sto_cp_inverse_forward) = 0) /\ (sto_cn_inverse_forward) = S ge_signed_half_inverse_forwardoutput))) /\ ((sto_ap_inverse_forward * sto_bp_inverse_forward + sto_an_inverse_forward * sto_bn_inverse_forward) + sto_cn_inverse_forward = (sto_ap_inverse_forward * sto_bn_inverse_forward + sto_an_inverse_forward * sto_bp_inverse_forward) + sto_cp_inverse_forward)))))))) -> (((u) = 2 \/ (u) = 1))) /\ ((((u) = 2 \/ (u) = 1)) -> exists v. (exists sto_ap_inverse_backward sto_an_inverse_backward sto_bp_inverse_backward sto_bn_inverse_backward sto_cp_inverse_backward sto_cn_inverse_backward. (((((u) = 2 * (sto_ap_inverse_backward) /\ (sto_an_inverse_backward) = 0) \/ exists ge_signed_half_inverse_backwardleft. (((u) = 2 * ge_signed_half_inverse_backwardleft + 1 /\ (sto_ap_inverse_backward) = 0) /\ (sto_an_inverse_backward) = S ge_signed_half_inverse_backwardleft))) /\ ((((((v) = 2 * (sto_bp_inverse_backward) /\ (sto_bn_inverse_backward) = 0) \/ exists ge_signed_half_inverse_backwardright. (((v) = 2 * ge_signed_half_inverse_backwardright + 1 /\ (sto_bp_inverse_backward) = 0) /\ (sto_bn_inverse_backward) = S ge_signed_half_inverse_backwardright))) /\ ((((((2) = 2 * (sto_cp_inverse_backward) /\ (sto_cn_inverse_backward) = 0) \/ exists ge_signed_half_inverse_backwardoutput. (((2) = 2 * ge_signed_half_inverse_backwardoutput + 1 /\ (sto_cp_inverse_backward) = 0) /\ (sto_cn_inverse_backward) = S ge_signed_half_inverse_backwardoutput))) /\ ((sto_ap_inverse_backward * sto_bp_inverse_backward + sto_an_inverse_backward * sto_bn_inverse_backward) + sto_cn_inverse_backward = (sto_ap_inverse_backward * sto_bn_inverse_backward + sto_an_inverse_backward * sto_bp_inverse_backward) + sto_cp_inverse_backward))))))))

Complete tactic proof in conservative notation

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

21 script commands · 12 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.

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 (2)
dirichlet signed unit product classificationdirichlet signed unit self product
01Fix variables and assumptionsL1–1

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

  1. L1
    intro u
02Separate the logical casesL2–2

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

  1. L2
    split
03Fix variables and assumptionsL3–3

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

  1. L3
    intro h
04Separate the logical casesL4–4

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

  1. L4
    cases h
05Establish hcL5–9

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

  1. L5
    have hc : (u=2 /\ x=2) \/ (u=1 /\ x=1)
  2. L6
    specialize dirichlet_signed_unit_product_classification (u)
  3. L7
    specialize dirichlet_signed_unit_product_classification (x)
  4. L8
    apply dirichlet_signed_unit_product_classification
  5. L9
    exact h_witness
06Separate the logical casesL10–12

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

  1. L10
    cases hc
  2. L11
    cases hc_left
  3. L12
    left
07Use earlier factsL13–13

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

  1. L13
    exact hc_left_left
08Separate the logical casesL14–15

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

  1. L14
    cases hc_right
  2. L15
    right
09Use earlier factsL16–16

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

  1. L16
    exact hc_right_left
10Fix variables and assumptionsL17–17

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

  1. L17
    intro hu
11Construct an explicit witnessL18–18

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

  1. L18
    exists u
12Use earlier factsL19–21

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

  1. L19
    specialize dirichlet_signed_unit_self_product (u)
  2. L20
    apply dirichlet_signed_unit_self_product
  3. L21
    exact hu

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro u
  2. 0002split
  3. 0003intro h
  4. 0004cases h
  5. 0005have hc : (u=2 /\ x=2) \/ (u=1 /\ x=1)
  6. 0006specialize dirichlet_signed_unit_product_classification (u)
  7. 0007specialize dirichlet_signed_unit_product_classification (x)
  8. 0008apply dirichlet_signed_unit_product_classification
  9. 0009exact h_witness
  10. 0010cases hc
  11. 0011cases hc_left
  12. 0012left
  13. 0013exact hc_left_left
  14. 0014cases hc_right
  15. 0015right
  16. 0016exact hc_right_left
  17. 0017intro hu
  18. 0018exists u
  19. 0019specialize dirichlet_signed_unit_self_product (u)
  20. 0020apply dirichlet_signed_unit_self_product
  21. 0021exact hu