PA00BW

beta_scaled_successor_prefix_from_pointwise

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

32 script commands · 5 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro tb
  7. L7
    intro tc
  8. L8
    intro h
  9. L9
    intro hhalf
  10. L10
    intro hrepeat
02Fix variables and assumptionsL11–15

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hpointwise
  2. L12
    intro i
  3. L13
    intro x
  4. L14
    intro hi
  5. L15
    intro hx
03Establish hcanonicalL16–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hhalf.

  1. L16
    have 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))
  2. L17
    specialize hhalf i
  3. L18
    apply hhalf
  4. L19
    exact hi
04Establish hrepeatedL20–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hrepeat.

  1. L20
    have 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))
  2. L21
    specialize hrepeat i
  3. L22
    apply hrepeat
  4. L23
    exact hi
  5. L24
    specialize hpointwise i
  6. L25
    specialize hpointwise a
  7. L26
    specialize hpointwise (1 + i)
  8. L27
    specialize hpointwise x
  9. L28
    apply hpointwise
  10. L29
    exact hi
05Use earlier factsL30–32

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L30
    exact hrepeated
  2. L31
    exact hcanonical
  3. L32
    exact hx

Library-wide reading audit

Original exact command ledger · 32 lines
  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