PA00BW · theorem

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.

Statement with defined notation

∀ a. ∀ b. ∀ c. ∀ ab. ∀ ac. ∀ tb. ∀ tc. ∀ h. Range(b,c,1,h) → Repeat(ab,ac,a,h) → (∀ x. ∀ y. ∀ z. ∀ n. Lt(x,h) → BetaAt(ab,ac,x,y) → BetaAt(b,c,x,z) → BetaAt(tb,tc,x,n) → n = y · z) → ∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = a · (1 + x)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0018 Range PD0019 Repeat

8 occurrences

In local proof propositions

PD0013 BetaAt

2 occurrences

Exact expanded native-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))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

PA00C0 prime_scaled_half_division_prefix_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : BetaAt(b,c,i,1 + i)Definitions: BetaAt(b,c,i,1 + i)Original native command in the exact edition
  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 : BetaAt(ab,ac,i,a)Definitions: BetaAt(ab,ac,i,a)Original native command in the exact edition
  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 defined 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 : BetaAt(b,c,i,1 + i)
    Exact native replay linehave 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 : BetaAt(ab,ac,i,a)
    Exact native replay linehave 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