BT0090 · Bertrand theorem

factorial_functional

Stable checked-use theorem · independently kernel verified

The beta-coded relational factorial has a unique value.

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. ∀ z. ∀ w. Factorial(n,z) → Factorial(n,w) → z = w

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

PD0023 Factorial

2 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0014 Product

4 occurrences

Exact expanded native-PA statement
forall n z w. (exists ff_b_functional_l ff_c_functional_l. ((forall ff_i_functional_l_range. (exists ff_lt_functional_l_range_bound. ff_lt_functional_l_range_bound + S ff_i_functional_l_range = n) -> (((exists ff_h_functional_l_range_decoded. ff_h_functional_l_range_decoded + S (1 + ff_i_functional_l_range) = S ((S (ff_i_functional_l_range)) * ff_c_functional_l)) /\ exists ff_q_functional_l_range_decoded. ff_b_functional_l = ff_q_functional_l_range_decoded * S ((S (ff_i_functional_l_range)) * ff_c_functional_l) + (1 + ff_i_functional_l_range)))) /\ (exists ff_u_functional_l_product ff_v_functional_l_product. ((((exists ff_h_functional_l_product_start. ff_h_functional_l_product_start + S (1) = S ((S (0)) * ff_v_functional_l_product)) /\ exists ff_q_functional_l_product_start. ff_u_functional_l_product = ff_q_functional_l_product_start * S ((S (0)) * ff_v_functional_l_product) + (1))) /\ ((((exists ff_h_functional_l_product_terminal. ff_h_functional_l_product_terminal + S (z) = S ((S (n)) * ff_v_functional_l_product)) /\ exists ff_q_functional_l_product_terminal. ff_u_functional_l_product = ff_q_functional_l_product_terminal * S ((S (n)) * ff_v_functional_l_product) + (z))) /\ forall ff_i_functional_l_product. (exists ff_lt_functional_l_product_bound. ff_lt_functional_l_product_bound + S ff_i_functional_l_product = n) -> exists ff_p_functional_l_product ff_r_functional_l_product ff_s_functional_l_product. ((((exists ff_h_functional_l_product_factor. ff_h_functional_l_product_factor + S (ff_p_functional_l_product) = S ((S (ff_i_functional_l_product)) * ff_c_functional_l)) /\ exists ff_q_functional_l_product_factor. ff_b_functional_l = ff_q_functional_l_product_factor * S ((S (ff_i_functional_l_product)) * ff_c_functional_l) + (ff_p_functional_l_product))) /\ ((((exists ff_h_functional_l_product_partial. ff_h_functional_l_product_partial + S (ff_r_functional_l_product) = S ((S (ff_i_functional_l_product)) * ff_v_functional_l_product)) /\ exists ff_q_functional_l_product_partial. ff_u_functional_l_product = ff_q_functional_l_product_partial * S ((S (ff_i_functional_l_product)) * ff_v_functional_l_product) + (ff_r_functional_l_product))) /\ ((((exists ff_h_functional_l_product_successor. ff_h_functional_l_product_successor + S (ff_s_functional_l_product) = S ((S (S ff_i_functional_l_product)) * ff_v_functional_l_product)) /\ exists ff_q_functional_l_product_successor. ff_u_functional_l_product = ff_q_functional_l_product_successor * S ((S (S ff_i_functional_l_product)) * ff_v_functional_l_product) + (ff_s_functional_l_product))) /\ ff_s_functional_l_product = ff_r_functional_l_product * ff_p_functional_l_product)))))))) -> (exists ff_b_functional_r ff_c_functional_r. ((forall ff_i_functional_r_range. (exists ff_lt_functional_r_range_bound. ff_lt_functional_r_range_bound + S ff_i_functional_r_range = n) -> (((exists ff_h_functional_r_range_decoded. ff_h_functional_r_range_decoded + S (1 + ff_i_functional_r_range) = S ((S (ff_i_functional_r_range)) * ff_c_functional_r)) /\ exists ff_q_functional_r_range_decoded. ff_b_functional_r = ff_q_functional_r_range_decoded * S ((S (ff_i_functional_r_range)) * ff_c_functional_r) + (1 + ff_i_functional_r_range)))) /\ (exists ff_u_functional_r_product ff_v_functional_r_product. ((((exists ff_h_functional_r_product_start. ff_h_functional_r_product_start + S (1) = S ((S (0)) * ff_v_functional_r_product)) /\ exists ff_q_functional_r_product_start. ff_u_functional_r_product = ff_q_functional_r_product_start * S ((S (0)) * ff_v_functional_r_product) + (1))) /\ ((((exists ff_h_functional_r_product_terminal. ff_h_functional_r_product_terminal + S (w) = S ((S (n)) * ff_v_functional_r_product)) /\ exists ff_q_functional_r_product_terminal. ff_u_functional_r_product = ff_q_functional_r_product_terminal * S ((S (n)) * ff_v_functional_r_product) + (w))) /\ forall ff_i_functional_r_product. (exists ff_lt_functional_r_product_bound. ff_lt_functional_r_product_bound + S ff_i_functional_r_product = n) -> exists ff_p_functional_r_product ff_r_functional_r_product ff_s_functional_r_product. ((((exists ff_h_functional_r_product_factor. ff_h_functional_r_product_factor + S (ff_p_functional_r_product) = S ((S (ff_i_functional_r_product)) * ff_c_functional_r)) /\ exists ff_q_functional_r_product_factor. ff_b_functional_r = ff_q_functional_r_product_factor * S ((S (ff_i_functional_r_product)) * ff_c_functional_r) + (ff_p_functional_r_product))) /\ ((((exists ff_h_functional_r_product_partial. ff_h_functional_r_product_partial + S (ff_r_functional_r_product) = S ((S (ff_i_functional_r_product)) * ff_v_functional_r_product)) /\ exists ff_q_functional_r_product_partial. ff_u_functional_r_product = ff_q_functional_r_product_partial * S ((S (ff_i_functional_r_product)) * ff_v_functional_r_product) + (ff_r_functional_r_product))) /\ ((((exists ff_h_functional_r_product_successor. ff_h_functional_r_product_successor + S (ff_s_functional_r_product) = S ((S (S ff_i_functional_r_product)) * ff_v_functional_r_product)) /\ exists ff_q_functional_r_product_successor. ff_u_functional_r_product = ff_q_functional_r_product_successor * S ((S (S ff_i_functional_r_product)) * ff_v_functional_r_product) + (ff_s_functional_r_product))) /\ ff_s_functional_r_product = ff_r_functional_r_product * ff_p_functional_r_product)))))))) -> z = w

