JT000C

jordan_primitive_tuple_product_components

Both primitive projections follow even without coprimality of the moduli.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ B. ∀ C. ∀ k. JordanPrimitiveTuple(a · b,B,C,k) → JordanPrimitiveTuple(a,B,C,k) ∧ JordanPrimitiveTuple(b,B,C,k)

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

Definition DAG

JordanPrimitiveTuple(n,b,c,k) · 3

Actual proof prerequisites

jordan_primitive_tuple_divisor_modulusmul_comm · checked external prerequisite
Original expanded first-order 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))

Complete tactic proof in conservative notation

All 27 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

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.

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 (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 defined 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