IV0002

dirichlet_unit_at_one_from_value

A genuine lookup with a canonical signed unit value satisfies the two-case unit-at-one predicate.

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.

For an actual table an inverse exists exactly when N=0 or F(1) is signed +1 or -1. At a positive window this is the unit-at-one criterion; the empty window imposes no condition at one. Every inverse has actual delta and two-sided convolution witnesses. Its zeroth value is arbitrary, so uniqueness is positive-value equality, not equality of codes or of zeroth values. Multiplicative-function closure and full finite signed G009 are admitted in the separate Alpha-v32 multiplicative-convolution family.

Exact theorem in conservative defined notation

∀ F. ∀ u. ArithAt(F,1,u) → SignedUnit(u) → DirichletUnitAtOne(F)

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

Definition DAG

ArithAt(F,i,z) · 1SignedUnit(u) · 1DirichletUnitAtOne(F) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall F u. (exists dst_positive_code_unit_value_entry dst_positive_scale_unit_value_entry dst_negative_code_unit_value_entry dst_negative_scale_unit_value_entry dst_positive_unit_value_entry dst_negative_unit_value_entry. (((F) = (((((dst_positive_code_unit_value_entry) + (dst_positive_scale_unit_value_entry)) * S ((dst_positive_code_unit_value_entry) + (dst_positive_scale_unit_value_entry)) + ((dst_positive_scale_unit_value_entry) + (dst_positive_scale_unit_value_entry))) + (((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) * S ((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) + ((dst_negative_scale_unit_value_entry) + (dst_negative_scale_unit_value_entry)))) * S ((((dst_positive_code_unit_value_entry) + (dst_positive_scale_unit_value_entry)) * S ((dst_positive_code_unit_value_entry) + (dst_positive_scale_unit_value_entry)) + ((dst_positive_scale_unit_value_entry) + (dst_positive_scale_unit_value_entry))) + (((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) * S ((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) + ((dst_negative_scale_unit_value_entry) + (dst_negative_scale_unit_value_entry)))) + ((((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) * S ((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) + ((dst_negative_scale_unit_value_entry) + (dst_negative_scale_unit_value_entry))) + (((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) * S ((dst_negative_code_unit_value_entry) + (dst_negative_scale_unit_value_entry)) + ((dst_negative_scale_unit_value_entry) + (dst_negative_scale_unit_value_entry)))))) /\ (((((exists ff_h_pvs_unit_value_entrypositive. ff_h_pvs_unit_value_entrypositive + S (dst_positive_unit_value_entry) = S ((S (1)) * dst_positive_scale_unit_value_entry)) /\ exists ff_q_pvs_unit_value_entrypositive. dst_positive_code_unit_value_entry = ff_q_pvs_unit_value_entrypositive * S ((S (1)) * dst_positive_scale_unit_value_entry) + (dst_positive_unit_value_entry))) /\ (((((exists ff_h_pvs_unit_value_entrynegative. ff_h_pvs_unit_value_entrynegative + S (dst_negative_unit_value_entry) = S ((S (1)) * dst_negative_scale_unit_value_entry)) /\ exists ff_q_pvs_unit_value_entrynegative. dst_negative_code_unit_value_entry = ff_q_pvs_unit_value_entrynegative * S ((S (1)) * dst_negative_scale_unit_value_entry) + (dst_negative_unit_value_entry))) /\ (exists ge_balance_positive_unit_value_entryvalue ge_balance_negative_unit_value_entryvalue. (((((u) = 2 * (ge_balance_positive_unit_value_entryvalue) /\ (ge_balance_negative_unit_value_entryvalue) = 0) \/ exists ge_signed_half_unit_value_entryvaluedecode. (((u) = 2 * ge_signed_half_unit_value_entryvaluedecode + 1 /\ (ge_balance_positive_unit_value_entryvalue) = 0) /\ (ge_balance_negative_unit_value_entryvalue) = S ge_signed_half_unit_value_entryvaluedecode))) /\ ((dst_positive_unit_value_entry) + ge_balance_negative_unit_value_entryvalue = (dst_negative_unit_value_entry) + ge_balance_positive_unit_value_entryvalue))))))))) -> (((u) = 2 \/ (u) = 1)) -> ((exists dst_positive_code_unit_value_resultpositive dst_positive_scale_unit_value_resultpositive dst_negative_code_unit_value_resultpositive dst_negative_scale_unit_value_resultpositive dst_positive_unit_value_resultpositive dst_negative_unit_value_resultpositive. (((F) = (((((dst_positive_code_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive)) * S ((dst_positive_code_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive)) + ((dst_positive_scale_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive))) + (((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) * S ((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) + ((dst_negative_scale_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)))) * S ((((dst_positive_code_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive)) * S ((dst_positive_code_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive)) + ((dst_positive_scale_unit_value_resultpositive) + (dst_positive_scale_unit_value_resultpositive))) + (((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) * S ((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) + ((dst_negative_scale_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)))) + ((((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) * S ((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) + ((dst_negative_scale_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive))) + (((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) * S ((dst_negative_code_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)) + ((dst_negative_scale_unit_value_resultpositive) + (dst_negative_scale_unit_value_resultpositive)))))) /\ (((((exists ff_h_pvs_unit_value_resultpositivepositive. ff_h_pvs_unit_value_resultpositivepositive + S (dst_positive_unit_value_resultpositive) = S ((S (1)) * dst_positive_scale_unit_value_resultpositive)) /\ exists ff_q_pvs_unit_value_resultpositivepositive. dst_positive_code_unit_value_resultpositive = ff_q_pvs_unit_value_resultpositivepositive * S ((S (1)) * dst_positive_scale_unit_value_resultpositive) + (dst_positive_unit_value_resultpositive))) /\ (((((exists ff_h_pvs_unit_value_resultpositivenegative. ff_h_pvs_unit_value_resultpositivenegative + S (dst_negative_unit_value_resultpositive) = S ((S (1)) * dst_negative_scale_unit_value_resultpositive)) /\ exists ff_q_pvs_unit_value_resultpositivenegative. dst_negative_code_unit_value_resultpositive = ff_q_pvs_unit_value_resultpositivenegative * S ((S (1)) * dst_negative_scale_unit_value_resultpositive) + (dst_negative_unit_value_resultpositive))) /\ (exists ge_balance_positive_unit_value_resultpositivevalue ge_balance_negative_unit_value_resultpositivevalue. (((((2) = 2 * (ge_balance_positive_unit_value_resultpositivevalue) /\ (ge_balance_negative_unit_value_resultpositivevalue) = 0) \/ exists ge_signed_half_unit_value_resultpositivevaluedecode. (((2) = 2 * ge_signed_half_unit_value_resultpositivevaluedecode + 1 /\ (ge_balance_positive_unit_value_resultpositivevalue) = 0) /\ (ge_balance_negative_unit_value_resultpositivevalue) = S ge_signed_half_unit_value_resultpositivevaluedecode))) /\ ((dst_positive_unit_value_resultpositive) + ge_balance_negative_unit_value_resultpositivevalue = (dst_negative_unit_value_resultpositive) + ge_balance_positive_unit_value_resultpositivevalue))))))))) \/ (exists dst_positive_code_unit_value_resultnegative dst_positive_scale_unit_value_resultnegative dst_negative_code_unit_value_resultnegative dst_negative_scale_unit_value_resultnegative dst_positive_unit_value_resultnegative dst_negative_unit_value_resultnegative. (((F) = (((((dst_positive_code_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative)) * S ((dst_positive_code_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative)) + ((dst_positive_scale_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative))) + (((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) * S ((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) + ((dst_negative_scale_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)))) * S ((((dst_positive_code_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative)) * S ((dst_positive_code_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative)) + ((dst_positive_scale_unit_value_resultnegative) + (dst_positive_scale_unit_value_resultnegative))) + (((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) * S ((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) + ((dst_negative_scale_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)))) + ((((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) * S ((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) + ((dst_negative_scale_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative))) + (((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) * S ((dst_negative_code_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)) + ((dst_negative_scale_unit_value_resultnegative) + (dst_negative_scale_unit_value_resultnegative)))))) /\ (((((exists ff_h_pvs_unit_value_resultnegativepositive. ff_h_pvs_unit_value_resultnegativepositive + S (dst_positive_unit_value_resultnegative) = S ((S (1)) * dst_positive_scale_unit_value_resultnegative)) /\ exists ff_q_pvs_unit_value_resultnegativepositive. dst_positive_code_unit_value_resultnegative = ff_q_pvs_unit_value_resultnegativepositive * S ((S (1)) * dst_positive_scale_unit_value_resultnegative) + (dst_positive_unit_value_resultnegative))) /\ (((((exists ff_h_pvs_unit_value_resultnegativenegative. ff_h_pvs_unit_value_resultnegativenegative + S (dst_negative_unit_value_resultnegative) = S ((S (1)) * dst_negative_scale_unit_value_resultnegative)) /\ exists ff_q_pvs_unit_value_resultnegativenegative. dst_negative_code_unit_value_resultnegative = ff_q_pvs_unit_value_resultnegativenegative * S ((S (1)) * dst_negative_scale_unit_value_resultnegative) + (dst_negative_unit_value_resultnegative))) /\ (exists ge_balance_positive_unit_value_resultnegativevalue ge_balance_negative_unit_value_resultnegativevalue. (((((1) = 2 * (ge_balance_positive_unit_value_resultnegativevalue) /\ (ge_balance_negative_unit_value_resultnegativevalue) = 0) \/ exists ge_signed_half_unit_value_resultnegativevaluedecode. (((1) = 2 * ge_signed_half_unit_value_resultnegativevaluedecode + 1 /\ (ge_balance_positive_unit_value_resultnegativevalue) = 0) /\ (ge_balance_negative_unit_value_resultnegativevalue) = S ge_signed_half_unit_value_resultnegativevaluedecode))) /\ ((dst_positive_unit_value_resultnegative) + ge_balance_negative_unit_value_resultnegativevalue = (dst_negative_unit_value_resultnegative) + ge_balance_positive_unit_value_resultnegativevalue))))))))))

Complete tactic proof in conservative notation

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

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

01Fix variables and assumptionsL1–4

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

  1. L1
    intro F
  2. L2
    intro u
  3. L3
    intro ha
  4. L4
    intro hu
02Separate the logical casesL5–6

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

  1. L5
    cases hu
  2. L6
    left
03Calculate and transport equalitiesL7–8

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

  1. L7
    rewrite hu_left at ha
  2. L8
    rewrite hu_left at ha
04Use earlier factsL9–9

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

  1. L9
    exact ha
05Separate the logical casesL10–10

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

  1. L10
    right
06Calculate and transport equalitiesL11–12

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

  1. L11
    rewrite hu_right at ha
  2. L12
    rewrite hu_right at ha
07Use earlier factsL13–13

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

  1. L13
    exact ha

Library-wide reading audit

Original defined command ledger · 13 lines
  1. 0001intro F
  2. 0002intro u
  3. 0003intro ha
  4. 0004intro hu
  5. 0005cases hu
  6. 0006left
  7. 0007rewrite hu_left at ha
  8. 0008rewrite hu_left at ha
  9. 0009exact ha
  10. 0010right
  11. 0011rewrite hu_right at ha
  12. 0012rewrite hu_right at ha
  13. 0013exact ha