BT00TW

factorial_weighted_product_combine

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Weighted factorial products combine by reassociation.

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 u v x y f K r F J. J = r * u -> F = f * v -> u * y = v * x -> f = (K * r) * x -> F = (K * J) * y

Structural proof guide

Weighted factorial products combine by reassociation.

Direct prerequisites: mul_comm, mul_assoc. The authored body proceeds by intermediate claims (4), equality transport (7).

Proof neighborhood

Direct dependencies

BT0006 mul_comm BT0008 mul_assoc

Direct dependents

BT00TX choose_factorial_bridge

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

29 script commands · 7 reading checkpoints · 4 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)
mul commmul assoc
01Fix variables and assumptionsL1–10

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

  1. L1
    intro u
  2. L2
    intro v
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro f
  6. L6
    intro K
  7. L7
    intro r
  8. L8
    intro F
  9. L9
    intro J
  10. L10
    intro hJ
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hF
  2. L12
    intro hweighted
  3. L13
    intro hf
03Calculate and transport equalitiesL14–14

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

  1. L14
    rewrite hf at hF
04Establish hassoc_xvL15–17

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

  1. L15
    have hassoc_xv : ((K * r) * x) * v = (K * r) * (x * v)
  2. L16
    apply mul_assoc
  3. L17
    rewrite hassoc_xv at hF
05Establish hcomm_xvL18–21

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

  1. L18
    have hcomm_xv : x * v = v * x
  2. L19
    apply mul_comm
  3. L20
    rewrite hcomm_xv at hF
  4. L21
    rewrite <- hweighted at hF
06Establish hassoc_uyL22–24

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

  1. L22
    have hassoc_uy : ((K * r) * u) * y = (K * r) * (u * y)
  2. L23
    apply mul_assoc
  3. L24
    rewrite <- hassoc_uy at hF
07Establish hassoc_kruL25–29

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

  1. L25
    have hassoc_kru : (K * r) * u = K * (r * u)
  2. L26
    apply mul_assoc
  3. L27
    rewrite hassoc_kru at hF
  4. L28
    rewrite <- hJ at hF
  5. L29
    exact hF

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro x
  4. 0004intro y
  5. 0005intro f
  6. 0006intro K
  7. 0007intro r
  8. 0008intro F
  9. 0009intro J
  10. 0010intro hJ
  11. 0011intro hF
  12. 0012intro hweighted
  13. 0013intro hf
  14. 0014rewrite hf at hF
  15. 0015have hassoc_xv : ((K * r) * x) * v = (K * r) * (x * v)
  16. 0016apply mul_assoc
  17. 0017rewrite hassoc_xv at hF
  18. 0018have hcomm_xv : x * v = v * x
  19. 0019apply mul_comm
  20. 0020rewrite hcomm_xv at hF
  21. 0021rewrite <- hweighted at hF
  22. 0022have hassoc_uy : ((K * r) * u) * y = (K * r) * (u * y)
  23. 0023apply mul_assoc
  24. 0024rewrite <- hassoc_uy at hF
  25. 0025have hassoc_kru : (K * r) * u = K * (r * u)
  26. 0026apply mul_assoc
  27. 0027rewrite hassoc_kru at hF
  28. 0028rewrite <- hJ at hF
  29. 0029exact hF