BT005B

beta_exclusive_recode_invariant_step

Stable checked-use theorem · independently kernel verified

Combine modulus-product and cross-base congruence updates 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.

Exact expanded PA statement

forall N c b e k P z. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> (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. (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ ((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) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))

Structural proof guide

Combine modulus-product and cross-base congruence updates for an exclusive prefix.

Direct prerequisites: beta_exclusive_accumulated_product_step, beta_exclusive_recode_congruence_step. The authored body proceeds by case analysis (3), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step

Direct dependents

BT005C bounded_beta_exclusive_recode_invariant

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

49 script commands · 14 reading checkpoints · 2 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 (2)
beta exclusive accumulated product stepbeta exclusive recode congruence step
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 hcm
  9. L9
    intro hkN
  10. L10
    intro hP
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hdiv
  2. L12
    intro hcong
  3. L13
    intro hfuture
03Establish hproductL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta exclusive accumulated product step.

  1. L14
    have hproduct : (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1))
  2. L15
    specialize beta_exclusive_accumulated_product_step N
  3. L16
    specialize beta_exclusive_accumulated_product_step c
  4. L17
    specialize beta_exclusive_accumulated_product_step k
  5. L18
    specialize beta_exclusive_accumulated_product_step P
  6. L19
    apply beta_exclusive_accumulated_product_step
  7. L20
    exact hcm
  8. L21
    exact hkN
  9. L22
    exact hP
  10. L23
    exact hdiv
04Use earlier factsL24–24

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

  1. L24
    exact hfuture
05Establish hcodesL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta exclusive recode congruence step.

  1. L25
    have hcodes : 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
  2. L26
    specialize beta_exclusive_recode_congruence_step N
  3. L27
    specialize beta_exclusive_recode_congruence_step c
  4. L28
    specialize beta_exclusive_recode_congruence_step b
  5. L29
    specialize beta_exclusive_recode_congruence_step e
  6. L30
    specialize beta_exclusive_recode_congruence_step k
  7. L31
    specialize beta_exclusive_recode_congruence_step P
  8. L32
    specialize beta_exclusive_recode_congruence_step z
  9. L33
    apply beta_exclusive_recode_congruence_step
  10. L34
    exact hkN
06Use earlier factsL35–38

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

  1. L35
    exact hP
  2. L36
    exact hdiv
  3. L37
    exact hcong
  4. L38
    exact hfuture
07Separate the logical casesL39–41

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

  1. L39
    cases hcodes
  2. L40
    cases hproduct
  3. L41
    cases hproduct_right
08Construct an explicit witnessL42–42

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

  1. L42
    exists x
09Separate the logical casesL43–43

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

  1. L43
    split
10Use earlier factsL44–44

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

  1. L44
    exact hproduct_left
11Separate the logical casesL45–45

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

  1. L45
    split
12Use earlier factsL46–46

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

  1. L46
    exact hproduct_right_left
13Separate the logical casesL47–47

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

  1. L47
    split
14Use earlier factsL48–49

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

  1. L48
    exact hcodes_witness
  2. L49
    exact hproduct_right_right

Library-wide reading audit

Original exact command ledger · 49 lines
  1. 0001intro N
  2. 0002intro c
  3. 0003intro b
  4. 0004intro e
  5. 0005intro k
  6. 0006intro P
  7. 0007intro z
  8. 0008intro hcm
  9. 0009intro hkN
  10. 0010intro hP
  11. 0011intro hdiv
  12. 0012intro hcong
  13. 0013intro hfuture
  14. 0014have hproduct : (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1))
  15. 0015specialize beta_exclusive_accumulated_product_step N
  16. 0016specialize beta_exclusive_accumulated_product_step c
  17. 0017specialize beta_exclusive_accumulated_product_step k
  18. 0018specialize beta_exclusive_accumulated_product_step P
  19. 0019apply beta_exclusive_accumulated_product_step
  20. 0020exact hcm
  21. 0021exact hkN
  22. 0022exact hP
  23. 0023exact hdiv
  24. 0024exact hfuture
  25. 0025have hcodes : 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
  26. 0026specialize beta_exclusive_recode_congruence_step N
  27. 0027specialize beta_exclusive_recode_congruence_step c
  28. 0028specialize beta_exclusive_recode_congruence_step b
  29. 0029specialize beta_exclusive_recode_congruence_step e
  30. 0030specialize beta_exclusive_recode_congruence_step k
  31. 0031specialize beta_exclusive_recode_congruence_step P
  32. 0032specialize beta_exclusive_recode_congruence_step z
  33. 0033apply beta_exclusive_recode_congruence_step
  34. 0034exact hkN
  35. 0035exact hP
  36. 0036exact hdiv
  37. 0037exact hcong
  38. 0038exact hfuture
  39. 0039cases hcodes
  40. 0040cases hproduct
  41. 0041cases hproduct_right
  42. 0042exists x
  43. 0043split
  44. 0044exact hproduct_left
  45. 0045split
  46. 0046exact hproduct_right_left
  47. 0047split
  48. 0048exact hcodes_witness
  49. 0049exact hproduct_right_right