CD0022

finite_modular_set_pullback_exists

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

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

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.

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ p. ∀ n. ∀ t. ¬p = 0 → BitCount(b,c,p,n) → ∃ x. ∃ y. BitCount(x,y,p,n) ∧ ModularSetPullback(b,c,x,y,p,t)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ModularSetPullback(b,c,d,e,p,t) · 1Lt(a,b) · 7ModEq(m,a,b) · 1BetaAt(b,c,i,x) · 7AllBits(b,c,l) · 1BitCount(b,c,l,z) · 3

Actual proof prerequisites

finite_modular_translation_indices_existsfinite_beta_composition_existsfinite_modular_composition_all_bitsbit_count_exists · checked external prerequisitefinite_modular_translation_indices_permutationbeta_sum_permutation_invariant · checked external prerequisitefinite_modular_composition_pullback
Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

All 88 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (5)
finite modular translation indices existsfinite beta composition existsfinite modular composition all bitsfinite modular translation indices permutationfinite modular composition pullback
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 : ∃ r. ∃ s. ∀ fms_i_indices. Lt(fms_i_indices,p) → ∃ x. BetaAt(r,s,fms_i_indices,x) ∧ (Lt(x,p) ∧ ModEq(p,fms_i_indices + t,x))Definitions: Lt(fms_i_indices,p)BetaAt(r,s,fms_i_indices,x)Lt(x,p)ModEq(p,fms_i_indices + t,x)Original native command in the exact edition
  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: 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)Original native command in the exact edition
  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 : AllBits(x2,x3,p)Definitions: AllBits(x2,x3,p)Original native command in the exact edition
  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(x2,x3,p,m)Original native command in the exact edition
  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: Lt(y,p)BetaAt(x,x1,y,z)Lt(z,p)BetaAt(x,x1,y,n)BetaAt(x,x1,z,n)Original native command in the exact edition
  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 defined 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 : ∃ r. ∃ s. ∀ fms_i_indices. Lt(fms_i_indices,p) → ∃ x. BetaAt(r,s,fms_i_indices,x) ∧ (Lt(x,p) ∧ ModEq(p,fms_i_indices + t,x))
  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 : ∃ 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)
  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 : AllBits(x2,x3,p)
  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 : ∃ m. BitCount(x2,x3,p,m)
  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 : (∀ 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)
  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