PA007U · theorem

beta_magnitude_predecessor_recode_injective

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

Injectivity of positive magnitudes transports to their uniquely decoded predecessor code.

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))) → InjectivePrefix(mb,mc,l) → (∀ x. ∀ y. Lt(x,l) → BetaAt(mb,mc,x,S y) → BetaAt(rb,rc,x,y)) → InjectivePrefix(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 PD0025 InjectivePrefix

9 occurrences

In local proof propositions

PD0013 BetaAt

2 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 fp_i_predecessor_transport_magnitude_injective fp_j_predecessor_transport_magnitude_injective fp_value_predecessor_transport_magnitude_injective. (exists fp_gap_predecessor_transport_magnitude_injective_i. fp_gap_predecessor_transport_magnitude_injective_i + S fp_i_predecessor_transport_magnitude_injective = l) -> (exists fp_gap_predecessor_transport_magnitude_injective_j. fp_gap_predecessor_transport_magnitude_injective_j + S fp_j_predecessor_transport_magnitude_injective = l) -> (((exists ff_h_predecessor_transport_magnitude_injective_left. ff_h_predecessor_transport_magnitude_injective_left + S (fp_value_predecessor_transport_magnitude_injective) = S ((S (fp_i_predecessor_transport_magnitude_injective)) * mc)) /\ exists ff_q_predecessor_transport_magnitude_injective_left. mb = ff_q_predecessor_transport_magnitude_injective_left * S ((S (fp_i_predecessor_transport_magnitude_injective)) * mc) + (fp_value_predecessor_transport_magnitude_injective))) -> (((exists ff_h_predecessor_transport_magnitude_injective_right. ff_h_predecessor_transport_magnitude_injective_right + S (fp_value_predecessor_transport_magnitude_injective) = S ((S (fp_j_predecessor_transport_magnitude_injective)) * mc)) /\ exists ff_q_predecessor_transport_magnitude_injective_right. mb = ff_q_predecessor_transport_magnitude_injective_right * S ((S (fp_j_predecessor_transport_magnitude_injective)) * mc) + (fp_value_predecessor_transport_magnitude_injective))) -> fp_i_predecessor_transport_magnitude_injective = fp_j_predecessor_transport_magnitude_injective) -> (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_target_injective fp_j_predecessor_transport_target_injective fp_value_predecessor_transport_target_injective. (exists fp_gap_predecessor_transport_target_injective_i. fp_gap_predecessor_transport_target_injective_i + S fp_i_predecessor_transport_target_injective = l) -> (exists fp_gap_predecessor_transport_target_injective_j. fp_gap_predecessor_transport_target_injective_j + S fp_j_predecessor_transport_target_injective = l) -> (((exists ff_h_predecessor_transport_target_injective_left. ff_h_predecessor_transport_target_injective_left + S (fp_value_predecessor_transport_target_injective) = S ((S (fp_i_predecessor_transport_target_injective)) * rc)) /\ exists ff_q_predecessor_transport_target_injective_left. rb = ff_q_predecessor_transport_target_injective_left * S ((S (fp_i_predecessor_transport_target_injective)) * rc) + (fp_value_predecessor_transport_target_injective))) -> (((exists ff_h_predecessor_transport_target_injective_right. ff_h_predecessor_transport_target_injective_right + S (fp_value_predecessor_transport_target_injective) = S ((S (fp_j_predecessor_transport_target_injective)) * rc)) /\ exists ff_q_predecessor_transport_target_injective_right. rb = ff_q_predecessor_transport_target_injective_right * S ((S (fp_j_predecessor_transport_target_injective)) * rc) + (fp_value_predecessor_transport_target_injective))) -> fp_i_predecessor_transport_target_injective = fp_j_predecessor_transport_target_injective)

Proof neighborhood

Direct theorem prerequisites

PA007T beta_magnitude_predecessor_recode_reflect

Direct theorem dependents

PA007Y gauss_magnitude_product_eq_half_range PA00B3 beta_magnitude_predecessor_recode_surjective 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

51 script commands · 7 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.

Named ingredients (1)
beta magnitude predecessor recode reflect
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 l
  6. L6
    intro hrange
  7. L7
    intro hsource_injective
  8. L8
    intro hrecode
  9. L9
    intro i
  10. L10
    intro j
02Fix variables and assumptionsL11–15

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

  1. L11
    intro r
  2. L12
    intro hi
  3. L13
    intro hj
  4. L14
    intro htarget_i
  5. L15
    intro htarget_j
03Establish hsource_iL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode reflect.

  1. L16
    have hsource_i : BetaAt(mb,mc,i,S r)Definitions: BetaAt(mb,mc,i,S r)Original native command in the exact edition
  2. L17
    specialize beta_magnitude_predecessor_recode_reflect mb
  3. L18
    specialize beta_magnitude_predecessor_recode_reflect mc
  4. L19
    specialize beta_magnitude_predecessor_recode_reflect rb
  5. L20
    specialize beta_magnitude_predecessor_recode_reflect rc
  6. L21
    specialize beta_magnitude_predecessor_recode_reflect l
  7. L22
    specialize beta_magnitude_predecessor_recode_reflect l
  8. L23
    specialize beta_magnitude_predecessor_recode_reflect i
  9. L24
    specialize beta_magnitude_predecessor_recode_reflect r
  10. L25
    apply beta_magnitude_predecessor_recode_reflect
