CD0022

finite_modular_set_pullback_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Construct the genuine modular pullback set and prove its exact cardinality is unchanged by the finite permutation.

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 first-order arithmetic statement

forall b c p n t. ~(p=0) -> (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((n)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((n)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_summand. (b) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (c)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_decoded. (b) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (c)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> exists z d. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((n)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((n)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (d))) /\ exists ff_q_fms_count_summand. (z) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (d)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (d))) /\ exists ff_q_fms_count_decoded. (z) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (d)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ (forall fms_i_pullback fms_j_pullback. (exists fms_gap_pullback_i. fms_gap_pullback_i + S (fms_i_pullback) = (p)) -> (exists fms_gap_pullback_j. fms_gap_pullback_j + S (fms_j_pullback) = (p)) -> (exists fms_u_pullback fms_v_pullback. (fms_i_pullback + t) + (p) * fms_u_pullback = (fms_j_pullback) + (p) * fms_v_pullback) -> ((((((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * d)) /\ exists fs_q_fms_pullback_target. z = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * d) + (1))) -> (((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1)))) /\ ((((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1))) -> (((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * d)) /\ exists fs_q_fms_pullback_target. z = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * d) + (1)))))))

Constructive proof overview

Generated structural guide

Construct the genuine modular pullback set and prove its exact cardinality is unchanged by the finite permutation.

The unchanged tactic script uses 7 declared prerequisites and contains 88 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

CD001D finite_modular_translation_indices_exists CD001C finite_beta_composition_exists CD0020 finite_modular_composition_all_bits bit_count_exists Stable theorem; checked-use authorized CD001F finite_modular_translation_indices_permutation beta_sum_permutation_invariant Alpha theorem; checked-use authorized CD0021 finite_modular_composition_pullback

Direct dependents

CD002F finite_modular_sumset_prefix_exists CD0038 finite_modular_dyson_transform_exists CD0046 prime_cauchy_davenport_cover_bound

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

88 script commands · 21 reading checkpoints · 6 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 (5)
finite modular translation indices existsfinite beta composition existsfinite modular composition all bitsfinite modular translation indices permutationfinite modular composition pullback

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–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro p
  4. L4
    intro n
  5. L5
    intro t
  6. L6
    intro hp
  7. L7
    intro hn
02Establish hindicesL8–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular translation indices exists.

  1. L8
    have hindices : exists r s. forall fms_i_indices. (exists fms_gap_indices. fms_gap_indices + S (fms_i_indices) = (p)) -> exists fms_j_indices. (((exists fs_h_fms_indices_entry. fs_h_fms_indices_entry + S (fms_j_indices) = S ((S (fms_i_indices)) * s)) /\ exists fs_q_fms_indices_entry. r = fs_q_fms_indices_entry * S ((S (fms_i_indices)) * s) + (fms_j_indices))) /\ ((exists fms_gap_indices_bound. fms_gap_indices_bound + S (fms_j_indices) = (p)) /\ (exists fms_u_indices fms_v_indices. (fms_i_indices+t) + (p) * fms_u_indices = (fms_j_indices) + (p) * fms_v_indices))
  2. L9
    specialize finite_modular_translation_indices_exists p
  3. L10
    specialize finite_modular_translation_indices_exists t
  4. L11
    specialize finite_modular_translation_indices_exists p
  5. L12
    apply finite_modular_translation_indices_exists
  6. L13
    exact hp
03Separate the logical casesL14–15

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases hindices
  2. L15
    cases hindices_witness
04Establish hcomposeL16–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite beta composition exists.

  1. L16
    have hcompose : ∃ z. ∃ d. ∀ fms_i_compose. ∀ fms_j_compose. ∀ fms_v_compose. Lt(fms_i_compose,p) → BetaAt(x,x1,fms_i_compose,fms_j_compose) → BetaAt(b,c,fms_j_compose,fms_v_compose) → BetaAt(z,d,fms_i_compose,fms_v_compose)Definitions: LtBetaAt
  2. L17
    specialize finite_beta_composition_exists x
  3. L18
    specialize finite_beta_composition_exists x1
  4. L19
    specialize finite_beta_composition_exists b
  5. L20
    specialize finite_beta_composition_exists c
  6. L21
    specialize finite_beta_composition_exists p
  7. L22
    apply finite_beta_composition_exists
