PA00B3

beta_magnitude_predecessor_recode_surjective

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

The predecessor code covers every value 0,...,l-1 by constructive finite pigeonhole.

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 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_value_predecessor_transport_target_surjective. (exists fp_gap_predecessor_transport_target_surjective_value. fp_gap_predecessor_transport_target_surjective_value + S fp_value_predecessor_transport_target_surjective = l) -> exists fp_i_predecessor_transport_target_surjective. ((exists fp_gap_predecessor_transport_target_surjective_index. fp_gap_predecessor_transport_target_surjective_index + S fp_i_predecessor_transport_target_surjective = l) /\ (((exists ff_h_predecessor_transport_target_surjective_entry. ff_h_predecessor_transport_target_surjective_entry + S (fp_value_predecessor_transport_target_surjective) = S ((S (fp_i_predecessor_transport_target_surjective)) * rc)) /\ exists ff_q_predecessor_transport_target_surjective_entry. rb = ff_q_predecessor_transport_target_surjective_entry * S ((S (fp_i_predecessor_transport_target_surjective)) * rc) + (fp_value_predecessor_transport_target_surjective)))))

Structural proof guide

Generated structural guide

The predecessor code covers every value 0,...,l-1 by constructive finite pigeonhole.

Use the direct prerequisites beta_magnitude_predecessor_recode_bounded, beta_magnitude_predecessor_recode_injective, finite_bounded_injective_surjective as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA007S beta_magnitude_predecessor_recode_bounded PA007U beta_magnitude_predecessor_recode_injective PA004W finite_bounded_injective_surjective

Proof neighborhood

Direct dependencies

PA007S beta_magnitude_predecessor_recode_bounded PA007U beta_magnitude_predecessor_recode_injective PA004W finite_bounded_injective_surjective

Direct dependents

PA00B4 finite_bounded_nonendpoint_injective_coverage

Formal native tactic body

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

Read the argument

Proof checkpoints

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

Named ingredients (3)
beta magnitude predecessor recode boundedbeta magnitude predecessor recode injectivefinite bounded injective surjective

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

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
02Establish hboundedL9–17

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

  1. L9
    have hbounded : BoundedPrefix(rb,rc,l)Definitions: BoundedPrefix
  2. L10
    specialize beta_magnitude_predecessor_recode_bounded mb
  3. L11
    specialize beta_magnitude_predecessor_recode_bounded mc
  4. L12
    specialize beta_magnitude_predecessor_recode_bounded rb
  5. L13
    specialize beta_magnitude_predecessor_recode_bounded rc
  6. L14
    specialize beta_magnitude_predecessor_recode_bounded l
  7. L15
    apply beta_magnitude_predecessor_recode_bounded
  8. L16
    exact hrange
  9. L17
    exact hrecode
03Establish hinjectiveL18–27

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

  1. L18
    have hinjective : InjectivePrefix(rb,rc,l)Definitions: InjectivePrefix
  2. L19
    specialize beta_magnitude_predecessor_recode_injective mb
  3. L20
    specialize beta_magnitude_predecessor_recode_injective mc
  4. L21
    specialize beta_magnitude_predecessor_recode_injective rb
  5. L22
    specialize beta_magnitude_predecessor_recode_injective rc
  6. L23
    specialize beta_magnitude_predecessor_recode_injective l
  7. L24
    apply beta_magnitude_predecessor_recode_injective
  8. L25
    exact hrange
  9. L26
    exact hsource_injective
  10. L27
    exact hrecode
04Use earlier factsL28–33

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

  1. L28
    specialize finite_bounded_injective_surjective l
  2. L29
    specialize finite_bounded_injective_surjective rb
  3. L30
    specialize finite_bounded_injective_surjective rc
  4. L31
    apply finite_bounded_injective_surjective
  5. L32
    exact hbounded
  6. L33
    exact hinjective

Library-wide reading audit

Original exact command ledger · 33 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. 0009have hbounded : forall fp_i_predecessor_transport_bounded_result. (exists fp_gap_predecessor_transport_bounded_result_index. fp_gap_predecessor_transport_bounded_result_index + S fp_i_predecessor_transport_bounded_result = l) -> exists fp_value_predecessor_transport_bounded_result. ((((exists ff_h_predecessor_transport_bounded_result_entry. ff_h_predecessor_transport_bounded_result_entry + S (fp_value_predecessor_transport_bounded_result) = S ((S (fp_i_predecessor_transport_bounded_result)) * rc)) /\ exists ff_q_predecessor_transport_bounded_result_entry. rb = ff_q_predecessor_transport_bounded_result_entry * S ((S (fp_i_predecessor_transport_bounded_result)) * rc) + (fp_value_predecessor_transport_bounded_result))) /\ (exists fp_gap_predecessor_transport_bounded_result_value. fp_gap_predecessor_transport_bounded_result_value + S fp_value_predecessor_transport_bounded_result = l))
  10. 0010specialize beta_magnitude_predecessor_recode_bounded mb
  11. 0011specialize beta_magnitude_predecessor_recode_bounded mc
  12. 0012specialize beta_magnitude_predecessor_recode_bounded rb
  13. 0013specialize beta_magnitude_predecessor_recode_bounded rc
  14. 0014specialize beta_magnitude_predecessor_recode_bounded l
  15. 0015apply beta_magnitude_predecessor_recode_bounded
  16. 0016exact hrange
  17. 0017exact hrecode
  18. 0018have hinjective : 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
  19. 0019specialize beta_magnitude_predecessor_recode_injective mb
  20. 0020specialize beta_magnitude_predecessor_recode_injective mc
  21. 0021specialize beta_magnitude_predecessor_recode_injective rb
  22. 0022specialize beta_magnitude_predecessor_recode_injective rc
  23. 0023specialize beta_magnitude_predecessor_recode_injective l
  24. 0024apply beta_magnitude_predecessor_recode_injective
  25. 0025exact hrange
  26. 0026exact hsource_injective
  27. 0027exact hrecode
  28. 0028specialize finite_bounded_injective_surjective l
  29. 0029specialize finite_bounded_injective_surjective rb
  30. 0030specialize finite_bounded_injective_surjective rc
  31. 0031apply finite_bounded_injective_surjective
  32. 0032exact hbounded
  33. 0033exact hinjective