JT000F

jordan_primitive_tuple_congruence_transport

Alpha v35 independently verified · alpha_closed; checked-use authorized; not Stable

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

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 46 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_exists Alpha theorem; checked-use authorized JT000D jordan_divisibility_congruence_transport mod_eq_symm Alpha theorem; checked-use authorized

Direct dependents

JT0033 jordan_primitive_crt_tuple_exists JT0045 jordan_enumeration_reduce_primitive

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 : exists z. ((exists fs_h_jt_primmodactual. fs_h_jt_primmodactual + S (z) = S ((S (i)) * e)) /\ exists fs_q_jt_primmodactual. d = fs_q_jt_primmodactual * S ((S (i)) * e) + (z))
  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 exact 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 : exists z. ((exists fs_h_jt_primmodactual. fs_h_jt_primmodactual + S (z) = S ((S (i)) * e)) /\ exists fs_q_jt_primmodactual. d = fs_q_jt_primmodactual * S ((S (i)) * e) + (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