PA007S · theorem

beta_magnitude_predecessor_recode_bounded

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

Removing one successor turns the positive 1,...,l range bound into the finite 0,...,l-1 bound.

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

∀ mb. ∀ mc. ∀ rb. ∀ rc. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(mb,mc,x,y) ∧ (Lt(0,y) ∧ Le(y,l))) → (∀ x. ∀ y. Lt(x,l) → BetaAt(mb,mc,x,S y) → BetaAt(rb,rc,x,y)) → BoundedPrefix(rb,rc,l)

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

PD0001 Le PD0002 Lt PD0013 BetaAt PD0024 BoundedPrefix

8 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

3 occurrences

Exact expanded native-PA statement
forall mb mc rb rc l. (forall gmp_index_predecessor_transport_finite_range. (exists gsp_lt_gap_predecessor_transport_finite_range_index_bound. gsp_lt_gap_predecessor_transport_finite_range_index_bound + S gmp_index_predecessor_transport_finite_range = l) -> exists gmp_magnitude_predecessor_transport_finite_range. ((((exists ff_h_gmp_predecessor_transport_finite_range_decoded. ff_h_gmp_predecessor_transport_finite_range_decoded + S (gmp_magnitude_predecessor_transport_finite_range) = S ((S (gmp_index_predecessor_transport_finite_range)) * mc)) /\ exists ff_q_gmp_predecessor_transport_finite_range_decoded. mb = ff_q_gmp_predecessor_transport_finite_range_decoded * S ((S (gmp_index_predecessor_transport_finite_range)) * mc) + (gmp_magnitude_predecessor_transport_finite_range))) /\ ((exists gsp_lt_gap_predecessor_transport_finite_range_positive. gsp_lt_gap_predecessor_transport_finite_range_positive + S 0 = gmp_magnitude_predecessor_transport_finite_range) /\ (exists gsp_le_gap_predecessor_transport_finite_range_bounded. gsp_le_gap_predecessor_transport_finite_range_bounded + gmp_magnitude_predecessor_transport_finite_range = l)))) -> (forall gmp_index_predecessor_transport_recode gmp_predecessor_predecessor_transport_recode. (exists gsp_lt_gap_predecessor_transport_recode_index_bound. gsp_lt_gap_predecessor_transport_recode_index_bound + S gmp_index_predecessor_transport_recode = l) -> (((exists gsp_beta_height_gmp_predecessor_transport_recode_source. gsp_beta_height_gmp_predecessor_transport_recode_source + S (S gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_transport_recode_source. mb = gsp_beta_quotient_gmp_predecessor_transport_recode_source * S ((S (gmp_index_predecessor_transport_recode)) * mc) + (S gmp_predecessor_predecessor_transport_recode))) -> (((exists ff_h_gmp_predecessor_transport_recode_target. ff_h_gmp_predecessor_transport_recode_target + S (gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * rc)) /\ exists ff_q_gmp_predecessor_transport_recode_target. rb = ff_q_gmp_predecessor_transport_recode_target * S ((S (gmp_index_predecessor_transport_recode)) * rc) + (gmp_predecessor_predecessor_transport_recode)))) -> (forall fp_i_predecessor_transport_bounded_result. (exists fp_gap_predecessor_transport_bounded_result_index. fp_gap_predecessor_transport_bounded_result_index + S fp_i_predecessor_transport_bounded_result = l) -> exists fp_value_predecessor_transport_bounded_result. ((((exists ff_h_predecessor_transport_bounded_result_entry. ff_h_predecessor_transport_bounded_result_entry + S (fp_value_predecessor_transport_bounded_result) = S ((S (fp_i_predecessor_transport_bounded_result)) * rc)) /\ exists ff_q_predecessor_transport_bounded_result_entry. rb = ff_q_predecessor_transport_bounded_result_entry * S ((S (fp_i_predecessor_transport_bounded_result)) * rc) + (fp_value_predecessor_transport_bounded_result))) /\ (exists fp_gap_predecessor_transport_bounded_result_value. fp_gap_predecessor_transport_bounded_result_value + S fp_value_predecessor_transport_bounded_result = l)))

Proof neighborhood

Direct theorem prerequisites

PA003U ne_zero_of_one_le PA001V nonzero_is_succ

Direct theorem dependents

PA007V gauss_predecessor_half_range_aligned PA007Y gauss_magnitude_product_eq_half_range PA00B3 beta_magnitude_predecessor_recode_surjective PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00BD pair_order_terminal_successor_product_eq_range_two PA00CY beta_magnitude_sum_permutation_exact

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

38 script commands · 13 reading checkpoints · 3 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.

Named ingredients (2)
ne zero of one lenonzero is succ
01Fix variables and assumptionsL1–9

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

  1. L1
    intro mb
  2. L2
    intro mc
  3. L3
    intro rb
  4. L4
    intro rc
  5. L5
    intro l
  6. L6
    intro hrange
  7. L7
    intro hrecode
  8. L8
    intro i
  9. L9
    intro hi
02Establish hentryL10–13

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

  1. L10
    have hentry : ∃ m. BetaAt(mb,mc,i,m) ∧ (Lt(0,m) ∧ Le(m,l))Definitions: BetaAt(mb,mc,i,m)Lt(0,m)Le(m,l)Original native command in the exact edition
  2. L11
    specialize hrange i
  3. L12
    apply hrange
  4. L13
    exact hi
03Separate the logical casesL14–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases hentry
  2. L15
    cases hentry_witness
  3. L16
    cases hentry_witness_right
04Establish hx0L17–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply ne zero of one le.

  1. L17
    have hx0 : ~(x = 0)
  2. L18
    intro hxzero
  3. L19
    specialize ne_zero_of_one_le x
  4. L20
    apply ne_zero_of_one_le
  5. L21
    exact hentry_witness_right_left
  6. L22
    exact hxzero
05Establish hxpredecessorL23–26

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

  1. L23
    have hxpredecessor : exists q. x = S q
  2. L24
    specialize nonzero_is_succ x
  3. L25
    apply nonzero_is_succ
  4. L26
    exact hx0
06Separate the logical casesL27–27

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L27
    cases hxpredecessor
07Construct an explicit witnessL28–28

Supply the displayed value, then prove that it has the required property.

  1. L28
    exists x1
08Separate the logical casesL29–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    split
09Use earlier factsL30–33

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

  1. L30
    specialize hrecode i
  2. L31
    specialize hrecode x1
  3. L32
    apply hrecode
  4. L33
    exact hi
10Calculate and transport equalitiesL34–35

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L34
    rewrite <- hxpredecessor_witness
  2. L35
    rewrite <- hxpredecessor_witness
11Use earlier factsL36–36

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

  1. L36
    exact hentry_witness_left
12Calculate and transport equalitiesL37–37

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L37
    rewrite hxpredecessor_witness at hentry_witness_right_right
13Use earlier factsL38–38

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

  1. L38
    exact hentry_witness_right_right

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro l
  6. 0006intro hrange
  7. 0007intro hrecode
  8. 0008intro i
  9. 0009intro hi
  10. 0010have hentry : ∃ m. BetaAt(mb,mc,i,m) ∧ (Lt(0,m) ∧ Le(m,l))
    Exact native replay linehave hentry : exists m. (((exists ff_h_gmp_predecessor_transport_finite_range_entry. ff_h_gmp_predecessor_transport_finite_range_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_gmp_predecessor_transport_finite_range_entry. mb = ff_q_gmp_predecessor_transport_finite_range_entry * S ((S (i)) * mc) + (m))) /\ ((exists gsp_lt_gap_predecessor_transport_finite_positive. gsp_lt_gap_predecessor_transport_finite_positive + S 0 = m) /\ (exists gsp_le_gap_predecessor_transport_finite_bounded. gsp_le_gap_predecessor_transport_finite_bounded + m = l))
  11. 0011specialize hrange i
  12. 0012apply hrange
  13. 0013exact hi
  14. 0014cases hentry
  15. 0015cases hentry_witness
  16. 0016cases hentry_witness_right
  17. 0017have hx0 : ~(x = 0)
  18. 0018intro hxzero
  19. 0019specialize ne_zero_of_one_le x
  20. 0020apply ne_zero_of_one_le
  21. 0021exact hentry_witness_right_left
  22. 0022exact hxzero
  23. 0023have hxpredecessor : exists q. x = S q
  24. 0024specialize nonzero_is_succ x
  25. 0025apply nonzero_is_succ
  26. 0026exact hx0
  27. 0027cases hxpredecessor
  28. 0028exists x1
  29. 0029split
  30. 0030specialize hrecode i
  31. 0031specialize hrecode x1
  32. 0032apply hrecode
  33. 0033exact hi
  34. 0034rewrite <- hxpredecessor_witness
  35. 0035rewrite <- hxpredecessor_witness
  36. 0036exact hentry_witness_left
  37. 0037rewrite hxpredecessor_witness at hentry_witness_right_right
  38. 0038exact hentry_witness_right_right