PA003T — beta_range

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.