JT000A

jordan_modulus_zero_excluded

Jordan never counts a purported finite complete residue system modulo zero.

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

∀ k. ∀ j. ¬JordanTotient(k,0,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 k j. ~(((~((k)=0)) /\ (((~((0)=0)) /\ (exists jt_codes_zeromod jt_code_scale_zeromod jt_scales_zeromod jt_scale_scale_zeromod. ((forall jt_i_zeromodenum. (exists jt_gap_zeromodenumsoundindex. jt_gap_zeromodenumsoundindex+S (jt_i_zeromodenum)=(j)) -> exists jt_b_zeromodenum jt_c_zeromodenum. ((((((exists fs_h_jt_zeromodenumsoundcode. fs_h_jt_zeromodenumsoundcode + S (jt_b_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod)) /\ exists fs_q_jt_zeromodenumsoundcode. jt_codes_zeromod = fs_q_jt_zeromodenumsoundcode * S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod) + (jt_b_zeromodenum))) /\ (((exists fs_h_jt_zeromodenumsoundscale. fs_h_jt_zeromodenumsoundscale + S (jt_c_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod)) /\ exists fs_q_jt_zeromodenumsoundscale. jt_scales_zeromod = fs_q_jt_zeromodenumsoundscale * S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod) + (jt_c_zeromodenum))))) /\ (((forall jt_index_zeromodenumbound. (exists jt_gap_zeromodenumboundindex. jt_gap_zeromodenumboundindex+S (jt_index_zeromodenumbound)=(k)) -> exists jt_value_zeromodenumbound. ((((exists fs_h_jt_zeromodenumboundat. fs_h_jt_zeromodenumboundat + S (jt_value_zeromodenumbound) = S ((S (jt_index_zeromodenumbound)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenumboundat. jt_b_zeromodenum = fs_q_jt_zeromodenumboundat * S ((S (jt_index_zeromodenumbound)) * jt_c_zeromodenum) + (jt_value_zeromodenumbound))) /\ (exists jt_gap_zeromodenumboundvalue. jt_gap_zeromodenumboundvalue+S (jt_value_zeromodenumbound)=(0)))) /\ (forall jt_divisor_zeromodenumprimitive. (exists jt_factor_zeromodenumprimitivemodulus. (0)=(jt_divisor_zeromodenumprimitive)*jt_factor_zeromodenumprimitivemodulus) -> (forall jt_index_zeromodenumprimitivecoordinates jt_value_zeromodenumprimitivecoordinates. (exists jt_gap_zeromodenumprimitivecoordinatesindex. jt_gap_zeromodenumprimitivecoordinatesindex+S (jt_index_zeromodenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_zeromodenumprimitivecoordinatesat. fs_h_jt_zeromodenumprimitivecoordinatesat + S (jt_value_zeromodenumprimitivecoordinates) = S ((S (jt_index_zeromodenumprimitivecoordinates)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenumprimitivecoordinatesat. jt_b_zeromodenum = fs_q_jt_zeromodenumprimitivecoordinatesat * S ((S (jt_index_zeromodenumprimitivecoordinates)) * jt_c_zeromodenum) + (jt_value_zeromodenumprimitivecoordinates))) -> (exists jt_factor_zeromodenumprimitivecoordinatesdivides. (jt_value_zeromodenumprimitivecoordinates)=(jt_divisor_zeromodenumprimitive)*jt_factor_zeromodenumprimitivecoordinatesdivides)) -> jt_divisor_zeromodenumprimitive=1))))) /\ (((forall jt_b_zeromodenum jt_c_zeromodenum. (forall jt_index_zeromodenuminputbound. (exists jt_gap_zeromodenuminputboundindex. jt_gap_zeromodenuminputboundindex+S (jt_index_zeromodenuminputbound)=(k)) -> exists jt_value_zeromodenuminputbound. ((((exists fs_h_jt_zeromodenuminputboundat. fs_h_jt_zeromodenuminputboundat + S (jt_value_zeromodenuminputbound) = S ((S (jt_index_zeromodenuminputbound)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenuminputboundat. jt_b_zeromodenum = fs_q_jt_zeromodenuminputboundat * S ((S (jt_index_zeromodenuminputbound)) * jt_c_zeromodenum) + (jt_value_zeromodenuminputbound))) /\ (exists jt_gap_zeromodenuminputboundvalue. jt_gap_zeromodenuminputboundvalue+S (jt_value_zeromodenuminputbound)=(0)))) -> (forall jt_divisor_zeromodenuminputprimitive. (exists jt_factor_zeromodenuminputprimitivemodulus. (0)=(jt_divisor_zeromodenuminputprimitive)*jt_factor_zeromodenuminputprimitivemodulus) -> (forall jt_index_zeromodenuminputprimitivecoordinates jt_value_zeromodenuminputprimitivecoordinates. (exists jt_gap_zeromodenuminputprimitivecoordinatesindex. jt_gap_zeromodenuminputprimitivecoordinatesindex+S (jt_index_zeromodenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_zeromodenuminputprimitivecoordinatesat. fs_h_jt_zeromodenuminputprimitivecoordinatesat + S (jt_value_zeromodenuminputprimitivecoordinates) = S ((S (jt_index_zeromodenuminputprimitivecoordinates)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenuminputprimitivecoordinatesat. jt_b_zeromodenum = fs_q_jt_zeromodenuminputprimitivecoordinatesat * S ((S (jt_index_zeromodenuminputprimitivecoordinates)) * jt_c_zeromodenum) + (jt_value_zeromodenuminputprimitivecoordinates))) -> (exists jt_factor_zeromodenuminputprimitivecoordinatesdivides. (jt_value_zeromodenuminputprimitivecoordinates)=(jt_divisor_zeromodenuminputprimitive)*jt_factor_zeromodenuminputprimitivecoordinatesdivides)) -> jt_divisor_zeromodenuminputprimitive=1) -> exists jt_i_zeromodenum jt_d_zeromodenum jt_e_zeromodenum. ((exists jt_gap_zeromodenumcompleteindex. jt_gap_zeromodenumcompleteindex+S (jt_i_zeromodenum)=(j)) /\ (((((((exists fs_h_jt_zeromodenumcompletecode. fs_h_jt_zeromodenumcompletecode + S (jt_d_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod)) /\ exists fs_q_jt_zeromodenumcompletecode. jt_codes_zeromod = fs_q_jt_zeromodenumcompletecode * S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod) + (jt_d_zeromodenum))) /\ (((exists fs_h_jt_zeromodenumcompletescale. fs_h_jt_zeromodenumcompletescale + S (jt_e_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod)) /\ exists fs_q_jt_zeromodenumcompletescale. jt_scales_zeromod = fs_q_jt_zeromodenumcompletescale * S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod) + (jt_e_zeromodenum))))) /\ (forall jt_index_zeromodenumrepresented jt_left_zeromodenumrepresented jt_right_zeromodenumrepresented. (exists jt_gap_zeromodenumrepresentedindex. jt_gap_zeromodenumrepresentedindex+S (jt_index_zeromodenumrepresented)=(k)) -> (((exists fs_h_jt_zeromodenumrepresentedleft. fs_h_jt_zeromodenumrepresentedleft + S (jt_left_zeromodenumrepresented) = S ((S (jt_index_zeromodenumrepresented)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenumrepresentedleft. jt_b_zeromodenum = fs_q_jt_zeromodenumrepresentedleft * S ((S (jt_index_zeromodenumrepresented)) * jt_c_zeromodenum) + (jt_left_zeromodenumrepresented))) -> (((exists fs_h_jt_zeromodenumrepresentedright. fs_h_jt_zeromodenumrepresentedright + S (jt_right_zeromodenumrepresented) = S ((S (jt_index_zeromodenumrepresented)) * jt_e_zeromodenum)) /\ exists fs_q_jt_zeromodenumrepresentedright. jt_d_zeromodenum = fs_q_jt_zeromodenumrepresentedright * S ((S (jt_index_zeromodenumrepresented)) * jt_e_zeromodenum) + (jt_right_zeromodenumrepresented))) -> jt_left_zeromodenumrepresented=jt_right_zeromodenumrepresented))))) /\ (forall jt_i_zeromodenum jt_h_zeromodenum jt_b_zeromodenum jt_c_zeromodenum jt_d_zeromodenum jt_e_zeromodenum. (exists jt_gap_zeromodenumfirstindex. jt_gap_zeromodenumfirstindex+S (jt_i_zeromodenum)=(j)) -> (exists jt_gap_zeromodenumsecondindex. jt_gap_zeromodenumsecondindex+S (jt_h_zeromodenum)=(j)) -> (((((exists fs_h_jt_zeromodenumfirstcode. fs_h_jt_zeromodenumfirstcode + S (jt_b_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod)) /\ exists fs_q_jt_zeromodenumfirstcode. jt_codes_zeromod = fs_q_jt_zeromodenumfirstcode * S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod) + (jt_b_zeromodenum))) /\ (((exists fs_h_jt_zeromodenumfirstscale. fs_h_jt_zeromodenumfirstscale + S (jt_c_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod)) /\ exists fs_q_jt_zeromodenumfirstscale. jt_scales_zeromod = fs_q_jt_zeromodenumfirstscale * S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod) + (jt_c_zeromodenum))))) -> (((((exists fs_h_jt_zeromodenumsecondcode. fs_h_jt_zeromodenumsecondcode + S (jt_d_zeromodenum) = S ((S (jt_h_zeromodenum)) * jt_code_scale_zeromod)) /\ exists fs_q_jt_zeromodenumsecondcode. jt_codes_zeromod = fs_q_jt_zeromodenumsecondcode * S ((S (jt_h_zeromodenum)) * jt_code_scale_zeromod) + (jt_d_zeromodenum))) /\ (((exists fs_h_jt_zeromodenumsecondscale. fs_h_jt_zeromodenumsecondscale + S (jt_e_zeromodenum) = S ((S (jt_h_zeromodenum)) * jt_scale_scale_zeromod)) /\ exists fs_q_jt_zeromodenumsecondscale. jt_scales_zeromod = fs_q_jt_zeromodenumsecondscale * S ((S (jt_h_zeromodenum)) * jt_scale_scale_zeromod) + (jt_e_zeromodenum))))) -> (forall jt_index_zeromodenumsame jt_left_zeromodenumsame jt_right_zeromodenumsame. (exists jt_gap_zeromodenumsameindex. jt_gap_zeromodenumsameindex+S (jt_index_zeromodenumsame)=(k)) -> (((exists fs_h_jt_zeromodenumsameleft. fs_h_jt_zeromodenumsameleft + S (jt_left_zeromodenumsame) = S ((S (jt_index_zeromodenumsame)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenumsameleft. jt_b_zeromodenum = fs_q_jt_zeromodenumsameleft * S ((S (jt_index_zeromodenumsame)) * jt_c_zeromodenum) + (jt_left_zeromodenumsame))) -> (((exists fs_h_jt_zeromodenumsameright. fs_h_jt_zeromodenumsameright + S (jt_right_zeromodenumsame) = S ((S (jt_index_zeromodenumsame)) * jt_e_zeromodenum)) /\ exists fs_q_jt_zeromodenumsameright. jt_d_zeromodenum = fs_q_jt_zeromodenumsameright * S ((S (jt_index_zeromodenumsame)) * jt_e_zeromodenum) + (jt_right_zeromodenumsame))) -> jt_left_zeromodenumsame=jt_right_zeromodenumsame) -> jt_i_zeromodenum=jt_h_zeromodenum)))))))))

Complete tactic proof in conservative notation

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

7 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 k
  2. L2
    intro j
  3. L3
    intro h
02Separate the logical casesL4–5

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

  1. L4
    cases h
  2. L5
    cases h_right
03Use earlier factsL6–6

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

  1. L6
    apply h_right_left
04Calculate and transport equalitiesL7–7

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

  1. L7
    refl

Library-wide reading audit

Original defined command ledger · 7 lines
  1. 0001intro k
  2. 0002intro j
  3. 0003intro h
  4. 0004cases h
  5. 0005cases h_right
  6. 0006apply h_right_left
  7. 0007refl