PA003X

beta_product_exists

Stable checked-use theorem · independently closed

Every finite decoded beta prefix has an exact relational product and a coded trace.

Exact expanded PA statement

forall b c l. exists n 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)))))

Structural proof guide

Generated structural guide

Every finite decoded beta prefix has an exact relational product and a coded trace.

Use the direct prerequisites beta_prefix_product_trace_exists, beta_at_exists as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (2).

Referenced ingredients

PA003W beta_prefix_product_trace_exists PA0029 beta_at_exists

Proof neighborhood

Direct dependencies

PA003W beta_prefix_product_trace_exists PA0029 beta_at_exists

Direct dependents

PA0046 pow_exists PA0060 factorial_exists PA007J beta_sign_factor_product_power_exists PA007O beta_pointwise_mul_product_exists PA007X beta_product_permutation_invariant PA0085 gauss_lemma_power_congruence_exists PA008J prime_mul_residue_product_balance PA00BA paired_pair_order_product_one_exists PA00BE prime_wilson_terminal_product_package_exists PA00BK scaled_pair_order_terminal_power_mod_predecessor

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004have htrace : exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ 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))))
  5. 0005specialize beta_prefix_product_trace_exists b
  6. 0006specialize beta_prefix_product_trace_exists c
  7. 0007specialize beta_prefix_product_trace_exists l
  8. 0008exact beta_prefix_product_trace_exists
  9. 0009cases htrace
  10. 0010cases htrace_witness
  11. 0011cases htrace_witness_witness
  12. 0012have hterminal : exists n. ((exists h. h + S n = S ((S l) * x1)) /\ exists q. x = q * S ((S l) * x1) + n)
  13. 0013specialize beta_at_exists x
  14. 0014specialize beta_at_exists x1
  15. 0015specialize beta_at_exists l
  16. 0016exact beta_at_exists
  17. 0017cases hterminal
  18. 0018exists x2
  19. 0019exists x
  20. 0020exists x1
  21. 0021split
  22. 0022exact htrace_witness_witness_left
  23. 0023split
  24. 0024exact hterminal_witness
  25. 0025exact htrace_witness_witness_right