JT0039

jordan_tuple_bounded_congruence_equal

Actual canonical residues with pointwise congruence are equal as coordinate functions.

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. BetaPrefixInto(b,c,k,n) → BetaPrefixInto(d,e,k,n) → JordanTupleCongruence(n,b,c,d,e,k) → IntegerVectorZero(b,c,d,e,k)

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

Definition DAG

IntegerVectorZero(ab,ac,db,dc,l) · 1BetaPrefixInto(b,c,l,B) · 2JordanTupleCongruence(n,b,c,d,e,k) · 1

Actual proof prerequisites

mod_eq_bounded_unique · checked external prerequisitematrix_rank_bounded_prefix_value · checked external prerequisite
Original expanded first-order statement 
forall n b c d e k. (forall jt_index_congboundleft. (exists jt_gap_congboundleftindex. jt_gap_congboundleftindex+S (jt_index_congboundleft)=(k)) -> exists jt_value_congboundleft. ((((exists fs_h_jt_congboundleftat. fs_h_jt_congboundleftat + S (jt_value_congboundleft) = S ((S (jt_index_congboundleft)) * c)) /\ exists fs_q_jt_congboundleftat. b = fs_q_jt_congboundleftat * S ((S (jt_index_congboundleft)) * c) + (jt_value_congboundleft))) /\ (exists jt_gap_congboundleftvalue. jt_gap_congboundleftvalue+S (jt_value_congboundleft)=(n)))) -> (forall jt_index_congboundright. (exists jt_gap_congboundrightindex. jt_gap_congboundrightindex+S (jt_index_congboundright)=(k)) -> exists jt_value_congboundright. ((((exists fs_h_jt_congboundrightat. fs_h_jt_congboundrightat + S (jt_value_congboundright) = S ((S (jt_index_congboundright)) * e)) /\ exists fs_q_jt_congboundrightat. d = fs_q_jt_congboundrightat * S ((S (jt_index_congboundright)) * e) + (jt_value_congboundright))) /\ (exists jt_gap_congboundrightvalue. jt_gap_congboundrightvalue+S (jt_value_congboundright)=(n)))) -> (forall jt_index_congboth jt_left_congboth jt_right_congboth. (exists jt_gap_congbothindex. jt_gap_congbothindex+S (jt_index_congboth)=(k)) -> (((exists fs_h_jt_congbothleft. fs_h_jt_congbothleft + S (jt_left_congboth) = S ((S (jt_index_congboth)) * c)) /\ exists fs_q_jt_congbothleft. b = fs_q_jt_congbothleft * S ((S (jt_index_congboth)) * c) + (jt_left_congboth))) -> (((exists fs_h_jt_congbothright. fs_h_jt_congbothright + S (jt_right_congboth) = S ((S (jt_index_congboth)) * e)) /\ exists fs_q_jt_congbothright. d = fs_q_jt_congbothright * S ((S (jt_index_congboth)) * e) + (jt_right_congboth))) -> (exists jt_left_congbothmod jt_right_congbothmod. (jt_left_congboth)+(n)*jt_left_congbothmod=(jt_right_congboth)+(n)*jt_right_congbothmod)) -> (forall jt_index_congequal jt_left_congequal jt_right_congequal. (exists jt_gap_congequalindex. jt_gap_congequalindex+S (jt_index_congequal)=(k)) -> (((exists fs_h_jt_congequalleft. fs_h_jt_congequalleft + S (jt_left_congequal) = S ((S (jt_index_congequal)) * c)) /\ exists fs_q_jt_congequalleft. b = fs_q_jt_congequalleft * S ((S (jt_index_congequal)) * c) + (jt_left_congequal))) -> (((exists fs_h_jt_congequalright. fs_h_jt_congequalright + S (jt_right_congequal) = S ((S (jt_index_congequal)) * e)) /\ exists fs_q_jt_congequalright. d = fs_q_jt_congequalright * S ((S (jt_index_congequal)) * e) + (jt_right_congequal))) -> jt_left_congequal=jt_right_congequal)

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 · 6 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–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 hb
  8. L8
    intro hd
  9. L9
    intro hm
  10. L10
    intro i
