JT0009

jordan_order_zero_excluded

Jordan is intentionally restricted to positive tuple order.

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

∀ n. ∀ j. ¬JordanTotient(0,n,j)

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

Definition DAG

JordanTotient(k,n,j) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall n j. ~(((~((0)=0)) /\ (((~((n)=0)) /\ (exists jt_codes_zeroorder jt_code_scale_zeroorder jt_scales_zeroorder jt_scale_scale_zeroorder. ((forall jt_i_zeroorderenum. (exists jt_gap_zeroorderenumsoundindex. jt_gap_zeroorderenumsoundindex+S (jt_i_zeroorderenum)=(j)) -> exists jt_b_zeroorderenum jt_c_zeroorderenum. ((((((exists fs_h_jt_zeroorderenumsoundcode. fs_h_jt_zeroorderenumsoundcode + S (jt_b_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumsoundcode. jt_codes_zeroorder = fs_q_jt_zeroorderenumsoundcode * S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder) + (jt_b_zeroorderenum))) /\ (((exists fs_h_jt_zeroorderenumsoundscale. fs_h_jt_zeroorderenumsoundscale + S (jt_c_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumsoundscale. jt_scales_zeroorder = fs_q_jt_zeroorderenumsoundscale * S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder) + (jt_c_zeroorderenum))))) /\ (((forall jt_index_zeroorderenumbound. (exists jt_gap_zeroorderenumboundindex. jt_gap_zeroorderenumboundindex+S (jt_index_zeroorderenumbound)=(0)) -> exists jt_value_zeroorderenumbound. ((((exists fs_h_jt_zeroorderenumboundat. fs_h_jt_zeroorderenumboundat + S (jt_value_zeroorderenumbound) = S ((S (jt_index_zeroorderenumbound)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumboundat. jt_b_zeroorderenum = fs_q_jt_zeroorderenumboundat * S ((S (jt_index_zeroorderenumbound)) * jt_c_zeroorderenum) + (jt_value_zeroorderenumbound))) /\ (exists jt_gap_zeroorderenumboundvalue. jt_gap_zeroorderenumboundvalue+S (jt_value_zeroorderenumbound)=(n)))) /\ (forall jt_divisor_zeroorderenumprimitive. (exists jt_factor_zeroorderenumprimitivemodulus. (n)=(jt_divisor_zeroorderenumprimitive)*jt_factor_zeroorderenumprimitivemodulus) -> (forall jt_index_zeroorderenumprimitivecoordinates jt_value_zeroorderenumprimitivecoordinates. (exists jt_gap_zeroorderenumprimitivecoordinatesindex. jt_gap_zeroorderenumprimitivecoordinatesindex+S (jt_index_zeroorderenumprimitivecoordinates)=(0)) -> (((exists fs_h_jt_zeroorderenumprimitivecoordinatesat. fs_h_jt_zeroorderenumprimitivecoordinatesat + S (jt_value_zeroorderenumprimitivecoordinates) = S ((S (jt_index_zeroorderenumprimitivecoordinates)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumprimitivecoordinatesat. jt_b_zeroorderenum = fs_q_jt_zeroorderenumprimitivecoordinatesat * S ((S (jt_index_zeroorderenumprimitivecoordinates)) * jt_c_zeroorderenum) + (jt_value_zeroorderenumprimitivecoordinates))) -> (exists jt_factor_zeroorderenumprimitivecoordinatesdivides. (jt_value_zeroorderenumprimitivecoordinates)=(jt_divisor_zeroorderenumprimitive)*jt_factor_zeroorderenumprimitivecoordinatesdivides)) -> jt_divisor_zeroorderenumprimitive=1))))) /\ (((forall jt_b_zeroorderenum jt_c_zeroorderenum. (forall jt_index_zeroorderenuminputbound. (exists jt_gap_zeroorderenuminputboundindex. jt_gap_zeroorderenuminputboundindex+S (jt_index_zeroorderenuminputbound)=(0)) -> exists jt_value_zeroorderenuminputbound. ((((exists fs_h_jt_zeroorderenuminputboundat. fs_h_jt_zeroorderenuminputboundat + S (jt_value_zeroorderenuminputbound) = S ((S (jt_index_zeroorderenuminputbound)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenuminputboundat. jt_b_zeroorderenum = fs_q_jt_zeroorderenuminputboundat * S ((S (jt_index_zeroorderenuminputbound)) * jt_c_zeroorderenum) + (jt_value_zeroorderenuminputbound))) /\ (exists jt_gap_zeroorderenuminputboundvalue. jt_gap_zeroorderenuminputboundvalue+S (jt_value_zeroorderenuminputbound)=(n)))) -> (forall jt_divisor_zeroorderenuminputprimitive. (exists jt_factor_zeroorderenuminputprimitivemodulus. (n)=(jt_divisor_zeroorderenuminputprimitive)*jt_factor_zeroorderenuminputprimitivemodulus) -> (forall jt_index_zeroorderenuminputprimitivecoordinates jt_value_zeroorderenuminputprimitivecoordinates. (exists jt_gap_zeroorderenuminputprimitivecoordinatesindex. jt_gap_zeroorderenuminputprimitivecoordinatesindex+S (jt_index_zeroorderenuminputprimitivecoordinates)=(0)) -> (((exists fs_h_jt_zeroorderenuminputprimitivecoordinatesat. fs_h_jt_zeroorderenuminputprimitivecoordinatesat + S (jt_value_zeroorderenuminputprimitivecoordinates) = S ((S (jt_index_zeroorderenuminputprimitivecoordinates)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenuminputprimitivecoordinatesat. jt_b_zeroorderenum = fs_q_jt_zeroorderenuminputprimitivecoordinatesat * S ((S (jt_index_zeroorderenuminputprimitivecoordinates)) * jt_c_zeroorderenum) + (jt_value_zeroorderenuminputprimitivecoordinates))) -> (exists jt_factor_zeroorderenuminputprimitivecoordinatesdivides. (jt_value_zeroorderenuminputprimitivecoordinates)=(jt_divisor_zeroorderenuminputprimitive)*jt_factor_zeroorderenuminputprimitivecoordinatesdivides)) -> jt_divisor_zeroorderenuminputprimitive=1) -> exists jt_i_zeroorderenum jt_d_zeroorderenum jt_e_zeroorderenum. ((exists jt_gap_zeroorderenumcompleteindex. jt_gap_zeroorderenumcompleteindex+S (jt_i_zeroorderenum)=(j)) /\ (((((((exists fs_h_jt_zeroorderenumcompletecode. fs_h_jt_zeroorderenumcompletecode + S (jt_d_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumcompletecode. jt_codes_zeroorder = fs_q_jt_zeroorderenumcompletecode * S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder) + (jt_d_zeroorderenum))) /\ (((exists fs_h_jt_zeroorderenumcompletescale. fs_h_jt_zeroorderenumcompletescale + S (jt_e_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumcompletescale. jt_scales_zeroorder = fs_q_jt_zeroorderenumcompletescale * S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder) + (jt_e_zeroorderenum))))) /\ (forall jt_index_zeroorderenumrepresented jt_left_zeroorderenumrepresented jt_right_zeroorderenumrepresented. (exists jt_gap_zeroorderenumrepresentedindex. jt_gap_zeroorderenumrepresentedindex+S (jt_index_zeroorderenumrepresented)=(0)) -> (((exists fs_h_jt_zeroorderenumrepresentedleft. fs_h_jt_zeroorderenumrepresentedleft + S (jt_left_zeroorderenumrepresented) = S ((S (jt_index_zeroorderenumrepresented)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumrepresentedleft. jt_b_zeroorderenum = fs_q_jt_zeroorderenumrepresentedleft * S ((S (jt_index_zeroorderenumrepresented)) * jt_c_zeroorderenum) + (jt_left_zeroorderenumrepresented))) -> (((exists fs_h_jt_zeroorderenumrepresentedright. fs_h_jt_zeroorderenumrepresentedright + S (jt_right_zeroorderenumrepresented) = S ((S (jt_index_zeroorderenumrepresented)) * jt_e_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumrepresentedright. jt_d_zeroorderenum = fs_q_jt_zeroorderenumrepresentedright * S ((S (jt_index_zeroorderenumrepresented)) * jt_e_zeroorderenum) + (jt_right_zeroorderenumrepresented))) -> jt_left_zeroorderenumrepresented=jt_right_zeroorderenumrepresented))))) /\ (forall jt_i_zeroorderenum jt_h_zeroorderenum jt_b_zeroorderenum jt_c_zeroorderenum jt_d_zeroorderenum jt_e_zeroorderenum. (exists jt_gap_zeroorderenumfirstindex. jt_gap_zeroorderenumfirstindex+S (jt_i_zeroorderenum)=(j)) -> (exists jt_gap_zeroorderenumsecondindex. jt_gap_zeroorderenumsecondindex+S (jt_h_zeroorderenum)=(j)) -> (((((exists fs_h_jt_zeroorderenumfirstcode. fs_h_jt_zeroorderenumfirstcode + S (jt_b_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumfirstcode. jt_codes_zeroorder = fs_q_jt_zeroorderenumfirstcode * S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder) + (jt_b_zeroorderenum))) /\ (((exists fs_h_jt_zeroorderenumfirstscale. fs_h_jt_zeroorderenumfirstscale + S (jt_c_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumfirstscale. jt_scales_zeroorder = fs_q_jt_zeroorderenumfirstscale * S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder) + (jt_c_zeroorderenum))))) -> (((((exists fs_h_jt_zeroorderenumsecondcode. fs_h_jt_zeroorderenumsecondcode + S (jt_d_zeroorderenum) = S ((S (jt_h_zeroorderenum)) * jt_code_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumsecondcode. jt_codes_zeroorder = fs_q_jt_zeroorderenumsecondcode * S ((S (jt_h_zeroorderenum)) * jt_code_scale_zeroorder) + (jt_d_zeroorderenum))) /\ (((exists fs_h_jt_zeroorderenumsecondscale. fs_h_jt_zeroorderenumsecondscale + S (jt_e_zeroorderenum) = S ((S (jt_h_zeroorderenum)) * jt_scale_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumsecondscale. jt_scales_zeroorder = fs_q_jt_zeroorderenumsecondscale * S ((S (jt_h_zeroorderenum)) * jt_scale_scale_zeroorder) + (jt_e_zeroorderenum))))) -> (forall jt_index_zeroorderenumsame jt_left_zeroorderenumsame jt_right_zeroorderenumsame. (exists jt_gap_zeroorderenumsameindex. jt_gap_zeroorderenumsameindex+S (jt_index_zeroorderenumsame)=(0)) -> (((exists fs_h_jt_zeroorderenumsameleft. fs_h_jt_zeroorderenumsameleft + S (jt_left_zeroorderenumsame) = S ((S (jt_index_zeroorderenumsame)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumsameleft. jt_b_zeroorderenum = fs_q_jt_zeroorderenumsameleft * S ((S (jt_index_zeroorderenumsame)) * jt_c_zeroorderenum) + (jt_left_zeroorderenumsame))) -> (((exists fs_h_jt_zeroorderenumsameright. fs_h_jt_zeroorderenumsameright + S (jt_right_zeroorderenumsame) = S ((S (jt_index_zeroorderenumsame)) * jt_e_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumsameright. jt_d_zeroorderenum = fs_q_jt_zeroorderenumsameright * S ((S (jt_index_zeroorderenumsame)) * jt_e_zeroorderenum) + (jt_right_zeroorderenumsame))) -> jt_left_zeroorderenumsame=jt_right_zeroorderenumsame) -> jt_i_zeroorderenum=jt_h_zeroorderenum)))))))))

Complete tactic proof in conservative notation

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

6 script commands · 4 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro j
  3. L3
    intro h
02Separate the logical casesL4–4

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

  1. L4
    cases h
03Use earlier factsL5–5

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

  1. L5
    apply h_left
04Calculate and transport equalitiesL6–6

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

  1. L6
    refl

Library-wide reading audit

Original defined command ledger · 6 lines
  1. 0001intro n
  2. 0002intro j
  3. 0003intro h
  4. 0004cases h
  5. 0005apply h_left
  6. 0006refl