JT002E

jordan_crt_tuple_right

Every actual output coordinate has the required right congruence.

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

∀ m. ∀ n. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ k. JordanTupleCRT(m,n,b,c,d,e,f,g,k) → JordanTupleCongruence(n,f,g,d,e,k)

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

Definition DAG

JordanTupleCongruence(n,b,c,d,e,k) · 1JordanTupleCRT(m,n,b,c,d,e,f,g,k) · 1ModEq(m,a,b) · 2BetaAt(b,c,i,x) · 3

Actual proof prerequisites

beta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall m n b c d e f g k. (forall jt_index_crtright. (exists jt_gap_crtrightindex. jt_gap_crtrightindex+S (jt_index_crtright)=(k)) -> exists jt_left_crtright jt_right_crtright jt_output_crtright. ((((exists fs_h_jt_crtrightleft. fs_h_jt_crtrightleft + S (jt_left_crtright) = S ((S (jt_index_crtright)) * c)) /\ exists fs_q_jt_crtrightleft. b = fs_q_jt_crtrightleft * S ((S (jt_index_crtright)) * c) + (jt_left_crtright))) /\ (((((exists fs_h_jt_crtrightright. fs_h_jt_crtrightright + S (jt_right_crtright) = S ((S (jt_index_crtright)) * e)) /\ exists fs_q_jt_crtrightright. d = fs_q_jt_crtrightright * S ((S (jt_index_crtright)) * e) + (jt_right_crtright))) /\ (((((exists fs_h_jt_crtrightoutput. fs_h_jt_crtrightoutput + S (jt_output_crtright) = S ((S (jt_index_crtright)) * g)) /\ exists fs_q_jt_crtrightoutput. f = fs_q_jt_crtrightoutput * S ((S (jt_index_crtright)) * g) + (jt_output_crtright))) /\ (((exists jt_left_crtrightmodleft jt_right_crtrightmodleft. (jt_output_crtright)+(m)*jt_left_crtrightmodleft=(jt_left_crtright)+(m)*jt_right_crtrightmodleft) /\ (exists jt_left_crtrightmodright jt_right_crtrightmodright. (jt_output_crtright)+(n)*jt_left_crtrightmodright=(jt_right_crtright)+(n)*jt_right_crtrightmodright))))))))) -> (forall jt_index_crtprojectionright jt_left_crtprojectionright jt_right_crtprojectionright. (exists jt_gap_crtprojectionrightindex. jt_gap_crtprojectionrightindex+S (jt_index_crtprojectionright)=(k)) -> (((exists fs_h_jt_crtprojectionrightleft. fs_h_jt_crtprojectionrightleft + S (jt_left_crtprojectionright) = S ((S (jt_index_crtprojectionright)) * g)) /\ exists fs_q_jt_crtprojectionrightleft. f = fs_q_jt_crtprojectionrightleft * S ((S (jt_index_crtprojectionright)) * g) + (jt_left_crtprojectionright))) -> (((exists fs_h_jt_crtprojectionrightright. fs_h_jt_crtprojectionrightright + S (jt_right_crtprojectionright) = S ((S (jt_index_crtprojectionright)) * e)) /\ exists fs_q_jt_crtprojectionrightright. d = fs_q_jt_crtprojectionrightright * S ((S (jt_index_crtprojectionright)) * e) + (jt_right_crtprojectionright))) -> (exists jt_left_crtprojectionrightmod jt_right_crtprojectionrightmod. (jt_left_crtprojectionright)+(n)*jt_left_crtprojectionrightmod=(jt_right_crtprojectionright)+(n)*jt_right_crtprojectionrightmod))

Complete tactic proof in conservative notation

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

48 script commands · 8 reading checkpoints · 3 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 m
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro k
  10. L10
    intro h
02Fix variables and assumptionsL11–16

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

  1. L11
    intro i
  2. L12
    intro w
  3. L13
    intro a
  4. L14
    intro hi
  5. L15
    intro hw
  6. L16
    intro ha
