JT000F

jordan_primitive_tuple_congruence_transport

Primitivity is invariant under actual coordinatewise residue transport, not field evaluation.

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. JordanTupleCongruence(n,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

JordanPrimitiveTuple(n,b,c,k) · 2JordanTupleCongruence(n,b,c,d,e,k) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisitejordan_divisibility_congruence_transportmod_eq_symm · checked external prerequisite
Original expanded first-order statement 
forall n b c d e k. (forall jt_index_primmod jt_left_primmod jt_right_primmod. (exists jt_gap_primmodindex. jt_gap_primmodindex+S (jt_index_primmod)=(k)) -> (((exists fs_h_jt_primmodleft. fs_h_jt_primmodleft + S (jt_left_primmod) = S ((S (jt_index_primmod)) * c)) /\ exists fs_q_jt_primmodleft. b = fs_q_jt_primmodleft * S ((S (jt_index_primmod)) * c) + (jt_left_primmod))) -> (((exists fs_h_jt_primmodright. fs_h_jt_primmodright + S (jt_right_primmod) = S ((S (jt_index_primmod)) * e)) /\ exists fs_q_jt_primmodright. d = fs_q_jt_primmodright * S ((S (jt_index_primmod)) * e) + (jt_right_primmod))) -> (exists jt_left_primmodmod jt_right_primmodmod. (jt_left_primmod)+(n)*jt_left_primmodmod=(jt_right_primmod)+(n)*jt_right_primmodmod)) -> (forall jt_divisor_primmodsource. (exists jt_factor_primmodsourcemodulus. (n)=(jt_divisor_primmodsource)*jt_factor_primmodsourcemodulus) -> (forall jt_index_primmodsourcecoordinates jt_value_primmodsourcecoordinates. (exists jt_gap_primmodsourcecoordinatesindex. jt_gap_primmodsourcecoordinatesindex+S (jt_index_primmodsourcecoordinates)=(k)) -> (((exists fs_h_jt_primmodsourcecoordinatesat. fs_h_jt_primmodsourcecoordinatesat + S (jt_value_primmodsourcecoordinates) = S ((S (jt_index_primmodsourcecoordinates)) * c)) /\ exists fs_q_jt_primmodsourcecoordinatesat. b = fs_q_jt_primmodsourcecoordinatesat * S ((S (jt_index_primmodsourcecoordinates)) * c) + (jt_value_primmodsourcecoordinates))) -> (exists jt_factor_primmodsourcecoordinatesdivides. (jt_value_primmodsourcecoordinates)=(jt_divisor_primmodsource)*jt_factor_primmodsourcecoordinatesdivides)) -> jt_divisor_primmodsource=1) -> (forall jt_divisor_primmodtarget. (exists jt_factor_primmodtargetmodulus. (n)=(jt_divisor_primmodtarget)*jt_factor_primmodtargetmodulus) -> (forall jt_index_primmodtargetcoordinates jt_value_primmodtargetcoordinates. (exists jt_gap_primmodtargetcoordinatesindex. jt_gap_primmodtargetcoordinatesindex+S (jt_index_primmodtargetcoordinates)=(k)) -> (((exists fs_h_jt_primmodtargetcoordinatesat. fs_h_jt_primmodtargetcoordinatesat + S (jt_value_primmodtargetcoordinates) = S ((S (jt_index_primmodtargetcoordinates)) * e)) /\ exists fs_q_jt_primmodtargetcoordinatesat. d = fs_q_jt_primmodtargetcoordinatesat * S ((S (jt_index_primmodtargetcoordinates)) * e) + (jt_value_primmodtargetcoordinates))) -> (exists jt_factor_primmodtargetcoordinatesdivides. (jt_value_primmodtargetcoordinates)=(jt_divisor_primmodtarget)*jt_factor_primmodtargetcoordinatesdivides)) -> jt_divisor_primmodtarget=1)

Complete tactic proof in conservative notation

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

46 script commands · 9 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 (1)
jordan divisibility congruence transport
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 hm
  8. L8
    intro hp
  9. L9
    intro q
  10. L10
    intro hqn
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hall
03Use earlier factsL12–14

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

  1. L12
    specialize hp (q)
  2. L13
    apply hp
  3. L14
    exact hqn
04Fix variables and assumptionsL15–18

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

  1. L15
    intro i
  2. L16
    intro a
  3. L17
    intro hi
  4. L18
    intro ha
05Establish hzL19–23

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

  1. L19
    have hz : ∃ z. BetaAt(d,e,i,z)Definitions: BetaAt(d,e,i,z)Original native command in the exact edition
  2. L20
    specialize beta_at_exists (d)
  3. L21
    specialize beta_at_exists (e)
  4. L22
    specialize beta_at_exists (i)
  5. L23
    apply beta_at_exists
06Separate the logical casesL24–24

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

  1. L24
    cases hz
07Use earlier factsL25–34

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

  1. L25
    specialize jordan_divisibility_congruence_transport (n)
  2. L26
    specialize jordan_divisibility_congruence_transport (q)
  3. L27
    specialize jordan_divisibility_congruence_transport (x)
  4. L28
    specialize jordan_divisibility_congruence_transport (a)
  5. L29
    apply jordan_divisibility_congruence_transport
  6. L30
    exact hqn
  7. L31
    specialize hall (i)
  8. L32
    specialize hall (x)
  9. L33
    apply hall
  10. L34
    exact hi
08Use earlier factsL35–44

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

  1. L35
    exact hz_witness
  2. L36
    specialize mod_eq_symm (n)
  3. L37
    specialize mod_eq_symm (a)
  4. L38
    specialize mod_eq_symm (x)
  5. L39
    apply mod_eq_symm
  6. L40
    specialize hm (i)
  7. L41
    specialize hm (a)
  8. L42
    specialize hm (x)
  9. L43
    apply hm
  10. L44
    exact hi
09Use earlier factsL45–46

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

  1. L45
    exact ha
  2. L46
    exact hz_witness

Library-wide reading audit

Original defined command ledger · 46 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro k
  7. 0007intro hm
  8. 0008intro hp
  9. 0009intro q
  10. 0010intro hqn
  11. 0011intro hall
  12. 0012specialize hp (q)
  13. 0013apply hp
  14. 0014exact hqn
  15. 0015intro i
  16. 0016intro a
  17. 0017intro hi
  18. 0018intro ha
  19. 0019have hz : ∃ z. BetaAt(d,e,i,z)
  20. 0020specialize beta_at_exists (d)
  21. 0021specialize beta_at_exists (e)
  22. 0022specialize beta_at_exists (i)
  23. 0023apply beta_at_exists
  24. 0024cases hz
  25. 0025specialize jordan_divisibility_congruence_transport (n)
  26. 0026specialize jordan_divisibility_congruence_transport (q)
  27. 0027specialize jordan_divisibility_congruence_transport (x)
  28. 0028specialize jordan_divisibility_congruence_transport (a)
  29. 0029apply jordan_divisibility_congruence_transport
  30. 0030exact hqn
  31. 0031specialize hall (i)
  32. 0032specialize hall (x)
  33. 0033apply hall
  34. 0034exact hi
  35. 0035exact hz_witness
  36. 0036specialize mod_eq_symm (n)
  37. 0037specialize mod_eq_symm (a)
  38. 0038specialize mod_eq_symm (x)
  39. 0039apply mod_eq_symm
  40. 0040specialize hm (i)
  41. 0041specialize hm (a)
  42. 0042specialize hm (x)
  43. 0043apply hm
  44. 0044exact hi
  45. 0045exact ha
  46. 0046exact hz_witness