PA007T · theorem

beta_magnitude_predecessor_recode_reflect

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

Unique target decoding reflects every predecessor-code entry back to its source successor magnitude.

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. ∀ H. ∀ l. ∀ i. ∀ r. (∀ x. Lt(x,l) → ∃ y. BetaAt(mb,mc,x,y) ∧ (Lt(0,y) ∧ Le(y,H))) → (∀ x. ∀ y. Lt(x,l) → BetaAt(mb,mc,x,S y) → BetaAt(rb,rc,x,y)) → Lt(i,l) → BetaAt(rb,rc,i,r) → BetaAt(mb,mc,i,S r)

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

10 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

5 occurrences

Exact expanded native-PA statement
forall mb mc rb rc H l i r. (forall gmp_index_predecessor_transport_range. (exists gsp_lt_gap_predecessor_transport_range_index_bound. gsp_lt_gap_predecessor_transport_range_index_bound + S gmp_index_predecessor_transport_range = l) -> exists gmp_magnitude_predecessor_transport_range. ((((exists ff_h_gmp_predecessor_transport_range_decoded. ff_h_gmp_predecessor_transport_range_decoded + S (gmp_magnitude_predecessor_transport_range) = S ((S (gmp_index_predecessor_transport_range)) * mc)) /\ exists ff_q_gmp_predecessor_transport_range_decoded. mb = ff_q_gmp_predecessor_transport_range_decoded * S ((S (gmp_index_predecessor_transport_range)) * mc) + (gmp_magnitude_predecessor_transport_range))) /\ ((exists gsp_lt_gap_predecessor_transport_range_positive. gsp_lt_gap_predecessor_transport_range_positive + S 0 = gmp_magnitude_predecessor_transport_range) /\ (exists gsp_le_gap_predecessor_transport_range_bounded. gsp_le_gap_predecessor_transport_range_bounded + gmp_magnitude_predecessor_transport_range = H)))) -> (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)))) -> (exists gsp_lt_gap_predecessor_transport_index_bound. gsp_lt_gap_predecessor_transport_index_bound + S i = l) -> (((exists ff_h_gmp_predecessor_transport_target_entry. ff_h_gmp_predecessor_transport_target_entry + S (r) = S ((S (i)) * rc)) /\ exists ff_q_gmp_predecessor_transport_target_entry. rb = ff_q_gmp_predecessor_transport_target_entry * S ((S (i)) * rc) + (r))) -> (((exists gsp_beta_height_predecessor_transport_source_entry. gsp_beta_height_predecessor_transport_source_entry + S (S r) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_predecessor_transport_source_entry. mb = gsp_beta_quotient_predecessor_transport_source_entry * S ((S (i)) * mc) + (S r)))

Proof neighborhood

Direct theorem prerequisites

PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA002F beta_at_unique

Direct theorem dependents

PA007U beta_magnitude_predecessor_recode_injective PA007V gauss_predecessor_half_range_aligned PA00B4 finite_bounded_nonendpoint_injective_coverage PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00CS beta_magnitude_predecessor_recode_aligned_half_range

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

58 script commands · 11 reading checkpoints · 7 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 (3)
ne zero of one lenonzero is succbeta at unique
01Fix variables and assumptionsL1–10

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 H
  6. L6
    intro l
  7. L7
    intro i
  8. L8
    intro r
  9. L9
    intro hrange
  10. L10
    intro hrecode
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hi
  2. L12
    intro htarget
03Establish hentryL13–16

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

  1. L13
    have hentry : ∃ m. BetaAt(mb,mc,i,m) ∧ (Lt(0,m) ∧ Le(m,H))Definitions: BetaAt(mb,mc,i,m)Lt(0,m)Le(m,H)Original native command in the exact edition
  2. L14
    specialize hrange i
  3. L15
    apply hrange
  4. L16
    exact hi
04Separate the logical casesL17–19

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

  1. L17
    cases hentry
  2. L18
    cases hentry_witness
  3. L19
    cases hentry_witness_right
05Establish hx0L20–25

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

  1. L20
    have hx0 : ~(x = 0)
  2. L21
    intro hxzero
  3. L22
    specialize ne_zero_of_one_le x
  4. L23
    apply ne_zero_of_one_le
  5. L24
    exact hentry_witness_right_left
  6. L25
    exact hxzero
06Establish hxpredecessorL26–29

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

  1. L26
    have hxpredecessor : exists q. x = S q
  2. L27
    specialize nonzero_is_succ x
  3. L28
    apply nonzero_is_succ
  4. L29
    exact hx0
07Separate the logical casesL30–30

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

  1. L30
    cases hxpredecessor
08Establish hsource_predecessorL31–34

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hsource_predecessor : BetaAt(mb,mc,i,S x1)Definitions: BetaAt(mb,mc,i,S x1)Original native command in the exact edition
  2. L32
    rewrite <- hxpredecessor_witness
  3. L33
    rewrite <- hxpredecessor_witness
  4. L34
    exact hentry_witness_left
09Establish htarget_predecessorL35–40

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

  1. L35
    have htarget_predecessor : BetaAt(rb,rc,i,x1)Definitions: BetaAt(rb,rc,i,x1)Original native command in the exact edition
  2. L36
    specialize hrecode i
  3. L37
    specialize hrecode x1
  4. L38
    apply hrecode
  5. L39
    exact hi
  6. L40
    exact hsource_predecessor
10Establish hrxL41–49

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

  1. L41
    have hrx : r = x1
  2. L42
    specialize beta_at_unique rb
  3. L43
    specialize beta_at_unique rc
  4. L44
    specialize beta_at_unique i
  5. L45
    specialize beta_at_unique r
  6. L46
    specialize beta_at_unique x1
  7. L47
    apply beta_at_unique
  8. L48
    exact htarget
  9. L49
    exact htarget_predecessor
11Establish hxsrL50–58

Establish this local claim before using it. It is not an additional assumption.

  1. L50
    have hxsr : x = S r
  2. L51
    trans S x1
  3. L52
    exact hxpredecessor_witness
  4. L53
    congr
  5. L54
    symm
  6. L55
    exact hrx
  7. L56
    rewrite hxsr at hentry_witness_left
  8. L57
    rewrite hxsr at hentry_witness_left
  9. L58
    exact hentry_witness_left

Library-wide reading audit

Original defined command ledger · 58 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro H
  6. 0006intro l
  7. 0007intro i
  8. 0008intro r
  9. 0009intro hrange
  10. 0010intro hrecode
  11. 0011intro hi
  12. 0012intro htarget
  13. 0013have hentry : ∃ m. BetaAt(mb,mc,i,m) ∧ (Lt(0,m) ∧ Le(m,H))
    Exact native replay linehave hentry : exists m. (((exists ff_h_gmp_predecessor_transport_range_entry. ff_h_gmp_predecessor_transport_range_entry + S (m) = S ((S (i)) * mc)) /\ exists ff_q_gmp_predecessor_transport_range_entry. mb = ff_q_gmp_predecessor_transport_range_entry * S ((S (i)) * mc) + (m))) /\ ((exists gsp_lt_gap_predecessor_transport_positive. gsp_lt_gap_predecessor_transport_positive + S 0 = m) /\ (exists gsp_le_gap_predecessor_transport_bounded. gsp_le_gap_predecessor_transport_bounded + m = H))
  14. 0014specialize hrange i
  15. 0015apply hrange
  16. 0016exact hi
  17. 0017cases hentry
  18. 0018cases hentry_witness
  19. 0019cases hentry_witness_right
  20. 0020have hx0 : ~(x = 0)
  21. 0021intro hxzero
  22. 0022specialize ne_zero_of_one_le x
  23. 0023apply ne_zero_of_one_le
  24. 0024exact hentry_witness_right_left
  25. 0025exact hxzero
  26. 0026have hxpredecessor : exists q. x = S q
  27. 0027specialize nonzero_is_succ x
  28. 0028apply nonzero_is_succ
  29. 0029exact hx0
  30. 0030cases hxpredecessor
  31. 0031have hsource_predecessor : BetaAt(mb,mc,i,S x1)
    Exact native replay linehave hsource_predecessor : ((exists gsp_beta_height_predecessor_transport_source_predecessor. gsp_beta_height_predecessor_transport_source_predecessor + S (S x1) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_predecessor_transport_source_predecessor. mb = gsp_beta_quotient_predecessor_transport_source_predecessor * S ((S (i)) * mc) + (S x1))
  32. 0032rewrite <- hxpredecessor_witness
  33. 0033rewrite <- hxpredecessor_witness
  34. 0034exact hentry_witness_left
  35. 0035have htarget_predecessor : BetaAt(rb,rc,i,x1)
    Exact native replay linehave htarget_predecessor : ((exists ff_h_gmp_predecessor_transport_target_predecessor. ff_h_gmp_predecessor_transport_target_predecessor + S (x1) = S ((S (i)) * rc)) /\ exists ff_q_gmp_predecessor_transport_target_predecessor. rb = ff_q_gmp_predecessor_transport_target_predecessor * S ((S (i)) * rc) + (x1))
  36. 0036specialize hrecode i
  37. 0037specialize hrecode x1
  38. 0038apply hrecode
  39. 0039exact hi
  40. 0040exact hsource_predecessor
  41. 0041have hrx : r = x1
  42. 0042specialize beta_at_unique rb
  43. 0043specialize beta_at_unique rc
  44. 0044specialize beta_at_unique i
  45. 0045specialize beta_at_unique r
  46. 0046specialize beta_at_unique x1
  47. 0047apply beta_at_unique
  48. 0048exact htarget
  49. 0049exact htarget_predecessor
  50. 0050have hxsr : x = S r
  51. 0051trans S x1
  52. 0052exact hxpredecessor_witness
  53. 0053congr
  54. 0054symm
  55. 0055exact hrx
  56. 0056rewrite hxsr at hentry_witness_left
  57. 0057rewrite hxsr at hentry_witness_left
  58. 0058exact hentry_witness_left