PA0029

beta_at_exists

Stable checked-use theorem · independently closed

Every Gödel-beta position has a bounded decoded residue.

Exact expanded PA statement

forall b c i. exists x. ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x)

Structural proof guide

Generated structural guide

Every Gödel-beta position has a bounded decoded residue.

Use the direct prerequisites beta_modulus_nonzero, mul_comm, division_remainder_exists as previously established PA formulas.

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

Referenced ingredients

PA000U beta_modulus_nonzero PA000H mul_comm PA001D division_remainder_exists

Proof neighborhood

Direct dependencies

PA000U beta_modulus_nonzero PA000H mul_comm PA001D division_remainder_exists

Direct dependents

PA002G beta_exclusive_recode_congruence_step PA003G beta_prefix_sum_trace_exists PA003H beta_sum_exists PA003W beta_prefix_product_trace_exists PA003X beta_product_exists PA004H finite_contains_decidable PA004J beta_prefix_replace_exists PA004N beta_prefix_swap_last_reflect PA007K beta_pointwise_mul_prefix_extend PA007L beta_pointwise_mul_prefix_exists PA007X beta_product_permutation_invariant PA008C beta_successor_lift_exists PA009L beta_prefix_append_two_reflect PA00BY beta_division_prefix_exists PA00CX beta_sum_permutation_invariant PA00E7 eisenstein_transposed_outer_column_choices PA00F6 eisenstein_transposed_column_counts_extensional PA00FA eisenstein_successor_terminal_prefix_to_last_column

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 i
  4. 0004have hm0 : ~(S ((S i) * c) = 0)
  5. 0005specialize beta_modulus_nonzero c
  6. 0006specialize beta_modulus_nonzero i
  7. 0007exact beta_modulus_nonzero
  8. 0008specialize division_remainder_exists (S ((S i) * c))
  9. 0009specialize division_remainder_exists b
  10. 0010have hdiv : exists q r. b = S ((S i) * c) * q + r /\ exists h. h + S r = S ((S i) * c)
  11. 0011apply division_remainder_exists
  12. 0012exact hm0
  13. 0013cases hdiv
  14. 0014cases hdiv_witness
  15. 0015cases hdiv_witness_witness
  16. 0016exists x1
  17. 0017split
  18. 0018exact hdiv_witness_witness_right
  19. 0019exists x
  20. 0020trans S ((S i) * c) * x + x1
  21. 0021exact hdiv_witness_witness_left
  22. 0022congr
  23. 0023apply mul_comm
  24. 0024refl