05Separate the logical casesL23–24

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L23
    cases hcompose
  2. L24
    cases hcompose_witness
06Establish hbitsL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular composition all bits.

  1. L25
    have hbits : forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (p)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (x3))) /\ exists ff_q_fms_bits_decoded. (x2) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (x3)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))
  2. L26
    specialize finite_modular_composition_all_bits p
  3. L27
    specialize finite_modular_composition_all_bits t
  4. L28
    specialize finite_modular_composition_all_bits x
  5. L29
    specialize finite_modular_composition_all_bits x1
  6. L30
    specialize finite_modular_composition_all_bits b
  7. L31
    specialize finite_modular_composition_all_bits c
  8. L32
    specialize finite_modular_composition_all_bits x2
  9. L33
    specialize finite_modular_composition_all_bits x3
  10. L34
    apply finite_modular_composition_all_bits
07Use earlier factsL35–36

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

  1. L35
    exact hindices_witness_witness
  2. L36
    exact hcompose_witness_witness
08Separate the logical casesL37–37

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L37
    cases hn
09Use earlier factsL38–38

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

  1. L38
    exact hn_right
10Establish hmL39–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bit count exists.

  1. L39
    have hm : ∃ m. BitCount(x2,x3,p,m)Definitions: BitCount
  2. L40
    specialize bit_count_exists x2
  3. L41
    specialize bit_count_exists x3
  4. L42
    specialize bit_count_exists p
  5. L43
    apply bit_count_exists
  6. L44
    exact hbits
11Separate the logical casesL45–45

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L45
    cases hm
12Establish heL46–46

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

  1. L46
    have he : n=x4
13Establish hpermutationL47–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular translation indices permutation.

  1. L47
    have hpermutation : (∀ y. Lt(y,p) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,p)) ∧ (∀ y. ∀ z. ∀ n. Lt(y,p) → Lt(z,p) → BetaAt(x,x1,y,n) → BetaAt(x,x1,z,n) → y = z)Definitions: LtBetaAt
  2. L48
    specialize finite_modular_translation_indices_permutation p
  3. L49
    specialize finite_modular_translation_indices_permutation t
  4. L50
    specialize finite_modular_translation_indices_permutation x
  5. L51
    specialize finite_modular_translation_indices_permutation x1
  6. L52
    apply finite_modular_translation_indices_permutation
  7. L53
    exact hindices_witness_witness
14Separate the logical casesL54–56

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    cases hpermutation
  2. L55
    cases hn
  3. L56
    cases hm_witness
15Use earlier factsL57–66

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

  1. L57
    specialize beta_sum_permutation_invariant p
  2. L58
    specialize beta_sum_permutation_invariant x
  3. L59
    specialize beta_sum_permutation_invariant x1
  4. L60
    specialize beta_sum_permutation_invariant b
  5. L61
    specialize beta_sum_permutation_invariant c
  6. L62
    specialize beta_sum_permutation_invariant x2
  7. L63
    specialize beta_sum_permutation_invariant x3
  8. L64
    specialize beta_sum_permutation_invariant n
  9. L65
    specialize beta_sum_permutation_invariant x4
  10. L66
    apply beta_sum_permutation_invariant
16Use earlier factsL67–71

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

  1. L67
    exact hpermutation_left
  2. L68
    exact hpermutation_right
  3. L69
    exact hcompose_witness_witness
  4. L70
    exact hn_left
  5. L71
    exact hm_witness_left
17Construct an explicit witnessL72–73

Supply the displayed value, then prove that it has the required property.

  1. L72
    exists x2
  2. L73
    exists x3
18Separate the logical casesL74–74

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L74
    split
19Calculate and transport equalitiesL75–76

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L75
    rewrite he
  2. L76
    rewrite he
20Use earlier factsL77–86

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

  1. L77
    exact hm_witness
  2. L78
    specialize finite_modular_composition_pullback p
  3. L79
    specialize finite_modular_composition_pullback t
  4. L80
    specialize finite_modular_composition_pullback x
  5. L81
    specialize finite_modular_composition_pullback x1
  6. L82
    specialize finite_modular_composition_pullback b
  7. L83
    specialize finite_modular_composition_pullback c
  8. L84
    specialize finite_modular_composition_pullback x2
  9. L85
    specialize finite_modular_composition_pullback x3
  10. L86
    apply finite_modular_composition_pullback