Proof neighborhood

Direct theorem prerequisites

BT0088 beta_range_transport_entry BT005L beta_product_transport_prefix BT005G beta_product_functional

Direct theorem dependents

BT00RP prime_factorial_valuation_succ BT00TX choose_factorial_bridge

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

55 script commands · 9 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.

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 (3)
beta range transport entrybeta product transport prefixbeta product functional
01Fix variables and assumptionsL1–5

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

  1. L1
    intro n
  2. L2
    intro z
  3. L3
    intro w
  4. L4
    intro hz
  5. L5
    intro hw
02Separate the logical casesL6–11

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

  1. L6
    cases hz
  2. L7
    cases hz_witness
  3. L8
    cases hz_witness_witness
  4. L9
    cases hw
  5. L10
    cases hw_witness
  6. L11
    cases hw_witness_witness
03Establish htransportL12–21

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

  1. L12
    have htransport : Product(x2,x3,n,z)Definitions: Product(x2,x3,n,z)Original native command in the exact edition
  2. L13
    specialize beta_product_transport_prefix x
  3. L14
    specialize beta_product_transport_prefix x1
  4. L15
    specialize beta_product_transport_prefix x2
  5. L16
    specialize beta_product_transport_prefix x3
  6. L17
    specialize beta_product_transport_prefix n
  7. L18
    specialize beta_product_transport_prefix z
  8. L19
    apply beta_product_transport_prefix
  9. L20
    exact hz_witness_witness_right
  10. L21
    intro i