02Fix variables and assumptionsL11–15

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

  1. L11
    intro a
  2. L12
    intro z
  3. L13
    intro hi
  4. L14
    intro ha
  5. L15
    intro hz
03Use earlier factsL16–25

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

  1. L16
    specialize mod_eq_bounded_unique (n)
  2. L17
    specialize mod_eq_bounded_unique (a)
  3. L18
    specialize mod_eq_bounded_unique (z)
  4. L19
    apply mod_eq_bounded_unique
  5. L20
    specialize matrix_rank_bounded_prefix_value (b)
  6. L21
    specialize matrix_rank_bounded_prefix_value (c)
  7. L22
    specialize matrix_rank_bounded_prefix_value (k)
  8. L23
    specialize matrix_rank_bounded_prefix_value (n)
  9. L24
    specialize matrix_rank_bounded_prefix_value (i)
  10. L25
    specialize matrix_rank_bounded_prefix_value (a)
04Use earlier factsL26–35

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

  1. L26
    apply matrix_rank_bounded_prefix_value
  2. L27
    exact hb
  3. L28
    exact hi
  4. L29
    exact ha
  5. L30
    specialize matrix_rank_bounded_prefix_value (d)
  6. L31
    specialize matrix_rank_bounded_prefix_value (e)
  7. L32
    specialize matrix_rank_bounded_prefix_value (k)
  8. L33
    specialize matrix_rank_bounded_prefix_value (n)
  9. L34
    specialize matrix_rank_bounded_prefix_value (i)
  10. L35
    specialize matrix_rank_bounded_prefix_value (z)
05Use earlier factsL36–45

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

  1. L36
    apply matrix_rank_bounded_prefix_value
  2. L37
    exact hd
  3. L38
    exact hi
  4. L39
    exact hz
  5. L40
    specialize hm (i)
  6. L41
    specialize hm (a)
  7. L42
    specialize hm (z)
  8. L43
    apply hm
  9. L44
    exact hi
  10. L45
    exact ha
06Use earlier factsL46–46

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

  1. L46
    exact hz

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 hb
  8. 0008intro hd
  9. 0009intro hm
  10. 0010intro i
  11. 0011intro a
  12. 0012intro z
  13. 0013intro hi
  14. 0014intro ha
  15. 0015intro hz
  16. 0016specialize mod_eq_bounded_unique (n)
  17. 0017specialize mod_eq_bounded_unique (a)
  18. 0018specialize mod_eq_bounded_unique (z)
  19. 0019apply mod_eq_bounded_unique
  20. 0020specialize matrix_rank_bounded_prefix_value (b)
  21. 0021specialize matrix_rank_bounded_prefix_value (c)
  22. 0022specialize matrix_rank_bounded_prefix_value (k)
  23. 0023specialize matrix_rank_bounded_prefix_value (n)
  24. 0024specialize matrix_rank_bounded_prefix_value (i)
  25. 0025specialize matrix_rank_bounded_prefix_value (a)
  26. 0026apply matrix_rank_bounded_prefix_value
  27. 0027exact hb
  28. 0028exact hi
  29. 0029exact ha
  30. 0030specialize matrix_rank_bounded_prefix_value (d)
  31. 0031specialize matrix_rank_bounded_prefix_value (e)
  32. 0032specialize matrix_rank_bounded_prefix_value (k)
  33. 0033specialize matrix_rank_bounded_prefix_value (n)
  34. 0034specialize matrix_rank_bounded_prefix_value (i)
  35. 0035specialize matrix_rank_bounded_prefix_value (z)
  36. 0036apply matrix_rank_bounded_prefix_value
  37. 0037exact hd
  38. 0038exact hi
  39. 0039exact hz
  40. 0040specialize hm (i)
  41. 0041specialize hm (a)
  42. 0042specialize hm (z)
  43. 0043apply hm
  44. 0044exact hi
  45. 0045exact ha
  46. 0046exact hz