04Use earlier factsL26–29

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

  1. L26
    exact hrange
  2. L27
    exact hrecode
  3. L28
    exact hi
  4. L29
    exact htarget_i
05Establish hsource_jL30–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta magnitude predecessor recode reflect.

  1. L30
    have hsource_j : BetaAt(mb,mc,j,S r)Definitions: BetaAt(mb,mc,j,S r)Original native command in the exact edition
  2. L31
    specialize beta_magnitude_predecessor_recode_reflect mb
  3. L32
    specialize beta_magnitude_predecessor_recode_reflect mc
  4. L33
    specialize beta_magnitude_predecessor_recode_reflect rb
  5. L34
    specialize beta_magnitude_predecessor_recode_reflect rc
  6. L35
    specialize beta_magnitude_predecessor_recode_reflect l
  7. L36
    specialize beta_magnitude_predecessor_recode_reflect l
  8. L37
    specialize beta_magnitude_predecessor_recode_reflect j
  9. L38
    specialize beta_magnitude_predecessor_recode_reflect r
  10. L39
    apply beta_magnitude_predecessor_recode_reflect
06Use earlier factsL40–49

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

  1. L40
    exact hrange
  2. L41
    exact hrecode
  3. L42
    exact hj
  4. L43
    exact htarget_j
  5. L44
    specialize hsource_injective i
  6. L45
    specialize hsource_injective j
  7. L46
    specialize hsource_injective (S r)
  8. L47
    apply hsource_injective
  9. L48
    exact hi
  10. L49
    exact hj
07Use earlier factsL50–51

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

  1. L50
    exact hsource_i
  2. L51
    exact hsource_j

Library-wide reading audit

Original defined command ledger · 51 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro rb
  4. 0004intro rc
  5. 0005intro l
  6. 0006intro hrange
  7. 0007intro hsource_injective
  8. 0008intro hrecode
  9. 0009intro i
  10. 0010intro j
  11. 0011intro r
  12. 0012intro hi
  13. 0013intro hj
  14. 0014intro htarget_i
  15. 0015intro htarget_j
  16. 0016have hsource_i : BetaAt(mb,mc,i,S r)
    Exact native replay linehave hsource_i : ((exists gsp_beta_height_predecessor_injective_source_i. gsp_beta_height_predecessor_injective_source_i + S (S r) = S ((S (i)) * mc)) /\ exists gsp_beta_quotient_predecessor_injective_source_i. mb = gsp_beta_quotient_predecessor_injective_source_i * S ((S (i)) * mc) + (S r))
  17. 0017specialize beta_magnitude_predecessor_recode_reflect mb
  18. 0018specialize beta_magnitude_predecessor_recode_reflect mc
  19. 0019specialize beta_magnitude_predecessor_recode_reflect rb
  20. 0020specialize beta_magnitude_predecessor_recode_reflect rc
  21. 0021specialize beta_magnitude_predecessor_recode_reflect l
  22. 0022specialize beta_magnitude_predecessor_recode_reflect l
  23. 0023specialize beta_magnitude_predecessor_recode_reflect i
  24. 0024specialize beta_magnitude_predecessor_recode_reflect r
  25. 0025apply beta_magnitude_predecessor_recode_reflect
  26. 0026exact hrange
  27. 0027exact hrecode
  28. 0028exact hi
  29. 0029exact htarget_i
  30. 0030have hsource_j : BetaAt(mb,mc,j,S r)
    Exact native replay linehave hsource_j : ((exists gsp_beta_height_predecessor_injective_source_j. gsp_beta_height_predecessor_injective_source_j + S (S r) = S ((S (j)) * mc)) /\ exists gsp_beta_quotient_predecessor_injective_source_j. mb = gsp_beta_quotient_predecessor_injective_source_j * S ((S (j)) * mc) + (S r))
  31. 0031specialize beta_magnitude_predecessor_recode_reflect mb
  32. 0032specialize beta_magnitude_predecessor_recode_reflect mc
  33. 0033specialize beta_magnitude_predecessor_recode_reflect rb
  34. 0034specialize beta_magnitude_predecessor_recode_reflect rc
  35. 0035specialize beta_magnitude_predecessor_recode_reflect l
  36. 0036specialize beta_magnitude_predecessor_recode_reflect l
  37. 0037specialize beta_magnitude_predecessor_recode_reflect j
  38. 0038specialize beta_magnitude_predecessor_recode_reflect r
  39. 0039apply beta_magnitude_predecessor_recode_reflect
  40. 0040exact hrange
  41. 0041exact hrecode
  42. 0042exact hj
  43. 0043exact htarget_j
  44. 0044specialize hsource_injective i
  45. 0045specialize hsource_injective j
  46. 0046specialize hsource_injective (S r)
  47. 0047apply hsource_injective
  48. 0048exact hi
  49. 0049exact hj
  50. 0050exact hsource_i
  51. 0051exact hsource_j