21Use earlier factsL87–88

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

  1. L87
    exact hindices_witness_witness
  2. L88
    exact hcompose_witness_witness

Library-wide reading audit

Original exact command ledger · 88 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro p
  4. 0004intro n
  5. 0005intro t
  6. 0006intro hp
  7. 0007intro hn
  8. 0008have hindices : exists r s. forall fms_i_indices. (exists fms_gap_indices. fms_gap_indices + S (fms_i_indices) = (p)) -> exists fms_j_indices. (((exists fs_h_fms_indices_entry. fs_h_fms_indices_entry + S (fms_j_indices) = S ((S (fms_i_indices)) * s)) /\ exists fs_q_fms_indices_entry. r = fs_q_fms_indices_entry * S ((S (fms_i_indices)) * s) + (fms_j_indices))) /\ ((exists fms_gap_indices_bound. fms_gap_indices_bound + S (fms_j_indices) = (p)) /\ (exists fms_u_indices fms_v_indices. (fms_i_indices+t) + (p) * fms_u_indices = (fms_j_indices) + (p) * fms_v_indices))
  9. 0009specialize finite_modular_translation_indices_exists p
  10. 0010specialize finite_modular_translation_indices_exists t
  11. 0011specialize finite_modular_translation_indices_exists p
  12. 0012apply finite_modular_translation_indices_exists
  13. 0013exact hp
  14. 0014cases hindices
  15. 0015cases hindices_witness
  16. 0016have hcompose : exists z d. forall fms_i_compose fms_j_compose fms_v_compose. (exists fms_gap_compose. fms_gap_compose + S (fms_i_compose) = (p)) -> (((exists fs_h_fms_compose_index. fs_h_fms_compose_index + S (fms_j_compose) = S ((S (fms_i_compose)) * x1)) /\ exists fs_q_fms_compose_index. x = fs_q_fms_compose_index * S ((S (fms_i_compose)) * x1) + (fms_j_compose))) -> (((exists fs_h_fms_compose_source. fs_h_fms_compose_source + S (fms_v_compose) = S ((S (fms_j_compose)) * c)) /\ exists fs_q_fms_compose_source. b = fs_q_fms_compose_source * S ((S (fms_j_compose)) * c) + (fms_v_compose))) -> (((exists fs_h_fms_compose_target. fs_h_fms_compose_target + S (fms_v_compose) = S ((S (fms_i_compose)) * d)) /\ exists fs_q_fms_compose_target. z = fs_q_fms_compose_target * S ((S (fms_i_compose)) * d) + (fms_v_compose)))
  17. 0017specialize finite_beta_composition_exists x
  18. 0018specialize finite_beta_composition_exists x1
  19. 0019specialize finite_beta_composition_exists b
  20. 0020specialize finite_beta_composition_exists c
  21. 0021specialize finite_beta_composition_exists p
  22. 0022apply finite_beta_composition_exists
  23. 0023cases hcompose
  24. 0024cases hcompose_witness
  25. 0025have hbits : forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (p)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (x3))) /\ exists ff_q_fms_bits_decoded. (x2) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (x3)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))
  26. 0026specialize finite_modular_composition_all_bits p
  27. 0027specialize finite_modular_composition_all_bits t
  28. 0028specialize finite_modular_composition_all_bits x
  29. 0029specialize finite_modular_composition_all_bits x1
  30. 0030specialize finite_modular_composition_all_bits b
  31. 0031specialize finite_modular_composition_all_bits c
  32. 0032specialize finite_modular_composition_all_bits x2
  33. 0033specialize finite_modular_composition_all_bits x3
  34. 0034apply finite_modular_composition_all_bits
  35. 0035exact hindices_witness_witness
  36. 0036exact hcompose_witness_witness
  37. 0037cases hn
  38. 0038exact hn_right
  39. 0039have hm : exists m. ((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((m)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((m)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (x3))) /\ exists ff_q_fms_count_summand. (x2) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (x3)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (x3))) /\ exists ff_q_fms_count_decoded. (x2) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (x3)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))
  40. 0040specialize bit_count_exists x2
  41. 0041specialize bit_count_exists x3
  42. 0042specialize bit_count_exists p
  43. 0043apply bit_count_exists
  44. 0044exact hbits
  45. 0045cases hm
  46. 0046have he : n=x4
  47. 0047have hpermutation : (forall fp_i_fms_pull_bounded. (exists fp_gap_fms_pull_bounded_index. fp_gap_fms_pull_bounded_index + S fp_i_fms_pull_bounded = p) -> exists fp_value_fms_pull_bounded. ((((exists ff_h_fms_pull_bounded_entry. ff_h_fms_pull_bounded_entry + S (fp_value_fms_pull_bounded) = S ((S (fp_i_fms_pull_bounded)) * x1)) /\ exists ff_q_fms_pull_bounded_entry. x = ff_q_fms_pull_bounded_entry * S ((S (fp_i_fms_pull_bounded)) * x1) + (fp_value_fms_pull_bounded))) /\ (exists fp_gap_fms_pull_bounded_value. fp_gap_fms_pull_bounded_value + S fp_value_fms_pull_bounded = p))) /\ (forall fp_i_fms_pull_injective fp_j_fms_pull_injective fp_value_fms_pull_injective. (exists fp_gap_fms_pull_injective_i. fp_gap_fms_pull_injective_i + S fp_i_fms_pull_injective = p) -> (exists fp_gap_fms_pull_injective_j. fp_gap_fms_pull_injective_j + S fp_j_fms_pull_injective = p) -> (((exists ff_h_fms_pull_injective_left. ff_h_fms_pull_injective_left + S (fp_value_fms_pull_injective) = S ((S (fp_i_fms_pull_injective)) * x1)) /\ exists ff_q_fms_pull_injective_left. x = ff_q_fms_pull_injective_left * S ((S (fp_i_fms_pull_injective)) * x1) + (fp_value_fms_pull_injective))) -> (((exists ff_h_fms_pull_injective_right. ff_h_fms_pull_injective_right + S (fp_value_fms_pull_injective) = S ((S (fp_j_fms_pull_injective)) * x1)) /\ exists ff_q_fms_pull_injective_right. x = ff_q_fms_pull_injective_right * S ((S (fp_j_fms_pull_injective)) * x1) + (fp_value_fms_pull_injective))) -> fp_i_fms_pull_injective = fp_j_fms_pull_injective)
  48. 0048specialize finite_modular_translation_indices_permutation p
  49. 0049specialize finite_modular_translation_indices_permutation t
  50. 0050specialize finite_modular_translation_indices_permutation x
  51. 0051specialize finite_modular_translation_indices_permutation x1
  52. 0052apply finite_modular_translation_indices_permutation
  53. 0053exact hindices_witness_witness
  54. 0054cases hpermutation
  55. 0055cases hn
  56. 0056cases hm_witness
  57. 0057specialize beta_sum_permutation_invariant p
  58. 0058specialize beta_sum_permutation_invariant x
  59. 0059specialize beta_sum_permutation_invariant x1
  60. 0060specialize beta_sum_permutation_invariant b
  61. 0061specialize beta_sum_permutation_invariant c
  62. 0062specialize beta_sum_permutation_invariant x2
  63. 0063specialize beta_sum_permutation_invariant x3
  64. 0064specialize beta_sum_permutation_invariant n
  65. 0065specialize beta_sum_permutation_invariant x4
  66. 0066apply beta_sum_permutation_invariant
  67. 0067exact hpermutation_left
  68. 0068exact hpermutation_right
  69. 0069exact hcompose_witness_witness
  70. 0070exact hn_left
  71. 0071exact hm_witness_left
  72. 0072exists x2
  73. 0073exists x3
  74. 0074split
  75. 0075rewrite he
  76. 0076rewrite he
  77. 0077exact hm_witness
  78. 0078specialize finite_modular_composition_pullback p
  79. 0079specialize finite_modular_composition_pullback t
  80. 0080specialize finite_modular_composition_pullback x
  81. 0081specialize finite_modular_composition_pullback x1
  82. 0082specialize finite_modular_composition_pullback b
  83. 0083specialize finite_modular_composition_pullback c
  84. 0084specialize finite_modular_composition_pullback x2
  85. 0085specialize finite_modular_composition_pullback x3
  86. 0086apply finite_modular_composition_pullback
  87. 0087exact hindices_witness_witness
  88. 0088exact hcompose_witness_witness