PA0030

beta_range_exists

Stable checked-use theorem · independently closed

Every start and length admit a beta-coded consecutive range.

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 + ff_i_r) = S ((S (ff_i_r)) * c)) /\ exists ff_q_r_decoded. b = ff_q_r_decoded * S ((S (ff_i_r)) * c) + (a + ff_i_r))))

Structural proof guide

Generated structural guide

Every start and length admit a beta-coded consecutive range.

Use the direct prerequisites beta_range_empty, beta_range_succ_extend as previously established PA formulas.

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

Referenced ingredients

PA0006 beta_range_empty PA002Y beta_range_succ_extend

Proof neighborhood

Direct dependencies

PA0006 beta_range_empty PA002Y beta_range_succ_extend

Direct dependents

PA0060 factorial_exists PA00BE prime_wilson_terminal_product_package_exists PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists

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_range_empty 0
  6. 0006specialize beta_range_empty 0
  7. 0007specialize beta_range_empty a
  8. 0008specialize beta_range_empty 0
  9. 0009apply beta_range_empty
  10. 0010refl
  11. 0011cases IH
  12. 0012cases IH_witness
  13. 0013specialize beta_range_succ_extend x
  14. 0014specialize beta_range_succ_extend x1
  15. 0015specialize beta_range_succ_extend a
  16. 0016specialize beta_range_succ_extend l
  17. 0017specialize beta_range_succ_extend (S l)
  18. 0018apply beta_range_succ_extend
  19. 0019refl
  20. 0020exact IH_witness_witness