PA006A — beta_range_transport

Exact expanded PA statement

forall b c z d a l. (forall ff_i_transport_l. (exists ff_lt_transport_l_bound. ff_lt_transport_l_bound + S ff_i_transport_l = l) -> (((exists ff_h_transport_l_decoded. ff_h_transport_l_decoded + S (a + ff_i_transport_l) = S ((S (ff_i_transport_l)) * c)) /\ exists ff_q_transport_l_decoded. b = ff_q_transport_l_decoded * S ((S (ff_i_transport_l)) * c) + (a + ff_i_transport_l)))) -> (forall ff_i_transport_r. (exists ff_lt_transport_r_bound. ff_lt_transport_r_bound + S ff_i_transport_r = l) -> (((exists ff_h_transport_r_decoded. ff_h_transport_r_decoded + S (a + ff_i_transport_r) = S ((S (ff_i_transport_r)) * d)) /\ exists ff_q_transport_r_decoded. z = ff_q_transport_r_decoded * S ((S (ff_i_transport_r)) * d) + (a + ff_i_transport_r)))) -> forall i x. (exists h. h + S i = l) -> (((exists ff_h_range_transport_x. ff_h_range_transport_x + S (x) = S ((S (i)) * c)) /\ exists ff_q_range_transport_x. b = ff_q_range_transport_x * S ((S (i)) * c) + (x))) -> (((exists ff_h_range_transport_y. ff_h_range_transport_y + S (x) = S ((S (i)) * d)) /\ exists ff_q_range_transport_y. z = ff_q_range_transport_y * S ((S (i)) * d) + (x)))

Structural proof guide

Generated structural guide

Two Range codes preserve every decoded entry extensionally.

Use the direct prerequisites beta_range_entry_eq as previously established PA formulas.

The proof proceeds by intermediate claims (1), equality transport (2).

Referenced ingredients

PA0032 beta_range_entry_eq

Proof neighborhood

Direct dependencies

PA0032 beta_range_entry_eq

Direct dependents

PA006B factorial_functional

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.