PA0045

beta_repeat_exists

Stable checked-use theorem · independently closed

Every value and length admit a beta-coded constant prefix.

Exact expanded PA statement

forall a l. exists b c. (forall ff_i_r. (exists ff_lt_r_bound. ff_lt_r_bound + S ff_i_r = l) -> (((exists ff_h_r_decoded. ff_h_r_decoded + S (a) = S ((S (ff_i_r)) * c)) /\ exists ff_q_r_decoded. b = ff_q_r_decoded * S ((S (ff_i_r)) * c) + (a))))

Structural proof guide

Generated structural guide

Every value and length admit a beta-coded constant prefix.

Use the direct prerequisites beta_repeat_empty, beta_repeat_succ_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (2).

Referenced ingredients

PA0043 beta_repeat_empty PA0044 beta_repeat_succ_extend

Proof neighborhood

Direct dependencies

PA0043 beta_repeat_empty PA0044 beta_repeat_succ_extend

Direct dependents

PA0046 pow_exists PA00C0 prime_scaled_half_division_prefix_exists PA00EL beta_repeat_sum_exists_exact PA00ES eisenstein_zero_width_rectangle_sum_zero

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 a
  2. 0002induction l
  3. 0003exists 0
  4. 0004exists 0
  5. 0005specialize beta_repeat_empty 0
  6. 0006specialize beta_repeat_empty 0
  7. 0007specialize beta_repeat_empty a
  8. 0008specialize beta_repeat_empty 0
  9. 0009apply beta_repeat_empty
  10. 0010refl
  11. 0011cases IH
  12. 0012cases IH_witness
  13. 0013specialize beta_repeat_succ_extend x
  14. 0014specialize beta_repeat_succ_extend x1
  15. 0015specialize beta_repeat_succ_extend a
  16. 0016specialize beta_repeat_succ_extend l
  17. 0017specialize beta_repeat_succ_extend (S l)
  18. 0018apply beta_repeat_succ_extend
  19. 0019refl
  20. 0020exact IH_witness_witness