CD0021

finite_modular_composition_pullback

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

The constructed value-level composition has exact two-way modular-set pullback membership.

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 p t r s b c z d. (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))) -> (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)) * s)) /\ exists fs_q_fms_compose_index. r = fs_q_fms_compose_index * S ((S (fms_i_compose)) * s) + (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)))) -> (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

The constructed value-level composition has exact two-way modular-set pullback membership.

The unchanged tactic script uses 5 declared prerequisites and contains 78 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mod_eq_bounded_unique Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized mod_eq_symm Stable theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized

Direct dependents

CD0022 finite_modular_set_pullback_exists

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

78 script commands · 17 reading checkpoints · 5 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro t
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro z
  8. L8
    intro d
  9. L9
    intro hindices
  10. L10
    intro hcompose
02Fix variables and assumptionsL11–15

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

  1. L11
    intro i
  2. L12
    intro j
  3. L13
    intro hi
  4. L14
    intro hj
  5. L15
    intro hmod
03Establish hkL16–19

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

  1. L16
    have hk : exists k. (((exists fs_h_fms_pullback_index. fs_h_fms_pullback_index + S (k) = S ((S (i)) * s)) /\ exists fs_q_fms_pullback_index. r = fs_q_fms_pullback_index * S ((S (i)) * s) + (k))) /\ ((exists fms_gap_lt. fms_gap_lt + S (k) = (p)) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (k) + (p) * fms_v_mod))
  2. L17
    specialize hindices i
  3. L18
    apply hindices
  4. L19
    exact hi
04Separate the logical casesL20–22

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

  1. L20
    cases hk
  2. L21
    cases hk_witness
  3. L22
    cases hk_witness_right
05Establish heL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq bounded unique.

  1. L23
    have he : x=j
  2. L24
    specialize mod_eq_bounded_unique p
  3. L25
    specialize mod_eq_bounded_unique x
  4. L26
    specialize mod_eq_bounded_unique j
  5. L27
    apply mod_eq_bounded_unique
  6. L28
    exact hk_witness_right_left
  7. L29
    exact hj
  8. L30
    specialize mod_eq_trans p
  9. L31
    specialize mod_eq_trans x
  10. L32
    specialize mod_eq_trans i+t
06Use earlier factsL33–40

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

  1. L33
    specialize mod_eq_trans j
  2. L34
    apply mod_eq_trans
  3. L35
    specialize mod_eq_symm p
  4. L36
    specialize mod_eq_symm i+t
  5. L37
    specialize mod_eq_symm x
  6. L38
    apply mod_eq_symm
  7. L39
    exact hk_witness_right_right
  8. L40
    exact hmod
07Calculate and transport equalitiesL41–42

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

  1. L41
    rewrite he at hk_witness_left
  2. L42
    rewrite he at hk_witness_left
08Separate the logical casesL43–43

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

  1. L43
    split
09Fix variables and assumptionsL44–44

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

  1. L44
    intro ht