04Fix variables and assumptionsL22–24

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

  1. L22
    intro p
  2. L23
    intro hi
  3. L24
    intro hp
05Use earlier factsL25–30

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

  1. L25
    specialize beta_range_transport_entry x
  2. L26
    specialize beta_range_transport_entry x1
  3. L27
    specialize beta_range_transport_entry x2
  4. L28
    specialize beta_range_transport_entry x3
  5. L29
    specialize beta_range_transport_entry 1
  6. L30
    specialize beta_range_transport_entry n
06Establish hentriesL31–39

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

  1. L31
    have hentries : ∀ i. ∀ p. Lt(i,n) → BetaAt(x,x1,i,p) → BetaAt(x2,x3,i,p)Definitions: Lt(i,n)BetaAt(x,x1,i,p)BetaAt(x2,x3,i,p)Original native command in the exact edition
  2. L32
    apply beta_range_transport_entry
  3. L33
    exact hz_witness_witness_left
  4. L34
    exact hw_witness_witness_left
  5. L35
    specialize hentries i
  6. L36
    specialize hentries p
  7. L37
    apply hentries
  8. L38
    exact hi
  9. L39
    exact hp
07Separate the logical casesL40–43

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

  1. L40
    cases htransport
  2. L41
    cases htransport_witness
  3. L42
    cases hw_witness_witness_right
  4. L43
    cases hw_witness_witness_right_witness
08Use earlier factsL44–53

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

  1. L44
    specialize beta_product_functional x2
  2. L45
    specialize beta_product_functional x3
  3. L46
    specialize beta_product_functional n
  4. L47
    specialize beta_product_functional z
  5. L48
    specialize beta_product_functional x4
  6. L49
    specialize beta_product_functional x5
  7. L50
    specialize beta_product_functional w
  8. L51
    specialize beta_product_functional x6
  9. L52
    specialize beta_product_functional x7
  10. L53
    apply beta_product_functional
