PA00BW

beta_scaled_successor_prefix_from_pointwise

Alpha v16 checked-use theorem · independently closed; not Stable

A constant prefix times 1,...,h decodes exactly as a*(1+i).

Exact expanded PA statement

forall a b c ab ac tb tc h. (forall gsp_range_index_eisenstein_scaled_half_range. (exists gsp_lt_gap_eisenstein_scaled_half_range_range_bound. gsp_lt_gap_eisenstein_scaled_half_range_range_bound + S gsp_range_index_eisenstein_scaled_half_range = h) -> (((exists gsp_beta_height_eisenstein_scaled_half_range_range_entry. gsp_beta_height_eisenstein_scaled_half_range_range_entry + S (1 + gsp_range_index_eisenstein_scaled_half_range) = S ((S (gsp_range_index_eisenstein_scaled_half_range)) * c)) /\ exists gsp_beta_quotient_eisenstein_scaled_half_range_range_entry. b = gsp_beta_quotient_eisenstein_scaled_half_range_range_entry * S ((S (gsp_range_index_eisenstein_scaled_half_range)) * c) + (1 + gsp_range_index_eisenstein_scaled_half_range)))) -> (forall ff_i_eisenstein_scaled_repeat. (exists ff_lt_eisenstein_scaled_repeat_bound. ff_lt_eisenstein_scaled_repeat_bound + S ff_i_eisenstein_scaled_repeat = h) -> (((exists ff_h_eisenstein_scaled_repeat_decoded. ff_h_eisenstein_scaled_repeat_decoded + S (a) = S ((S (ff_i_eisenstein_scaled_repeat)) * ac)) /\ exists ff_q_eisenstein_scaled_repeat_decoded. ab = ff_q_eisenstein_scaled_repeat_decoded * S ((S (ff_i_eisenstein_scaled_repeat)) * ac) + (a)))) -> (forall fpmp_index_eisenstein_scaled_pointwise fpmp_left_eisenstein_scaled_pointwise fpmp_right_eisenstein_scaled_pointwise fpmp_target_eisenstein_scaled_pointwise. (exists fpmp_gap_eisenstein_scaled_pointwise. fpmp_gap_eisenstein_scaled_pointwise + S fpmp_index_eisenstein_scaled_pointwise = h) -> (((exists ff_h_fpmp_eisenstein_scaled_pointwise_left. ff_h_fpmp_eisenstein_scaled_pointwise_left + S (fpmp_left_eisenstein_scaled_pointwise) = S ((S (fpmp_index_eisenstein_scaled_pointwise)) * ac)) /\ exists ff_q_fpmp_eisenstein_scaled_pointwise_left. ab = ff_q_fpmp_eisenstein_scaled_pointwise_left * S ((S (fpmp_index_eisenstein_scaled_pointwise)) * ac) + (fpmp_left_eisenstein_scaled_pointwise))) -> (((exists ff_h_fpmp_eisenstein_scaled_pointwise_right. ff_h_fpmp_eisenstein_scaled_pointwise_right + S (fpmp_right_eisenstein_scaled_pointwise) = S ((S (fpmp_index_eisenstein_scaled_pointwise)) * c)) /\ exists ff_q_fpmp_eisenstein_scaled_pointwise_right. b = ff_q_fpmp_eisenstein_scaled_pointwise_right * S ((S (fpmp_index_eisenstein_scaled_pointwise)) * c) + (fpmp_right_eisenstein_scaled_pointwise))) -> (((exists ff_h_fpmp_eisenstein_scaled_pointwise_target. ff_h_fpmp_eisenstein_scaled_pointwise_target + S (fpmp_target_eisenstein_scaled_pointwise) = S ((S (fpmp_index_eisenstein_scaled_pointwise)) * tc)) /\ exists ff_q_fpmp_eisenstein_scaled_pointwise_target. tb = ff_q_fpmp_eisenstein_scaled_pointwise_target * S ((S (fpmp_index_eisenstein_scaled_pointwise)) * tc) + (fpmp_target_eisenstein_scaled_pointwise))) -> fpmp_target_eisenstein_scaled_pointwise = fpmp_left_eisenstein_scaled_pointwise * fpmp_right_eisenstein_scaled_pointwise) -> (forall esd_index_eisenstein_scaled_exact esd_value_eisenstein_scaled_exact. (exists esd_gap_eisenstein_scaled_exact. esd_gap_eisenstein_scaled_exact + S esd_index_eisenstein_scaled_exact = h) -> (((exists ff_h_esd_eisenstein_scaled_exact_decoded. ff_h_esd_eisenstein_scaled_exact_decoded + S (esd_value_eisenstein_scaled_exact) = S ((S (esd_index_eisenstein_scaled_exact)) * tc)) /\ exists ff_q_esd_eisenstein_scaled_exact_decoded. tb = ff_q_esd_eisenstein_scaled_exact_decoded * S ((S (esd_index_eisenstein_scaled_exact)) * tc) + (esd_value_eisenstein_scaled_exact))) -> esd_value_eisenstein_scaled_exact = a * (1 + esd_index_eisenstein_scaled_exact))

Structural proof guide

Generated structural guide

A constant prefix times 1,...,h decodes exactly as a*(1+i).

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by intermediate claims (2).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA00C0 prime_scaled_half_division_prefix_exists

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro tb
  7. 0007intro tc
  8. 0008intro h
  9. 0009intro hhalf
  10. 0010intro hrepeat
  11. 0011intro hpointwise
  12. 0012intro i
  13. 0013intro x
  14. 0014intro hi
  15. 0015intro hx
  16. 0016have hcanonical : ((exists gsp_beta_height_eisenstein_scaled_canonical_entry. gsp_beta_height_eisenstein_scaled_canonical_entry + S (1 + i) = S ((S (i)) * c)) /\ exists gsp_beta_quotient_eisenstein_scaled_canonical_entry. b = gsp_beta_quotient_eisenstein_scaled_canonical_entry * S ((S (i)) * c) + (1 + i))
  17. 0017specialize hhalf i
  18. 0018apply hhalf
  19. 0019exact hi
  20. 0020have hrepeated : ((exists ff_h_eisenstein_scaled_repeated_entry. ff_h_eisenstein_scaled_repeated_entry + S (a) = S ((S (i)) * ac)) /\ exists ff_q_eisenstein_scaled_repeated_entry. ab = ff_q_eisenstein_scaled_repeated_entry * S ((S (i)) * ac) + (a))
  21. 0021specialize hrepeat i
  22. 0022apply hrepeat
  23. 0023exact hi
  24. 0024specialize hpointwise i
  25. 0025specialize hpointwise a
  26. 0026specialize hpointwise (1 + i)
  27. 0027specialize hpointwise x
  28. 0028apply hpointwise
  29. 0029exact hi
  30. 0030exact hrepeated
  31. 0031exact hcanonical
  32. 0032exact hx