10Establish haL45–49

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

  1. L45
    have ha : exists a. ((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (a) = S ((S (j)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (j)) * c) + (a))
  2. L46
    specialize beta_at_exists b
  3. L47
    specialize beta_at_exists c
  4. L48
    specialize beta_at_exists j
  5. L49
    apply beta_at_exists
11Separate the logical casesL50–50

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

  1. L50
    cases ha
12Establish hvL51–58

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

  1. L51
    have hv : ((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (x1) = S ((S (i)) * d)) /\ exists fs_q_fms_pullback_target. z = fs_q_fms_pullback_target * S ((S (i)) * d) + (x1))
  2. L52
    specialize hcompose i
  3. L53
    specialize hcompose j
  4. L54
    specialize hcompose x1
  5. L55
    apply hcompose
  6. L56
    exact hi
  7. L57
    exact hk_witness_left
  8. L58
    exact ha_witness
13Establish honeL59–68

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

  1. L59
    have hone : x1=1
  2. L60
    specialize beta_at_unique z
  3. L61
    specialize beta_at_unique d
  4. L62
    specialize beta_at_unique i
  5. L63
    specialize beta_at_unique x1
  6. L64
    specialize beta_at_unique 1
  7. L65
    apply beta_at_unique
  8. L66
    exact hv
  9. L67
    exact ht
  10. L68
    rewrite hone at ha_witness
14Calculate and transport equalitiesL69–69

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

  1. L69
    rewrite hone at ha_witness
15Use earlier factsL70–70

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

  1. L70
    exact ha_witness
16Fix variables and assumptionsL71–71

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

  1. L71
    intro hs
17Use earlier factsL72–78

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

  1. L72
    specialize hcompose i
  2. L73
    specialize hcompose j
  3. L74
    specialize hcompose 1
  4. L75
    apply hcompose
  5. L76
    exact hi
  6. L77
    exact hk_witness_left
  7. L78
    exact hs

Library-wide reading audit

Original exact command ledger · 78 lines
  1. 0001intro p
  2. 0002intro t
  3. 0003intro r
  4. 0004intro s
  5. 0005intro b
  6. 0006intro c
  7. 0007intro z
  8. 0008intro d
  9. 0009intro hindices
  10. 0010intro hcompose
  11. 0011intro i
  12. 0012intro j
  13. 0013intro hi
  14. 0014intro hj
  15. 0015intro hmod
  16. 0016have hk : exists k. (((exists fs_h_fms_pullback_index. fs_h_fms_pullback_index + S (k) = S ((S (i)) * s)) /\ exists fs_q_fms_pullback_index. r = fs_q_fms_pullback_index * S ((S (i)) * s) + (k))) /\ ((exists fms_gap_lt. fms_gap_lt + S (k) = (p)) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (k) + (p) * fms_v_mod))
  17. 0017specialize hindices i
  18. 0018apply hindices
  19. 0019exact hi
  20. 0020cases hk
  21. 0021cases hk_witness
  22. 0022cases hk_witness_right
  23. 0023have he : x=j
  24. 0024specialize mod_eq_bounded_unique p
  25. 0025specialize mod_eq_bounded_unique x
  26. 0026specialize mod_eq_bounded_unique j
  27. 0027apply mod_eq_bounded_unique
  28. 0028exact hk_witness_right_left
  29. 0029exact hj
  30. 0030specialize mod_eq_trans p
  31. 0031specialize mod_eq_trans x
  32. 0032specialize mod_eq_trans i+t
  33. 0033specialize mod_eq_trans j
  34. 0034apply mod_eq_trans
  35. 0035specialize mod_eq_symm p
  36. 0036specialize mod_eq_symm i+t
  37. 0037specialize mod_eq_symm x
  38. 0038apply mod_eq_symm
  39. 0039exact hk_witness_right_right
  40. 0040exact hmod
  41. 0041rewrite he at hk_witness_left
  42. 0042rewrite he at hk_witness_left
  43. 0043split
  44. 0044intro ht
  45. 0045have ha : exists a. ((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (a) = S ((S (j)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (j)) * c) + (a))
  46. 0046specialize beta_at_exists b
  47. 0047specialize beta_at_exists c
  48. 0048specialize beta_at_exists j
  49. 0049apply beta_at_exists
  50. 0050cases ha
  51. 0051have hv : ((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (x1) = S ((S (i)) * d)) /\ exists fs_q_fms_pullback_target. z = fs_q_fms_pullback_target * S ((S (i)) * d) + (x1))
  52. 0052specialize hcompose i
  53. 0053specialize hcompose j
  54. 0054specialize hcompose x1
  55. 0055apply hcompose
  56. 0056exact hi
  57. 0057exact hk_witness_left
  58. 0058exact ha_witness
  59. 0059have hone : x1=1
  60. 0060specialize beta_at_unique z
  61. 0061specialize beta_at_unique d
  62. 0062specialize beta_at_unique i
  63. 0063specialize beta_at_unique x1
  64. 0064specialize beta_at_unique 1
  65. 0065apply beta_at_unique
  66. 0066exact hv
  67. 0067exact ht
  68. 0068rewrite hone at ha_witness
  69. 0069rewrite hone at ha_witness
  70. 0070exact ha_witness
  71. 0071intro hs
  72. 0072specialize hcompose i
  73. 0073specialize hcompose j
  74. 0074specialize hcompose 1
  75. 0075apply hcompose
  76. 0076exact hi
  77. 0077exact hk_witness_left
  78. 0078exact hs