03Establish htL17–20

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

  1. L17
    have ht : ∃ u. ∃ v. ∃ q. BetaAt(b,c,i,u) ∧ (BetaAt(d,e,i,v) ∧ (BetaAt(f,g,i,q) ∧ (ModEq(m,q,u) ∧ ModEq(n,q,v))))Definitions: BetaAt(b,c,i,u)BetaAt(d,e,i,v)BetaAt(f,g,i,q)ModEq(m,q,u)ModEq(n,q,v)Original native command in the exact edition
  2. L18
    specialize h (i)
  3. L19
    apply h
  4. L20
    exact hi
04Separate the logical casesL21–27

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

  1. L21
    cases ht
  2. L22
    cases ht_witness
  3. L23
    cases ht_witness_witness
  4. L24
    cases ht_witness_witness_witness
  5. L25
    cases ht_witness_witness_witness_right
  6. L26
    cases ht_witness_witness_witness_right_right
  7. L27
    cases ht_witness_witness_witness_right_right_right
05Establish houtL28–36

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

  1. L28
    have hout : x2=w
  2. L29
    specialize beta_at_unique (f)
  3. L30
    specialize beta_at_unique (g)
  4. L31
    specialize beta_at_unique (i)
  5. L32
    specialize beta_at_unique (x2)
  6. L33
    specialize beta_at_unique (w)
  7. L34
    apply beta_at_unique
  8. L35
    exact ht_witness_witness_witness_right_right_left
  9. L36
    exact hw
06Establish hinL37–46

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

  1. L37
    have hin : x1=a
  2. L38
    specialize beta_at_unique (d)
  3. L39
    specialize beta_at_unique (e)
  4. L40
    specialize beta_at_unique (i)
  5. L41
    specialize beta_at_unique (x1)
  6. L42
    specialize beta_at_unique (a)
  7. L43
    apply beta_at_unique
  8. L44
    exact ht_witness_witness_witness_right_left
  9. L45
    exact ha
  10. L46
    rewrite hout at ht_witness_witness_witness_right_right_right_right
07Calculate and transport equalitiesL47–47

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L47
    rewrite hin at ht_witness_witness_witness_right_right_right_right
08Use earlier factsL48–48

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

  1. L48
    exact ht_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro f
  8. 0008intro g
  9. 0009intro k
  10. 0010intro h
  11. 0011intro i
  12. 0012intro w
  13. 0013intro a
  14. 0014intro hi
  15. 0015intro hw
  16. 0016intro ha
  17. 0017have ht : ∃ u. ∃ v. ∃ q. BetaAt(b,c,i,u) ∧ (BetaAt(d,e,i,v) ∧ (BetaAt(f,g,i,q) ∧ (ModEq(m,q,u) ∧ ModEq(n,q,v))))
  18. 0018specialize h (i)
  19. 0019apply h
  20. 0020exact hi
  21. 0021cases ht
  22. 0022cases ht_witness
  23. 0023cases ht_witness_witness
  24. 0024cases ht_witness_witness_witness
  25. 0025cases ht_witness_witness_witness_right
  26. 0026cases ht_witness_witness_witness_right_right
  27. 0027cases ht_witness_witness_witness_right_right_right
  28. 0028have hout : x2=w
  29. 0029specialize beta_at_unique (f)
  30. 0030specialize beta_at_unique (g)
  31. 0031specialize beta_at_unique (i)
  32. 0032specialize beta_at_unique (x2)
  33. 0033specialize beta_at_unique (w)
  34. 0034apply beta_at_unique
  35. 0035exact ht_witness_witness_witness_right_right_left
  36. 0036exact hw
  37. 0037have hin : x1=a
  38. 0038specialize beta_at_unique (d)
  39. 0039specialize beta_at_unique (e)
  40. 0040specialize beta_at_unique (i)
  41. 0041specialize beta_at_unique (x1)
  42. 0042specialize beta_at_unique (a)
  43. 0043apply beta_at_unique
  44. 0044exact ht_witness_witness_witness_right_left
  45. 0045exact ha
  46. 0046rewrite hout at ht_witness_witness_witness_right_right_right_right
  47. 0047rewrite hin at ht_witness_witness_witness_right_right_right_right
  48. 0048exact ht_witness_witness_witness_right_right_right_right