JT003B

jordan_crt_component_recovery

Equal output tuples recover equal canonical input components, not equal raw beta codes.

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. ∀ f. ∀ g. ∀ h. ∀ s. ∀ k. BetaPrefixInto(b,c,k,n) → BetaPrefixInto(d,e,k,n) → JordanTupleCongruence(n,f,g,b,c,k) → JordanTupleCongruence(n,h,s,d,e,k) → IntegerVectorZero(f,g,h,s,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) · 2BetaPrefixInto(b,c,l,B) · 2JordanTupleCongruence(n,b,c,d,e,k) · 3

Actual proof prerequisites

jordan_tuple_bounded_congruence_equaljordan_tuple_congruence_transjordan_tuple_congruence_symmjordan_tuple_equal_congruence
Original expanded first-order statement 
forall n b c d e f g h s k. (forall jt_index_recoverleft. (exists jt_gap_recoverleftindex. jt_gap_recoverleftindex+S (jt_index_recoverleft)=(k)) -> exists jt_value_recoverleft. ((((exists fs_h_jt_recoverleftat. fs_h_jt_recoverleftat + S (jt_value_recoverleft) = S ((S (jt_index_recoverleft)) * c)) /\ exists fs_q_jt_recoverleftat. b = fs_q_jt_recoverleftat * S ((S (jt_index_recoverleft)) * c) + (jt_value_recoverleft))) /\ (exists jt_gap_recoverleftvalue. jt_gap_recoverleftvalue+S (jt_value_recoverleft)=(n)))) -> (forall jt_index_recoverright. (exists jt_gap_recoverrightindex. jt_gap_recoverrightindex+S (jt_index_recoverright)=(k)) -> exists jt_value_recoverright. ((((exists fs_h_jt_recoverrightat. fs_h_jt_recoverrightat + S (jt_value_recoverright) = S ((S (jt_index_recoverright)) * e)) /\ exists fs_q_jt_recoverrightat. d = fs_q_jt_recoverrightat * S ((S (jt_index_recoverright)) * e) + (jt_value_recoverright))) /\ (exists jt_gap_recoverrightvalue. jt_gap_recoverrightvalue+S (jt_value_recoverright)=(n)))) -> (forall jt_index_recoverfirst jt_left_recoverfirst jt_right_recoverfirst. (exists jt_gap_recoverfirstindex. jt_gap_recoverfirstindex+S (jt_index_recoverfirst)=(k)) -> (((exists fs_h_jt_recoverfirstleft. fs_h_jt_recoverfirstleft + S (jt_left_recoverfirst) = S ((S (jt_index_recoverfirst)) * g)) /\ exists fs_q_jt_recoverfirstleft. f = fs_q_jt_recoverfirstleft * S ((S (jt_index_recoverfirst)) * g) + (jt_left_recoverfirst))) -> (((exists fs_h_jt_recoverfirstright. fs_h_jt_recoverfirstright + S (jt_right_recoverfirst) = S ((S (jt_index_recoverfirst)) * c)) /\ exists fs_q_jt_recoverfirstright. b = fs_q_jt_recoverfirstright * S ((S (jt_index_recoverfirst)) * c) + (jt_right_recoverfirst))) -> (exists jt_left_recoverfirstmod jt_right_recoverfirstmod. (jt_left_recoverfirst)+(n)*jt_left_recoverfirstmod=(jt_right_recoverfirst)+(n)*jt_right_recoverfirstmod)) -> (forall jt_index_recoversecond jt_left_recoversecond jt_right_recoversecond. (exists jt_gap_recoversecondindex. jt_gap_recoversecondindex+S (jt_index_recoversecond)=(k)) -> (((exists fs_h_jt_recoversecondleft. fs_h_jt_recoversecondleft + S (jt_left_recoversecond) = S ((S (jt_index_recoversecond)) * s)) /\ exists fs_q_jt_recoversecondleft. h = fs_q_jt_recoversecondleft * S ((S (jt_index_recoversecond)) * s) + (jt_left_recoversecond))) -> (((exists fs_h_jt_recoversecondright. fs_h_jt_recoversecondright + S (jt_right_recoversecond) = S ((S (jt_index_recoversecond)) * e)) /\ exists fs_q_jt_recoversecondright. d = fs_q_jt_recoversecondright * S ((S (jt_index_recoversecond)) * e) + (jt_right_recoversecond))) -> (exists jt_left_recoversecondmod jt_right_recoversecondmod. (jt_left_recoversecond)+(n)*jt_left_recoversecondmod=(jt_right_recoversecond)+(n)*jt_right_recoversecondmod)) -> (forall jt_index_recoveroutput jt_left_recoveroutput jt_right_recoveroutput. (exists jt_gap_recoveroutputindex. jt_gap_recoveroutputindex+S (jt_index_recoveroutput)=(k)) -> (((exists fs_h_jt_recoveroutputleft. fs_h_jt_recoveroutputleft + S (jt_left_recoveroutput) = S ((S (jt_index_recoveroutput)) * g)) /\ exists fs_q_jt_recoveroutputleft. f = fs_q_jt_recoveroutputleft * S ((S (jt_index_recoveroutput)) * g) + (jt_left_recoveroutput))) -> (((exists fs_h_jt_recoveroutputright. fs_h_jt_recoveroutputright + S (jt_right_recoveroutput) = S ((S (jt_index_recoveroutput)) * s)) /\ exists fs_q_jt_recoveroutputright. h = fs_q_jt_recoveroutputright * S ((S (jt_index_recoveroutput)) * s) + (jt_right_recoveroutput))) -> jt_left_recoveroutput=jt_right_recoveroutput) -> (forall jt_index_recoverinputs jt_left_recoverinputs jt_right_recoverinputs. (exists jt_gap_recoverinputsindex. jt_gap_recoverinputsindex+S (jt_index_recoverinputs)=(k)) -> (((exists fs_h_jt_recoverinputsleft. fs_h_jt_recoverinputsleft + S (jt_left_recoverinputs) = S ((S (jt_index_recoverinputs)) * c)) /\ exists fs_q_jt_recoverinputsleft. b = fs_q_jt_recoverinputsleft * S ((S (jt_index_recoverinputs)) * c) + (jt_left_recoverinputs))) -> (((exists fs_h_jt_recoverinputsright. fs_h_jt_recoverinputsright + S (jt_right_recoverinputs) = S ((S (jt_index_recoverinputs)) * e)) /\ exists fs_q_jt_recoverinputsright. d = fs_q_jt_recoverinputsright * S ((S (jt_index_recoverinputs)) * e) + (jt_right_recoverinputs))) -> jt_left_recoverinputs=jt_right_recoverinputs)

