JT000C

jordan_primitive_tuple_product_components

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

Both primitive projections follow even without coprimality of the moduli.

Exact expanded first-order arithmetic statement

forall a b B C k. (forall jt_divisor_componentab. (exists jt_factor_componentabmodulus. (a*b)=(jt_divisor_componentab)*jt_factor_componentabmodulus) -> (forall jt_index_componentabcoordinates jt_value_componentabcoordinates. (exists jt_gap_componentabcoordinatesindex. jt_gap_componentabcoordinatesindex+S (jt_index_componentabcoordinates)=(k)) -> (((exists fs_h_jt_componentabcoordinatesat. fs_h_jt_componentabcoordinatesat + S (jt_value_componentabcoordinates) = S ((S (jt_index_componentabcoordinates)) * C)) /\ exists fs_q_jt_componentabcoordinatesat. B = fs_q_jt_componentabcoordinatesat * S ((S (jt_index_componentabcoordinates)) * C) + (jt_value_componentabcoordinates))) -> (exists jt_factor_componentabcoordinatesdivides. (jt_value_componentabcoordinates)=(jt_divisor_componentab)*jt_factor_componentabcoordinatesdivides)) -> jt_divisor_componentab=1) -> ((forall jt_divisor_componenta. (exists jt_factor_componentamodulus. (a)=(jt_divisor_componenta)*jt_factor_componentamodulus) -> (forall jt_index_componentacoordinates jt_value_componentacoordinates. (exists jt_gap_componentacoordinatesindex. jt_gap_componentacoordinatesindex+S (jt_index_componentacoordinates)=(k)) -> (((exists fs_h_jt_componentacoordinatesat. fs_h_jt_componentacoordinatesat + S (jt_value_componentacoordinates) = S ((S (jt_index_componentacoordinates)) * C)) /\ exists fs_q_jt_componentacoordinatesat. B = fs_q_jt_componentacoordinatesat * S ((S (jt_index_componentacoordinates)) * C) + (jt_value_componentacoordinates))) -> (exists jt_factor_componentacoordinatesdivides. (jt_value_componentacoordinates)=(jt_divisor_componenta)*jt_factor_componentacoordinatesdivides)) -> jt_divisor_componenta=1) /\ (forall jt_divisor_componentb. (exists jt_factor_componentbmodulus. (b)=(jt_divisor_componentb)*jt_factor_componentbmodulus) -> (forall jt_index_componentbcoordinates jt_value_componentbcoordinates. (exists jt_gap_componentbcoordinatesindex. jt_gap_componentbcoordinatesindex+S (jt_index_componentbcoordinates)=(k)) -> (((exists fs_h_jt_componentbcoordinatesat. fs_h_jt_componentbcoordinatesat + S (jt_value_componentbcoordinates) = S ((S (jt_index_componentbcoordinates)) * C)) /\ exists fs_q_jt_componentbcoordinatesat. B = fs_q_jt_componentbcoordinatesat * S ((S (jt_index_componentbcoordinates)) * C) + (jt_value_componentbcoordinates))) -> (exists jt_factor_componentbcoordinatesdivides. (jt_value_componentbcoordinates)=(jt_divisor_componentb)*jt_factor_componentbcoordinatesdivides)) -> jt_divisor_componentb=1))

Constructive proof overview

Generated structural guide

Both primitive projections follow even without coprimality of the moduli.

The unchanged tactic script uses 2 declared prerequisites and contains 27 exact native proof lines.

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

Proof neighborhood

Direct dependencies

JT0006 jordan_primitive_tuple_divisor_modulus mul_comm Alpha theorem; checked-use authorized

Direct dependents

JT0047 jordan_rectangle_crt_covers

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

27 script commands · 8 reading checkpoints · 0 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 (1)
jordan primitive tuple divisor modulus
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro B
  4. L4
    intro C
  5. L5
    intro k
  6. L6
    intro h
02Separate the logical casesL7–7

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

  1. L7
    split
03Use earlier factsL8–13

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

  1. L8
    specialize jordan_primitive_tuple_divisor_modulus (a)
  2. L9
    specialize jordan_primitive_tuple_divisor_modulus (a*b)
  3. L10
    specialize jordan_primitive_tuple_divisor_modulus (B)
  4. L11
    specialize jordan_primitive_tuple_divisor_modulus (C)
  5. L12
    specialize jordan_primitive_tuple_divisor_modulus (k)
  6. L13
    apply jordan_primitive_tuple_divisor_modulus
04Construct an explicit witnessL14–14

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

  1. L14
    exists b
05Calculate and transport equalitiesL15–15

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

  1. L15
    refl
06Use earlier factsL16–22

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

  1. L16
    exact h
  2. L17
    specialize jordan_primitive_tuple_divisor_modulus (b)
  3. L18
    specialize jordan_primitive_tuple_divisor_modulus (a*b)
  4. L19
    specialize jordan_primitive_tuple_divisor_modulus (B)
  5. L20
    specialize jordan_primitive_tuple_divisor_modulus (C)
  6. L21
    specialize jordan_primitive_tuple_divisor_modulus (k)
  7. L22
    apply jordan_primitive_tuple_divisor_modulus
07Construct an explicit witnessL23–23

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

  1. L23
    exists a
08Use earlier factsL24–27

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

  1. L24
    specialize mul_comm (a)
  2. L25
    specialize mul_comm (b)
  3. L26
    apply mul_comm
  4. L27
    exact h

Library-wide reading audit

Original exact command ledger · 27 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro B
  4. 0004intro C
  5. 0005intro k
  6. 0006intro h
  7. 0007split
  8. 0008specialize jordan_primitive_tuple_divisor_modulus (a)
  9. 0009specialize jordan_primitive_tuple_divisor_modulus (a*b)
  10. 0010specialize jordan_primitive_tuple_divisor_modulus (B)
  11. 0011specialize jordan_primitive_tuple_divisor_modulus (C)
  12. 0012specialize jordan_primitive_tuple_divisor_modulus (k)
  13. 0013apply jordan_primitive_tuple_divisor_modulus
  14. 0014exists b
  15. 0015refl
  16. 0016exact h
  17. 0017specialize jordan_primitive_tuple_divisor_modulus (b)
  18. 0018specialize jordan_primitive_tuple_divisor_modulus (a*b)
  19. 0019specialize jordan_primitive_tuple_divisor_modulus (B)
  20. 0020specialize jordan_primitive_tuple_divisor_modulus (C)
  21. 0021specialize jordan_primitive_tuple_divisor_modulus (k)
  22. 0022apply jordan_primitive_tuple_divisor_modulus
  23. 0023exists a
  24. 0024specialize mul_comm (a)
  25. 0025specialize mul_comm (b)
  26. 0026apply mul_comm
  27. 0027exact h