JT0005

jordan_primitive_tuple_transport

Primitive means common-divisor one and is independent of beta presentation.

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

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

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

Definition DAG

IntegerVectorZero(ab,ac,db,dc,l) · 1JordanPrimitiveTuple(n,b,c,k) · 2

Actual proof prerequisites

jordan_tuple_common_divisor_transportjordan_tuple_equal_symm
Original expanded first-order statement 
forall n b c d e k. (forall jt_index_pr_equal jt_left_pr_equal jt_right_pr_equal. (exists jt_gap_pr_equalindex. jt_gap_pr_equalindex+S (jt_index_pr_equal)=(k)) -> (((exists fs_h_jt_pr_equalleft. fs_h_jt_pr_equalleft + S (jt_left_pr_equal) = S ((S (jt_index_pr_equal)) * c)) /\ exists fs_q_jt_pr_equalleft. b = fs_q_jt_pr_equalleft * S ((S (jt_index_pr_equal)) * c) + (jt_left_pr_equal))) -> (((exists fs_h_jt_pr_equalright. fs_h_jt_pr_equalright + S (jt_right_pr_equal) = S ((S (jt_index_pr_equal)) * e)) /\ exists fs_q_jt_pr_equalright. d = fs_q_jt_pr_equalright * S ((S (jt_index_pr_equal)) * e) + (jt_right_pr_equal))) -> jt_left_pr_equal=jt_right_pr_equal) -> (forall jt_divisor_prsource. (exists jt_factor_prsourcemodulus. (n)=(jt_divisor_prsource)*jt_factor_prsourcemodulus) -> (forall jt_index_prsourcecoordinates jt_value_prsourcecoordinates. (exists jt_gap_prsourcecoordinatesindex. jt_gap_prsourcecoordinatesindex+S (jt_index_prsourcecoordinates)=(k)) -> (((exists fs_h_jt_prsourcecoordinatesat. fs_h_jt_prsourcecoordinatesat + S (jt_value_prsourcecoordinates) = S ((S (jt_index_prsourcecoordinates)) * c)) /\ exists fs_q_jt_prsourcecoordinatesat. b = fs_q_jt_prsourcecoordinatesat * S ((S (jt_index_prsourcecoordinates)) * c) + (jt_value_prsourcecoordinates))) -> (exists jt_factor_prsourcecoordinatesdivides. (jt_value_prsourcecoordinates)=(jt_divisor_prsource)*jt_factor_prsourcecoordinatesdivides)) -> jt_divisor_prsource=1) -> (forall jt_divisor_prtarget. (exists jt_factor_prtargetmodulus. (n)=(jt_divisor_prtarget)*jt_factor_prtargetmodulus) -> (forall jt_index_prtargetcoordinates jt_value_prtargetcoordinates. (exists jt_gap_prtargetcoordinatesindex. jt_gap_prtargetcoordinatesindex+S (jt_index_prtargetcoordinates)=(k)) -> (((exists fs_h_jt_prtargetcoordinatesat. fs_h_jt_prtargetcoordinatesat + S (jt_value_prtargetcoordinates) = S ((S (jt_index_prtargetcoordinates)) * e)) /\ exists fs_q_jt_prtargetcoordinatesat. d = fs_q_jt_prtargetcoordinatesat * S ((S (jt_index_prtargetcoordinates)) * e) + (jt_value_prtargetcoordinates))) -> (exists jt_factor_prtargetcoordinatesdivides. (jt_value_prtargetcoordinates)=(jt_divisor_prtarget)*jt_factor_prtargetcoordinatesdivides)) -> jt_divisor_prtarget=1)

Complete tactic proof in conservative notation

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

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

Named ingredients (2)
jordan tuple common divisor transportjordan tuple equal symm
01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro k
  7. L7
    intro heq
  8. L8
    intro hp
  9. L9
    intro q
  10. L10
    intro hq
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hall
03Use earlier factsL12–21

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

  1. L12
    specialize hp (q)
  2. L13
    apply hp
  3. L14
    exact hq
  4. L15
    specialize jordan_tuple_common_divisor_transport (q)
  5. L16
    specialize jordan_tuple_common_divisor_transport (d)
  6. L17
    specialize jordan_tuple_common_divisor_transport (e)
  7. L18
    specialize jordan_tuple_common_divisor_transport (b)
  8. L19
    specialize jordan_tuple_common_divisor_transport (c)
  9. L20
    specialize jordan_tuple_common_divisor_transport (k)
  10. L21
    apply jordan_tuple_common_divisor_transport
04Use earlier factsL22–29

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

  1. L22
    specialize jordan_tuple_equal_symm (b)
  2. L23
    specialize jordan_tuple_equal_symm (c)
  3. L24
    specialize jordan_tuple_equal_symm (d)
  4. L25
    specialize jordan_tuple_equal_symm (e)
  5. L26
    specialize jordan_tuple_equal_symm (k)
  6. L27
    apply jordan_tuple_equal_symm
  7. L28
    exact heq
  8. L29
    exact hall

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro k
  7. 0007intro heq
  8. 0008intro hp
  9. 0009intro q
  10. 0010intro hq
  11. 0011intro hall
  12. 0012specialize hp (q)
  13. 0013apply hp
  14. 0014exact hq
  15. 0015specialize jordan_tuple_common_divisor_transport (q)
  16. 0016specialize jordan_tuple_common_divisor_transport (d)
  17. 0017specialize jordan_tuple_common_divisor_transport (e)
  18. 0018specialize jordan_tuple_common_divisor_transport (b)
  19. 0019specialize jordan_tuple_common_divisor_transport (c)
  20. 0020specialize jordan_tuple_common_divisor_transport (k)
  21. 0021apply jordan_tuple_common_divisor_transport
  22. 0022specialize jordan_tuple_equal_symm (b)
  23. 0023specialize jordan_tuple_equal_symm (c)
  24. 0024specialize jordan_tuple_equal_symm (d)
  25. 0025specialize jordan_tuple_equal_symm (e)
  26. 0026specialize jordan_tuple_equal_symm (k)
  27. 0027apply jordan_tuple_equal_symm
  28. 0028exact heq
  29. 0029exact hall