BT005A · Bertrand theorem

beta_exclusive_recode_congruence_step

Stable checked-use theorem · independently kernel verified

Add the next source value to a target-base CRT code for an exclusive prefix.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ N. ∀ c. ∀ b. ∀ e. ∀ k. ∀ P. ∀ z. Lt(k,N) → ¬P = 0 → (∀ x. Lt(x,k) → Dvd(S (S x · c),P)) → (∀ x. ∀ y. Lt(x,k) → BetaAt(b,e,x,y) → ModEq(S (S x · c),z,y)) → (∀ x. Le(k,x) → Le(x,N) → Coprime(P,S (S x · c))) → ∃ x. ∀ y. ∀ n. Lt(y,S k) → BetaAt(b,e,y,n) → ModEq(S (S y · c),x,n)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0003 Dvd PD0005 Coprime PD0008 ModEq PD0013 BetaAt

12 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd PD0005 Coprime PD0008 ModEq PD0013 BetaAt

12 occurrences

Exact expanded native-PA statement
forall N c b e k P z. (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> exists z2. forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v

Proof neighborhood

Direct theorem prerequisites

BT003Y beta_modulus_nonzero BT000E le_refl BT0019 lt_to_le BT004U binary_crt_fold_step BT0041 beta_at_exists BT0042 beta_at_unique BT0017 le_of_succ_le_succ BT001C le_eq_or_lt

Direct theorem dependents

BT005B beta_exclusive_recode_invariant_step

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

92 script commands · 21 reading checkpoints · 11 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 (8)
beta modulus nonzerole refllt to lebinary crt fold stepbeta at existsbeta at uniquele of succ le succle eq or lt
01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro c
  3. L3
    intro b
  4. L4
    intro e
  5. L5
    intro k
  6. L6
    intro P
  7. L7
    intro z
  8. L8
    intro hkN
  9. L9
    intro hP
  10. L10
    intro hdiv
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hcong
  2. L12
    intro hfuture
03Establish hnewL13–16

Establish this local claim before using it. It is not an additional assumption.

  1. L13
    have hnew : ~(S ((S k) * c) = 0)
  2. L14
    specialize beta_modulus_nonzero c
  3. L15
    specialize beta_modulus_nonzero k
  4. L16
    exact beta_modulus_nonzero
04Establish hkboundL17–21

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

  1. L17
    have hkbound : Le(k,N)Definitions: Le(k,N)Original native command in the exact edition
  2. L18
    specialize lt_to_le k
  3. L19
    specialize lt_to_le N
  4. L20
    apply lt_to_le
  5. L21
    exact hkN
05Establish hcopL22–27

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

  1. L22
    have hcop : Coprime(P,S (S k · c))Definitions: Coprime(P,S (S k · c))Original native command in the exact edition
  2. L23
    specialize hfuture k
  3. L24
    apply hfuture
  4. L25
    specialize le_refl k
  5. L26
    exact le_refl
  6. L27
    exact hkbound
06Establish hvalueL28–32

Establish this local claim before using it. It is not an additional assumption.

  1. L28
    have hvalue : ∃ a. BetaAt(b,e,k,a)Definitions: BetaAt(b,e,k,a)Original native command in the exact edition
  2. L29
    specialize beta_at_exists b
  3. L30
    specialize beta_at_exists e
  4. L31
    specialize beta_at_exists k
  5. L32
    exact beta_at_exists
07Separate the logical casesL33–33

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

  1. L33
    cases hvalue
08Establish hfoldL34–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary crt fold step.

  1. L34
    have hfold : ∃ z2. (∀ y. ∀ n. Dvd(y,P) → ModEq(y,z,n) → ModEq(y,z2,n)) ∧ ModEq(S (S k · c),z2,x)Definitions: Dvd(y,P)ModEq(y,z,n)ModEq(y,z2,n)ModEq(S (S k · c),z2,x)Original native command in the exact edition
  2. L35
    specialize binary_crt_fold_step P
  3. L36
    specialize binary_crt_fold_step (S ((S k) * c))
  4. L37
    specialize binary_crt_fold_step z
  5. L38
    specialize binary_crt_fold_step x
  6. L39
    apply binary_crt_fold_step
  7. L40
    exact hP
  8. L41
    exact hnew
  9. L42
    exact hcop
09Separate the logical casesL43–44

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

  1. L43
    cases hfold
  2. L44
    cases hfold_witness
10Construct an explicit witnessL45–45

Supply the displayed value, then prove that it has the required property.

  1. L45
    exists x1
11Fix variables and assumptionsL46–49

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

  1. L46
    intro i
  2. L47
    intro a
  3. L48
    intro hi
  4. L49
    intro hati
12Establish hikL50–54

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

  1. L50
  2. L51
    specialize le_of_succ_le_succ i
  3. L52
    specialize le_of_succ_le_succ k
  4. L53
    apply le_of_succ_le_succ
  5. L54
    exact hi
13Establish hsplitL55–59

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L55
    have hsplit : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L56
    specialize le_eq_or_lt i
  3. L57
    specialize le_eq_or_lt k
  4. L58
    apply le_eq_or_lt
  5. L59
    exact hik
14Separate the logical casesL60–60

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

  1. L60
    cases hsplit
15Establish hati_newL61–64

Establish this local claim before using it. It is not an additional assumption.

  1. L61
    have hati_new : BetaAt(b,e,k,a)Definitions: BetaAt(b,e,k,a)Original native command in the exact edition
  2. L62
    rewrite <- hsplit_left
  3. L63
    rewrite <- hsplit_left
  4. L64
    exact hati
16Establish haeqL65–74

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

  1. L65
    have haeq : a = x
  2. L66
    specialize beta_at_unique b
  3. L67
    specialize beta_at_unique e
  4. L68
    specialize beta_at_unique k
  5. L69
    specialize beta_at_unique a
  6. L70
    specialize beta_at_unique x
  7. L71
    apply beta_at_unique
  8. L72
    exact hati_new
  9. L73
    exact hvalue_witness
  10. L74
    rewrite hsplit_left
17Calculate and transport equalitiesL75–76

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

  1. L75
    rewrite hsplit_left
  2. L76
    rewrite haeq
18Use earlier factsL77–77

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

  1. L77
    exact hfold_witness_right
19Establish hmiPL78–81

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

  1. L78
    have hmiP : Dvd(S (S i · c),P)Definitions: Dvd(S (S i · c),P)Original native command in the exact edition
  2. L79
    specialize hdiv i
  3. L80
    apply hdiv
  4. L81
    exact hsplit_right
20Establish hzoldL82–91

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

  1. L82
    have hzold : ModEq(S (S i · c),z,a)Definitions: ModEq(S (S i · c),z,a)Original native command in the exact edition
  2. L83
    specialize hcong i
  3. L84
    specialize hcong a
  4. L85
    apply hcong
  5. L86
    exact hsplit_right
  6. L87
    exact hati
  7. L88
    specialize hfold_witness_left (S ((S i) * c))
  8. L89
    specialize hfold_witness_left a
  9. L90
    apply hfold_witness_left
  10. L91
    exact hmiP
21Use earlier factsL92–92

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

  1. L92
    exact hzold

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro N
  2. 0002intro c
  3. 0003intro b
  4. 0004intro e
  5. 0005intro k
  6. 0006intro P
  7. 0007intro z
  8. 0008intro hkN
  9. 0009intro hP
  10. 0010intro hdiv
  11. 0011intro hcong
  12. 0012intro hfuture
  13. 0013have hnew : ~(S ((S k) * c) = 0)
  14. 0014specialize beta_modulus_nonzero c
  15. 0015specialize beta_modulus_nonzero k
  16. 0016exact beta_modulus_nonzero
  17. 0017have hkbound : Le(k,N)
    Exact native replay linehave hkbound : exists h. h + k = N
  18. 0018specialize lt_to_le k
  19. 0019specialize lt_to_le N
  20. 0020apply lt_to_le
  21. 0021exact hkN
  22. 0022have hcop : Coprime(P,S (S k · c))
    Exact native replay linehave hcop : forall d. (exists u. P = d * u) -> (exists v. S ((S k) * c) = d * v) -> d = 1
  23. 0023specialize hfuture k
  24. 0024apply hfuture
  25. 0025specialize le_refl k
  26. 0026exact le_refl
  27. 0027exact hkbound
  28. 0028have hvalue : ∃ a. BetaAt(b,e,k,a)
    Exact native replay linehave hvalue : exists a. ((exists h. h + S a = S ((S k) * e)) /\ exists q. b = q * S ((S k) * e) + a)
  29. 0029specialize beta_at_exists b
  30. 0030specialize beta_at_exists e
  31. 0031specialize beta_at_exists k
  32. 0032exact beta_at_exists
  33. 0033cases hvalue
  34. 0034have hfold : ∃ z2. (∀ y. ∀ n. Dvd(y,P) → ModEq(y,z,n) → ModEq(y,z2,n)) ∧ ModEq(S (S k · c),z2,x)
    Exact native replay linehave hfold : exists z2. ((forall m a. (exists q. P = m * q) -> (exists u v. z + m * u = a + m * v) -> exists r s. z2 + m * r = a + m * s) /\ exists q r. z2 + S ((S k) * c) * q = x + S ((S k) * c) * r)
  35. 0035specialize binary_crt_fold_step P
  36. 0036specialize binary_crt_fold_step (S ((S k) * c))
  37. 0037specialize binary_crt_fold_step z
  38. 0038specialize binary_crt_fold_step x
  39. 0039apply binary_crt_fold_step
  40. 0040exact hP
  41. 0041exact hnew
  42. 0042exact hcop
  43. 0043cases hfold
  44. 0044cases hfold_witness
  45. 0045exists x1
  46. 0046intro i
  47. 0047intro a
  48. 0048intro hi
  49. 0049intro hati
  50. 0050have hik : Le(i,k)
    Exact native replay linehave hik : exists r. r + i = k
  51. 0051specialize le_of_succ_le_succ i
  52. 0052specialize le_of_succ_le_succ k
  53. 0053apply le_of_succ_le_succ
  54. 0054exact hi
  55. 0055have hsplit : i = k ∨ Lt(i,k)
    Exact native replay linehave hsplit : i = k \/ exists r. r + S i = k
  56. 0056specialize le_eq_or_lt i
  57. 0057specialize le_eq_or_lt k
  58. 0058apply le_eq_or_lt
  59. 0059exact hik
  60. 0060cases hsplit
  61. 0061have hati_new : BetaAt(b,e,k,a)
    Exact native replay linehave hati_new : ((exists h. h + S a = S ((S k) * e)) /\ exists q. b = q * S ((S k) * e) + a)
  62. 0062rewrite <- hsplit_left
  63. 0063rewrite <- hsplit_left
  64. 0064exact hati
  65. 0065have haeq : a = x
  66. 0066specialize beta_at_unique b
  67. 0067specialize beta_at_unique e
  68. 0068specialize beta_at_unique k
  69. 0069specialize beta_at_unique a
  70. 0070specialize beta_at_unique x
  71. 0071apply beta_at_unique
  72. 0072exact hati_new
  73. 0073exact hvalue_witness
  74. 0074rewrite hsplit_left
  75. 0075rewrite hsplit_left
  76. 0076rewrite haeq
  77. 0077exact hfold_witness_right
  78. 0078have hmiP : Dvd(S (S i · c),P)
    Exact native replay linehave hmiP : exists q. P = S ((S i) * c) * q
  79. 0079specialize hdiv i
  80. 0080apply hdiv
  81. 0081exact hsplit_right
  82. 0082have hzold : ModEq(S (S i · c),z,a)
    Exact native replay linehave hzold : exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v
  83. 0083specialize hcong i
  84. 0084specialize hcong a
  85. 0085apply hcong
  86. 0086exact hsplit_right
  87. 0087exact hati
  88. 0088specialize hfold_witness_left (S ((S i) * c))
  89. 0089specialize hfold_witness_left a
  90. 0090apply hfold_witness_left
  91. 0091exact hmiP
  92. 0092exact hzold