Complete tactic proof in conservative notation

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

61 script commands · 7 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 (4)
jordan tuple congruence transjordan tuple equal congruencejordan tuple bounded congruence equaljordan tuple congruence 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 f
  7. L7
    intro g
  8. L8
    intro h
  9. L9
    intro s
  10. L10
    intro k
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hb
  2. L12
    intro hd
  3. L13
    intro hleft
  4. L14
    intro hright
  5. L15
    intro heq
03Establish hmiddleL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple congruence trans.

  1. L16
    have hmiddle : JordanTupleCongruence(n,f,g,d,e,k)Definitions: JordanTupleCongruence(n,f,g,d,e,k)Original native command in the exact edition
  2. L17
    specialize jordan_tuple_congruence_trans (n)
  3. L18
    specialize jordan_tuple_congruence_trans (f)
  4. L19
    specialize jordan_tuple_congruence_trans (g)
  5. L20
    specialize jordan_tuple_congruence_trans (h)
  6. L21
    specialize jordan_tuple_congruence_trans (s)
  7. L22
    specialize jordan_tuple_congruence_trans (d)
  8. L23
    specialize jordan_tuple_congruence_trans (e)
  9. L24
    specialize jordan_tuple_congruence_trans (k)
  10. L25
    apply jordan_tuple_congruence_trans
04Use earlier factsL26–35

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

  1. L26
    specialize jordan_tuple_equal_congruence (n)
  2. L27
    specialize jordan_tuple_equal_congruence (f)
  3. L28
    specialize jordan_tuple_equal_congruence (g)
  4. L29
    specialize jordan_tuple_equal_congruence (h)
  5. L30
    specialize jordan_tuple_equal_congruence (s)
  6. L31
    specialize jordan_tuple_equal_congruence (k)
  7. L32
    apply jordan_tuple_equal_congruence
  8. L33
    exact heq
  9. L34
    exact hright
  10. L35
    specialize jordan_tuple_bounded_congruence_equal (n)
05Use earlier factsL36–45

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

  1. L36
    specialize jordan_tuple_bounded_congruence_equal (b)
  2. L37
    specialize jordan_tuple_bounded_congruence_equal (c)
  3. L38
    specialize jordan_tuple_bounded_congruence_equal (d)
  4. L39
    specialize jordan_tuple_bounded_congruence_equal (e)
  5. L40
    specialize jordan_tuple_bounded_congruence_equal (k)
  6. L41
    apply jordan_tuple_bounded_congruence_equal
  7. L42
    exact hb
  8. L43
    exact hd
  9. L44
    specialize jordan_tuple_congruence_trans (n)
  10. L45
    specialize jordan_tuple_congruence_trans (b)
