BT005L

beta_product_transport_prefix

Stable checked-use theorem · independently kernel verified

One-way extensional factor-prefix preservation transports Product without changing its trace.

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 b c z e l n. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> (forall i a. (exists h. h + S i = l) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + a) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + a)) -> (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p))))))

Structural proof guide

One-way extensional factor-prefix preservation transports Product without changing its trace.

Direct prerequisites: none. The authored body proceeds by case analysis (10), intermediate claims (1).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT0082 pow_functional BT0090 factorial_functional

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

44 script commands · 17 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.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro z
  4. L4
    intro e
  5. L5
    intro l
  6. L6
    intro n
  7. L7
    intro hproduct
  8. L8
    intro hpres
02Separate the logical casesL9–12

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

  1. L9
    cases hproduct
  2. L10
    cases hproduct_witness
  3. L11
    cases hproduct_witness_witness
  4. L12
    cases hproduct_witness_witness_right
03Construct an explicit witnessL13–14

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

  1. L13
    exists x
  2. L14
    exists x1
04Separate the logical casesL15–15

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

  1. L15
    split
05Use earlier factsL16–16

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

  1. L16
    exact hproduct_witness_witness_left
06Separate the logical casesL17–17

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

  1. L17
    split
07Use earlier factsL18–18

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

  1. L18
    exact hproduct_witness_witness_right_left
08Fix variables and assumptionsL19–20

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

  1. L19
    intro i
  2. L20
    intro hi
09Establish hstepL21–24

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

  1. L21
    have hstep : exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + r) /\ (((exists h. h + S s = S ((S S i) * x1)) /\ exists q. x = q * S ((S S i) * x1) + s) /\ s = r * p)))
  2. L22
    specialize hproduct_witness_witness_right_right i
  3. L23
    apply hproduct_witness_witness_right_right
  4. L24
    exact hi
10Separate the logical casesL25–30

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

  1. L25
    cases hstep
  2. L26
    cases hstep_witness
  3. L27
    cases hstep_witness_witness
  4. L28
    cases hstep_witness_witness_witness
  5. L29
    cases hstep_witness_witness_witness_right
  6. L30
    cases hstep_witness_witness_witness_right_right
11Construct an explicit witnessL31–33

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

  1. L31
    exists x2
  2. L32
    exists x3
  3. L33
    exists x4
12Separate the logical casesL34–34

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

  1. L34
    split
13Use earlier factsL35–39

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

  1. L35
    specialize hpres i
  2. L36
    specialize hpres x2
  3. L37
    apply hpres
  4. L38
    exact hi
  5. L39
    exact hstep_witness_witness_witness_left
14Separate the logical casesL40–40

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

  1. L40
    split
15Use earlier factsL41–41

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

  1. L41
    exact hstep_witness_witness_witness_right_left
16Separate the logical casesL42–42

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

  1. L42
    split
17Use earlier factsL43–44

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

  1. L43
    exact hstep_witness_witness_witness_right_right_left
  2. L44
    exact hstep_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 44 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro e
  5. 0005intro l
  6. 0006intro n
  7. 0007intro hproduct
  8. 0008intro hpres
  9. 0009cases hproduct
  10. 0010cases hproduct_witness
  11. 0011cases hproduct_witness_witness
  12. 0012cases hproduct_witness_witness_right
  13. 0013exists x
  14. 0014exists x1
  15. 0015split
  16. 0016exact hproduct_witness_witness_left
  17. 0017split
  18. 0018exact hproduct_witness_witness_right_left
  19. 0019intro i
  20. 0020intro hi
  21. 0021have hstep : exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + r) /\ (((exists h. h + S s = S ((S S i) * x1)) /\ exists q. x = q * S ((S S i) * x1) + s) /\ s = r * p)))
  22. 0022specialize hproduct_witness_witness_right_right i
  23. 0023apply hproduct_witness_witness_right_right
  24. 0024exact hi
  25. 0025cases hstep
  26. 0026cases hstep_witness
  27. 0027cases hstep_witness_witness
  28. 0028cases hstep_witness_witness_witness
  29. 0029cases hstep_witness_witness_witness_right
  30. 0030cases hstep_witness_witness_witness_right_right
  31. 0031exists x2
  32. 0032exists x3
  33. 0033exists x4
  34. 0034split
  35. 0035specialize hpres i
  36. 0036specialize hpres x2
  37. 0037apply hpres
  38. 0038exact hi
  39. 0039exact hstep_witness_witness_witness_left
  40. 0040split
  41. 0041exact hstep_witness_witness_witness_right_left
  42. 0042split
  43. 0043exact hstep_witness_witness_witness_right_right_left
  44. 0044exact hstep_witness_witness_witness_right_right_right