JT0007

jordan_tuple_divisor_downward

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

A divisor of a common coordinate divisor is again a common divisor.

Exact expanded first-order arithmetic statement

forall q r b c k. (exists jt_factor_downfactor. (r)=(q)*jt_factor_downfactor) -> (forall jt_index_downsource jt_value_downsource. (exists jt_gap_downsourceindex. jt_gap_downsourceindex+S (jt_index_downsource)=(k)) -> (((exists fs_h_jt_downsourceat. fs_h_jt_downsourceat + S (jt_value_downsource) = S ((S (jt_index_downsource)) * c)) /\ exists fs_q_jt_downsourceat. b = fs_q_jt_downsourceat * S ((S (jt_index_downsource)) * c) + (jt_value_downsource))) -> (exists jt_factor_downsourcedivides. (jt_value_downsource)=(r)*jt_factor_downsourcedivides)) -> (forall jt_index_downtarget jt_value_downtarget. (exists jt_gap_downtargetindex. jt_gap_downtargetindex+S (jt_index_downtarget)=(k)) -> (((exists fs_h_jt_downtargetat. fs_h_jt_downtargetat + S (jt_value_downtarget) = S ((S (jt_index_downtarget)) * c)) /\ exists fs_q_jt_downtargetat. b = fs_q_jt_downtargetat * S ((S (jt_index_downtarget)) * c) + (jt_value_downtarget))) -> (exists jt_factor_downtargetdivides. (jt_value_downtarget)=(q)*jt_factor_downtargetdivides))

Constructive proof overview

Generated structural guide

A divisor of a common coordinate divisor is again a common divisor.

The unchanged tactic script uses 1 declared prerequisite and contains 21 exact native proof lines.

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

Proof neighborhood

Direct dependencies

multiple_trans Alpha theorem; checked-use authorized

Direct dependents

JT000B jordan_primitive_tuple_coprime_product JT005E jordan_prime_power_tuple_primitive_of_not_all_divisible

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

21 script commands · 3 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro q
  2. L2
    intro r
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro k
  6. L6
    intro hqr
  7. L7
    intro hall
  8. L8
    intro i
  9. L9
    intro a
  10. L10
    intro hi
02Fix variables and assumptionsL11–11

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

  1. L11
    intro ha
03Use earlier factsL12–21

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

  1. L12
    specialize multiple_trans (r)
  2. L13
    specialize multiple_trans (q)
  3. L14
    specialize multiple_trans (a)
  4. L15
    apply multiple_trans
  5. L16
    specialize hall (i)
  6. L17
    specialize hall (a)
  7. L18
    apply hall
  8. L19
    exact hi
  9. L20
    exact ha
  10. L21
    exact hqr

Library-wide reading audit

Original exact command ledger · 21 lines
  1. 0001intro q
  2. 0002intro r
  3. 0003intro b
  4. 0004intro c
  5. 0005intro k
  6. 0006intro hqr
  7. 0007intro hall
  8. 0008intro i
  9. 0009intro a
  10. 0010intro hi
  11. 0011intro ha
  12. 0012specialize multiple_trans (r)
  13. 0013specialize multiple_trans (q)
  14. 0014specialize multiple_trans (a)
  15. 0015apply multiple_trans
  16. 0016specialize hall (i)
  17. 0017specialize hall (a)
  18. 0018apply hall
  19. 0019exact hi
  20. 0020exact ha
  21. 0021exact hqr