06Use earlier factsL46–55

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

  1. L46
    specialize jordan_tuple_congruence_trans (c)
  2. L47
    specialize jordan_tuple_congruence_trans (f)
  3. L48
    specialize jordan_tuple_congruence_trans (g)
  4. L49
    specialize jordan_tuple_congruence_trans (d)
  5. L50
    specialize jordan_tuple_congruence_trans (e)
  6. L51
    specialize jordan_tuple_congruence_trans (k)
  7. L52
    apply jordan_tuple_congruence_trans
  8. L53
    specialize jordan_tuple_congruence_symm (n)
  9. L54
    specialize jordan_tuple_congruence_symm (f)
  10. L55
    specialize jordan_tuple_congruence_symm (g)
07Use earlier factsL56–61

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

  1. L56
    specialize jordan_tuple_congruence_symm (b)
  2. L57
    specialize jordan_tuple_congruence_symm (c)
  3. L58
    specialize jordan_tuple_congruence_symm (k)
  4. L59
    apply jordan_tuple_congruence_symm
  5. L60
    exact hleft
  6. L61
    exact hmiddle

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009intro s
  10. 0010intro k
  11. 0011intro hb
  12. 0012intro hd
  13. 0013intro hleft
  14. 0014intro hright
  15. 0015intro heq
  16. 0016have hmiddle : JordanTupleCongruence(n,f,g,d,e,k)
  17. 0017specialize jordan_tuple_congruence_trans (n)
  18. 0018specialize jordan_tuple_congruence_trans (f)
  19. 0019specialize jordan_tuple_congruence_trans (g)
  20. 0020specialize jordan_tuple_congruence_trans (h)
  21. 0021specialize jordan_tuple_congruence_trans (s)
  22. 0022specialize jordan_tuple_congruence_trans (d)
  23. 0023specialize jordan_tuple_congruence_trans (e)
  24. 0024specialize jordan_tuple_congruence_trans (k)
  25. 0025apply jordan_tuple_congruence_trans
  26. 0026specialize jordan_tuple_equal_congruence (n)
  27. 0027specialize jordan_tuple_equal_congruence (f)
  28. 0028specialize jordan_tuple_equal_congruence (g)
  29. 0029specialize jordan_tuple_equal_congruence (h)
  30. 0030specialize jordan_tuple_equal_congruence (s)
  31. 0031specialize jordan_tuple_equal_congruence (k)
  32. 0032apply jordan_tuple_equal_congruence
  33. 0033exact heq
  34. 0034exact hright
  35. 0035specialize jordan_tuple_bounded_congruence_equal (n)
  36. 0036specialize jordan_tuple_bounded_congruence_equal (b)
  37. 0037specialize jordan_tuple_bounded_congruence_equal (c)
  38. 0038specialize jordan_tuple_bounded_congruence_equal (d)
  39. 0039specialize jordan_tuple_bounded_congruence_equal (e)
  40. 0040specialize jordan_tuple_bounded_congruence_equal (k)
  41. 0041apply jordan_tuple_bounded_congruence_equal
  42. 0042exact hb
  43. 0043exact hd
  44. 0044specialize jordan_tuple_congruence_trans (n)
  45. 0045specialize jordan_tuple_congruence_trans (b)
  46. 0046specialize jordan_tuple_congruence_trans (c)
  47. 0047specialize jordan_tuple_congruence_trans (f)
  48. 0048specialize jordan_tuple_congruence_trans (g)
  49. 0049specialize jordan_tuple_congruence_trans (d)
  50. 0050specialize jordan_tuple_congruence_trans (e)
  51. 0051specialize jordan_tuple_congruence_trans (k)
  52. 0052apply jordan_tuple_congruence_trans
  53. 0053specialize jordan_tuple_congruence_symm (n)
  54. 0054specialize jordan_tuple_congruence_symm (f)
  55. 0055specialize jordan_tuple_congruence_symm (g)
  56. 0056specialize jordan_tuple_congruence_symm (b)
  57. 0057specialize jordan_tuple_congruence_symm (c)
  58. 0058specialize jordan_tuple_congruence_symm (k)
  59. 0059apply jordan_tuple_congruence_symm
  60. 0060exact hleft
  61. 0061exact hmiddle