PA003T

beta_range_injective

Stable checked-use theorem · independently closed

Equal decoded values in one consecutive range have equal indices.

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 b c a l i j x y. (forall ff_i_generic. (exists ff_lt_generic_bound. ff_lt_generic_bound + S ff_i_generic = l) -> (((exists ff_h_generic_decoded. ff_h_generic_decoded + S (a + ff_i_generic) = S ((S (ff_i_generic)) * c)) /\ exists ff_q_generic_decoded. b = ff_q_generic_decoded * S ((S (ff_i_generic)) * c) + (a + ff_i_generic)))) -> (exists gh_lt_generic_i. gh_lt_generic_i + S i = l) -> (exists gh_lt_generic_j. gh_lt_generic_j + S j = l) -> (((exists ff_h_generic_i. ff_h_generic_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_generic_i. b = ff_q_generic_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_generic_j. ff_h_generic_j + S (y) = S ((S (j)) * c)) /\ exists ff_q_generic_j. b = ff_q_generic_j * S ((S (j)) * c) + (y))) -> x = y -> i = j

Structural proof guide

Generated structural guide

Equal decoded values in one consecutive range have equal indices.

Use the direct prerequisites beta_range_entry_eq, add_left_cancel as previously established PA formulas.

The proof proceeds by intermediate claims (3).

Referenced ingredients

PA0032 beta_range_entry_eq PA002B add_left_cancel

Proof neighborhood

Direct dependencies

PA0032 beta_range_entry_eq PA002B add_left_cancel

Direct dependents

PA007C gauss_signed_half_magnitude_injective

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

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

Named ingredients (2)
beta range entry eqadd left cancel
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro a
  4. L4
    intro l
  5. L5
    intro i
  6. L6
    intro j
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro hrange
  10. L10
    intro hi
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hj
  2. L12
    intro hxi
  3. L13
    intro hyj
  4. L14
    intro hxy
03Establish hxiaL15–24

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

  1. L15
    have hxia : x = a + i
  2. L16
    specialize beta_range_entry_eq b
  3. L17
    specialize beta_range_entry_eq c
  4. L18
    specialize beta_range_entry_eq a
  5. L19
    specialize beta_range_entry_eq l
  6. L20
    specialize beta_range_entry_eq i
  7. L21
    specialize beta_range_entry_eq x
  8. L22
    apply beta_range_entry_eq
  9. L23
    exact hrange
  10. L24
    exact hi
04Use earlier factsL25–25

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

  1. L25
    exact hxi
05Establish hyjaL26–35

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

  1. L26
    have hyja : y = a + j
  2. L27
    specialize beta_range_entry_eq b
  3. L28
    specialize beta_range_entry_eq c
  4. L29
    specialize beta_range_entry_eq a
  5. L30
    specialize beta_range_entry_eq l
  6. L31
    specialize beta_range_entry_eq j
  7. L32
    specialize beta_range_entry_eq y
  8. L33
    apply beta_range_entry_eq
  9. L34
    exact hrange
  10. L35
    exact hj
06Use earlier factsL36–36

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

  1. L36
    exact hyj
07Establish haijL37–46

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

  1. L37
    have haij : a + i = a + j
  2. L38
    trans x
  3. L39
    symm
  4. L40
    exact hxia
  5. L41
    trans y
  6. L42
    exact hxy
  7. L43
    exact hyja
  8. L44
    specialize add_left_cancel a
  9. L45
    specialize add_left_cancel i
  10. L46
    specialize add_left_cancel j
08Use earlier factsL47–48

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

  1. L47
    apply add_left_cancel
  2. L48
    exact haij

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro l
  5. 0005intro i
  6. 0006intro j
  7. 0007intro x
  8. 0008intro y
  9. 0009intro hrange
  10. 0010intro hi
  11. 0011intro hj
  12. 0012intro hxi
  13. 0013intro hyj
  14. 0014intro hxy
  15. 0015have hxia : x = a + i
  16. 0016specialize beta_range_entry_eq b
  17. 0017specialize beta_range_entry_eq c
  18. 0018specialize beta_range_entry_eq a
  19. 0019specialize beta_range_entry_eq l
  20. 0020specialize beta_range_entry_eq i
  21. 0021specialize beta_range_entry_eq x
  22. 0022apply beta_range_entry_eq
  23. 0023exact hrange
  24. 0024exact hi
  25. 0025exact hxi
  26. 0026have hyja : y = a + j
  27. 0027specialize beta_range_entry_eq b
  28. 0028specialize beta_range_entry_eq c
  29. 0029specialize beta_range_entry_eq a
  30. 0030specialize beta_range_entry_eq l
  31. 0031specialize beta_range_entry_eq j
  32. 0032specialize beta_range_entry_eq y
  33. 0033apply beta_range_entry_eq
  34. 0034exact hrange
  35. 0035exact hj
  36. 0036exact hyj
  37. 0037have haij : a + i = a + j
  38. 0038trans x
  39. 0039symm
  40. 0040exact hxia
  41. 0041trans y
  42. 0042exact hxy
  43. 0043exact hyja
  44. 0044specialize add_left_cancel a
  45. 0045specialize add_left_cancel i
  46. 0046specialize add_left_cancel j
  47. 0047apply add_left_cancel
  48. 0048exact haij