JT0002

jordan_tuple_equal_symm

Coordinate equality is symmetric without selecting canonical codes.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ k. IntegerVectorZero(b,c,d,e,k) → IntegerVectorZero(d,e,b,c,k)

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

Definition DAG

IntegerVectorZero(ab,ac,db,dc,l) · 2

Actual proof prerequisites

none
Original expanded first-order statement 
forall b c d e k. (forall jt_index_symmsource jt_left_symmsource jt_right_symmsource. (exists jt_gap_symmsourceindex. jt_gap_symmsourceindex+S (jt_index_symmsource)=(k)) -> (((exists fs_h_jt_symmsourceleft. fs_h_jt_symmsourceleft + S (jt_left_symmsource) = S ((S (jt_index_symmsource)) * c)) /\ exists fs_q_jt_symmsourceleft. b = fs_q_jt_symmsourceleft * S ((S (jt_index_symmsource)) * c) + (jt_left_symmsource))) -> (((exists fs_h_jt_symmsourceright. fs_h_jt_symmsourceright + S (jt_right_symmsource) = S ((S (jt_index_symmsource)) * e)) /\ exists fs_q_jt_symmsourceright. d = fs_q_jt_symmsourceright * S ((S (jt_index_symmsource)) * e) + (jt_right_symmsource))) -> jt_left_symmsource=jt_right_symmsource) -> (forall jt_index_symmtarget jt_left_symmtarget jt_right_symmtarget. (exists jt_gap_symmtargetindex. jt_gap_symmtargetindex+S (jt_index_symmtarget)=(k)) -> (((exists fs_h_jt_symmtargetleft. fs_h_jt_symmtargetleft + S (jt_left_symmtarget) = S ((S (jt_index_symmtarget)) * e)) /\ exists fs_q_jt_symmtargetleft. d = fs_q_jt_symmtargetleft * S ((S (jt_index_symmtarget)) * e) + (jt_left_symmtarget))) -> (((exists fs_h_jt_symmtargetright. fs_h_jt_symmtargetright + S (jt_right_symmtarget) = S ((S (jt_index_symmtarget)) * c)) /\ exists fs_q_jt_symmtargetright. b = fs_q_jt_symmtargetright * S ((S (jt_index_symmtarget)) * c) + (jt_right_symmtarget))) -> jt_left_symmtarget=jt_right_symmtarget)

Complete tactic proof in conservative notation

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

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

01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro k
  6. L6
    intro h
  7. L7
    intro i
  8. L8
    intro a
  9. L9
    intro z
  10. L10
    intro hi
02Fix variables and assumptionsL11–12

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

  1. L11
    intro ha
  2. L12
    intro hz
03Establish hreverseL13–22

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

  1. L13
    have hreverse : z=a
  2. L14
    specialize h (i)
  3. L15
    specialize h (z)
  4. L16
    specialize h (a)
  5. L17
    apply h
  6. L18
    exact hi
  7. L19
    exact hz
  8. L20
    exact ha
  9. L21
    symm
  10. L22
    exact hreverse

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro k
  6. 0006intro h
  7. 0007intro i
  8. 0008intro a
  9. 0009intro z
  10. 0010intro hi
  11. 0011intro ha
  12. 0012intro hz
  13. 0013have hreverse : z=a
  14. 0014specialize h (i)
  15. 0015specialize h (z)
  16. 0016specialize h (a)
  17. 0017apply h
  18. 0018exact hi
  19. 0019exact hz
  20. 0020exact ha
  21. 0021symm
  22. 0022exact hreverse