09Use earlier factsL54–55

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

  1. L54
    exact htransport_witness_witness
  2. L55
    exact hw_witness_witness_right_witness_witness

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro n
  2. 0002intro z
  3. 0003intro w
  4. 0004intro hz
  5. 0005intro hw
  6. 0006cases hz
  7. 0007cases hz_witness
  8. 0008cases hz_witness_witness
  9. 0009cases hw
  10. 0010cases hw_witness
  11. 0011cases hw_witness_witness
  12. 0012have htransport : Product(x2,x3,n,z)
    Exact native replay linehave htransport : exists ff_u_factorial_transport ff_v_factorial_transport. ((((exists ff_h_factorial_transport_start. ff_h_factorial_transport_start + S (1) = S ((S (0)) * ff_v_factorial_transport)) /\ exists ff_q_factorial_transport_start. ff_u_factorial_transport = ff_q_factorial_transport_start * S ((S (0)) * ff_v_factorial_transport) + (1))) /\ ((((exists ff_h_factorial_transport_terminal. ff_h_factorial_transport_terminal + S (z) = S ((S (n)) * ff_v_factorial_transport)) /\ exists ff_q_factorial_transport_terminal. ff_u_factorial_transport = ff_q_factorial_transport_terminal * S ((S (n)) * ff_v_factorial_transport) + (z))) /\ forall ff_i_factorial_transport. (exists ff_lt_factorial_transport_bound. ff_lt_factorial_transport_bound + S ff_i_factorial_transport = n) -> exists ff_p_factorial_transport ff_r_factorial_transport ff_s_factorial_transport. ((((exists ff_h_factorial_transport_factor. ff_h_factorial_transport_factor + S (ff_p_factorial_transport) = S ((S (ff_i_factorial_transport)) * x3)) /\ exists ff_q_factorial_transport_factor. x2 = ff_q_factorial_transport_factor * S ((S (ff_i_factorial_transport)) * x3) + (ff_p_factorial_transport))) /\ ((((exists ff_h_factorial_transport_partial. ff_h_factorial_transport_partial + S (ff_r_factorial_transport) = S ((S (ff_i_factorial_transport)) * ff_v_factorial_transport)) /\ exists ff_q_factorial_transport_partial. ff_u_factorial_transport = ff_q_factorial_transport_partial * S ((S (ff_i_factorial_transport)) * ff_v_factorial_transport) + (ff_r_factorial_transport))) /\ ((((exists ff_h_factorial_transport_successor. ff_h_factorial_transport_successor + S (ff_s_factorial_transport) = S ((S (S ff_i_factorial_transport)) * ff_v_factorial_transport)) /\ exists ff_q_factorial_transport_successor. ff_u_factorial_transport = ff_q_factorial_transport_successor * S ((S (S ff_i_factorial_transport)) * ff_v_factorial_transport) + (ff_s_factorial_transport))) /\ ff_s_factorial_transport = ff_r_factorial_transport * ff_p_factorial_transport)))))
  13. 0013specialize beta_product_transport_prefix x
  14. 0014specialize beta_product_transport_prefix x1
  15. 0015specialize beta_product_transport_prefix x2
  16. 0016specialize beta_product_transport_prefix x3
  17. 0017specialize beta_product_transport_prefix n
  18. 0018specialize beta_product_transport_prefix z
  19. 0019apply beta_product_transport_prefix
  20. 0020exact hz_witness_witness_right
  21. 0021intro i
  22. 0022intro p
  23. 0023intro hi
  24. 0024intro hp
  25. 0025specialize beta_range_transport_entry x
  26. 0026specialize beta_range_transport_entry x1
  27. 0027specialize beta_range_transport_entry x2
  28. 0028specialize beta_range_transport_entry x3
  29. 0029specialize beta_range_transport_entry 1
  30. 0030specialize beta_range_transport_entry n
  31. 0031have hentries : ∀ i. ∀ p. Lt(i,n) → BetaAt(x,x1,i,p) → BetaAt(x2,x3,i,p)
    Exact native replay linehave hentries : forall i p. (exists h. h + S i = n) -> (((exists ff_h_factorial_transport_l. ff_h_factorial_transport_l + S (p) = S ((S (i)) * x1)) /\ exists ff_q_factorial_transport_l. x = ff_q_factorial_transport_l * S ((S (i)) * x1) + (p))) -> (((exists ff_h_factorial_transport_r. ff_h_factorial_transport_r + S (p) = S ((S (i)) * x3)) /\ exists ff_q_factorial_transport_r. x2 = ff_q_factorial_transport_r * S ((S (i)) * x3) + (p)))
  32. 0032apply beta_range_transport_entry
  33. 0033exact hz_witness_witness_left
  34. 0034exact hw_witness_witness_left
  35. 0035specialize hentries i
  36. 0036specialize hentries p
  37. 0037apply hentries
  38. 0038exact hi
  39. 0039exact hp
  40. 0040cases htransport
  41. 0041cases htransport_witness
  42. 0042cases hw_witness_witness_right
  43. 0043cases hw_witness_witness_right_witness
  44. 0044specialize beta_product_functional x2
  45. 0045specialize beta_product_functional x3
  46. 0046specialize beta_product_functional n
  47. 0047specialize beta_product_functional z
  48. 0048specialize beta_product_functional x4
  49. 0049specialize beta_product_functional x5
  50. 0050specialize beta_product_functional w
  51. 0051specialize beta_product_functional x6
  52. 0052specialize beta_product_functional x7
  53. 0053apply beta_product_functional
  54. 0054exact htransport_witness_witness
  55. 0055exact hw_witness_witness_right_witness_witness