JT005B

jordan_totient_at_one

For every positive rank k, J_k(1)=1, proved by the explicit singleton enumeration.

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. ¬k = 0 → JordanTotient(k,1,1)

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

Definition DAG

JordanTotient(k,n,j) · 1

Actual proof prerequisites

succ_ne_zero · checked external prerequisitejordan_unit_modulus_singleton_enumeration
Original expanded first-order statement 
forall k. (~(k=0)) -> (((~((k)=0)) /\ (((~((1)=0)) /\ (exists jt_codes_unit_count jt_code_scale_unit_count jt_scales_unit_count jt_scale_scale_unit_count. ((forall jt_i_unit_countenum. (exists jt_gap_unit_countenumsoundindex. jt_gap_unit_countenumsoundindex+S (jt_i_unit_countenum)=(1)) -> exists jt_b_unit_countenum jt_c_unit_countenum. ((((((exists fs_h_jt_unit_countenumsoundcode. fs_h_jt_unit_countenumsoundcode + S (jt_b_unit_countenum) = S ((S (jt_i_unit_countenum)) * jt_code_scale_unit_count)) /\ exists fs_q_jt_unit_countenumsoundcode. jt_codes_unit_count = fs_q_jt_unit_countenumsoundcode * S ((S (jt_i_unit_countenum)) * jt_code_scale_unit_count) + (jt_b_unit_countenum))) /\ (((exists fs_h_jt_unit_countenumsoundscale. fs_h_jt_unit_countenumsoundscale + S (jt_c_unit_countenum) = S ((S (jt_i_unit_countenum)) * jt_scale_scale_unit_count)) /\ exists fs_q_jt_unit_countenumsoundscale. jt_scales_unit_count = fs_q_jt_unit_countenumsoundscale * S ((S (jt_i_unit_countenum)) * jt_scale_scale_unit_count) + (jt_c_unit_countenum))))) /\ (((forall jt_index_unit_countenumbound. (exists jt_gap_unit_countenumboundindex. jt_gap_unit_countenumboundindex+S (jt_index_unit_countenumbound)=(k)) -> exists jt_value_unit_countenumbound. ((((exists fs_h_jt_unit_countenumboundat. fs_h_jt_unit_countenumboundat + S (jt_value_unit_countenumbound) = S ((S (jt_index_unit_countenumbound)) * jt_c_unit_countenum)) /\ exists fs_q_jt_unit_countenumboundat. jt_b_unit_countenum = fs_q_jt_unit_countenumboundat * S ((S (jt_index_unit_countenumbound)) * jt_c_unit_countenum) + (jt_value_unit_countenumbound))) /\ (exists jt_gap_unit_countenumboundvalue. jt_gap_unit_countenumboundvalue+S (jt_value_unit_countenumbound)=(1)))) /\ (forall jt_divisor_unit_countenumprimitive. (exists jt_factor_unit_countenumprimitivemodulus. (1)=(jt_divisor_unit_countenumprimitive)*jt_factor_unit_countenumprimitivemodulus) -> (forall jt_index_unit_countenumprimitivecoordinates jt_value_unit_countenumprimitivecoordinates. (exists jt_gap_unit_countenumprimitivecoordinatesindex. jt_gap_unit_countenumprimitivecoordinatesindex+S (jt_index_unit_countenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unit_countenumprimitivecoordinatesat. fs_h_jt_unit_countenumprimitivecoordinatesat + S (jt_value_unit_countenumprimitivecoordinates) = S ((S (jt_index_unit_countenumprimitivecoordinates)) * jt_c_unit_countenum)) /\ exists fs_q_jt_unit_countenumprimitivecoordinatesat. jt_b_unit_countenum = fs_q_jt_unit_countenumprimitivecoordinatesat * S ((S (jt_index_unit_countenumprimitivecoordinates)) * jt_c_unit_countenum) + (jt_value_unit_countenumprimitivecoordinates))) -> (exists jt_factor_unit_countenumprimitivecoordinatesdivides. (jt_value_unit_countenumprimitivecoordinates)=(jt_divisor_unit_countenumprimitive)*jt_factor_unit_countenumprimitivecoordinatesdivides)) -> jt_divisor_unit_countenumprimitive=1))))) /\ (((forall jt_b_unit_countenum jt_c_unit_countenum. (forall jt_index_unit_countenuminputbound. (exists jt_gap_unit_countenuminputboundindex. jt_gap_unit_countenuminputboundindex+S (jt_index_unit_countenuminputbound)=(k)) -> exists jt_value_unit_countenuminputbound. ((((exists fs_h_jt_unit_countenuminputboundat. fs_h_jt_unit_countenuminputboundat + S (jt_value_unit_countenuminputbound) = S ((S (jt_index_unit_countenuminputbound)) * jt_c_unit_countenum)) /\ exists fs_q_jt_unit_countenuminputboundat. jt_b_unit_countenum = fs_q_jt_unit_countenuminputboundat * S ((S (jt_index_unit_countenuminputbound)) * jt_c_unit_countenum) + (jt_value_unit_countenuminputbound))) /\ (exists jt_gap_unit_countenuminputboundvalue. jt_gap_unit_countenuminputboundvalue+S (jt_value_unit_countenuminputbound)=(1)))) -> (forall jt_divisor_unit_countenuminputprimitive. (exists jt_factor_unit_countenuminputprimitivemodulus. (1)=(jt_divisor_unit_countenuminputprimitive)*jt_factor_unit_countenuminputprimitivemodulus) -> (forall jt_index_unit_countenuminputprimitivecoordinates jt_value_unit_countenuminputprimitivecoordinates. (exists jt_gap_unit_countenuminputprimitivecoordinatesindex. jt_gap_unit_countenuminputprimitivecoordinatesindex+S (jt_index_unit_countenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unit_countenuminputprimitivecoordinatesat. fs_h_jt_unit_countenuminputprimitivecoordinatesat + S (jt_value_unit_countenuminputprimitivecoordinates) = S ((S (jt_index_unit_countenuminputprimitivecoordinates)) * jt_c_unit_countenum)) /\ exists fs_q_jt_unit_countenuminputprimitivecoordinatesat. jt_b_unit_countenum = fs_q_jt_unit_countenuminputprimitivecoordinatesat * S ((S (jt_index_unit_countenuminputprimitivecoordinates)) * jt_c_unit_countenum) + (jt_value_unit_countenuminputprimitivecoordinates))) -> (exists jt_factor_unit_countenuminputprimitivecoordinatesdivides. (jt_value_unit_countenuminputprimitivecoordinates)=(jt_divisor_unit_countenuminputprimitive)*jt_factor_unit_countenuminputprimitivecoordinatesdivides)) -> jt_divisor_unit_countenuminputprimitive=1) -> exists jt_i_unit_countenum jt_d_unit_countenum jt_e_unit_countenum. ((exists jt_gap_unit_countenumcompleteindex. jt_gap_unit_countenumcompleteindex+S (jt_i_unit_countenum)=(1)) /\ (((((((exists fs_h_jt_unit_countenumcompletecode. fs_h_jt_unit_countenumcompletecode + S (jt_d_unit_countenum) = S ((S (jt_i_unit_countenum)) * jt_code_scale_unit_count)) /\ exists fs_q_jt_unit_countenumcompletecode. jt_codes_unit_count = fs_q_jt_unit_countenumcompletecode * S ((S (jt_i_unit_countenum)) * jt_code_scale_unit_count) + (jt_d_unit_countenum))) /\ (((exists fs_h_jt_unit_countenumcompletescale. fs_h_jt_unit_countenumcompletescale + S (jt_e_unit_countenum) = S ((S (jt_i_unit_countenum)) * jt_scale_scale_unit_count)) /\ exists fs_q_jt_unit_countenumcompletescale. jt_scales_unit_count = fs_q_jt_unit_countenumcompletescale * S ((S (jt_i_unit_countenum)) * jt_scale_scale_unit_count) + (jt_e_unit_countenum))))) /\ (forall jt_index_unit_countenumrepresented jt_left_unit_countenumrepresented jt_right_unit_countenumrepresented. (exists jt_gap_unit_countenumrepresentedindex. jt_gap_unit_countenumrepresentedindex+S (jt_index_unit_countenumrepresented)=(k)) -> (((exists fs_h_jt_unit_countenumrepresentedleft. fs_h_jt_unit_countenumrepresentedleft + S (jt_left_unit_countenumrepresented) = S ((S (jt_index_unit_countenumrepresented)) * jt_c_unit_countenum)) /\ exists fs_q_jt_unit_countenumrepresentedleft. jt_b_unit_countenum = fs_q_jt_unit_countenumrepresentedleft * S ((S (jt_index_unit_countenumrepresented)) * jt_c_unit_countenum) + (jt_left_unit_countenumrepresented))) -> (((exists fs_h_jt_unit_countenumrepresentedright. fs_h_jt_unit_countenumrepresentedright + S (jt_right_unit_countenumrepresented) = S ((S (jt_index_unit_countenumrepresented)) * jt_e_unit_countenum)) /\ exists fs_q_jt_unit_countenumrepresentedright. jt_d_unit_countenum = fs_q_jt_unit_countenumrepresentedright * S ((S (jt_index_unit_countenumrepresented)) * jt_e_unit_countenum) + (jt_right_unit_countenumrepresented))) -> jt_left_unit_countenumrepresented=jt_right_unit_countenumrepresented))))) /\ (forall jt_i_unit_countenum jt_h_unit_countenum jt_b_unit_countenum jt_c_unit_countenum jt_d_unit_countenum jt_e_unit_countenum. (exists jt_gap_unit_countenumfirstindex. jt_gap_unit_countenumfirstindex+S (jt_i_unit_countenum)=(1)) -> (exists jt_gap_unit_countenumsecondindex. jt_gap_unit_countenumsecondindex+S (jt_h_unit_countenum)=(1)) -> (((((exists fs_h_jt_unit_countenumfirstcode. fs_h_jt_unit_countenumfirstcode + S (jt_b_unit_countenum) = S ((S (jt_i_unit_countenum)) * jt_code_scale_unit_count)) /\ exists fs_q_jt_unit_countenumfirstcode. jt_codes_unit_count = fs_q_jt_unit_countenumfirstcode * S ((S (jt_i_unit_countenum)) * jt_code_scale_unit_count) + (jt_b_unit_countenum))) /\ (((exists fs_h_jt_unit_countenumfirstscale. fs_h_jt_unit_countenumfirstscale + S (jt_c_unit_countenum) = S ((S (jt_i_unit_countenum)) * jt_scale_scale_unit_count)) /\ exists fs_q_jt_unit_countenumfirstscale. jt_scales_unit_count = fs_q_jt_unit_countenumfirstscale * S ((S (jt_i_unit_countenum)) * jt_scale_scale_unit_count) + (jt_c_unit_countenum))))) -> (((((exists fs_h_jt_unit_countenumsecondcode. fs_h_jt_unit_countenumsecondcode + S (jt_d_unit_countenum) = S ((S (jt_h_unit_countenum)) * jt_code_scale_unit_count)) /\ exists fs_q_jt_unit_countenumsecondcode. jt_codes_unit_count = fs_q_jt_unit_countenumsecondcode * S ((S (jt_h_unit_countenum)) * jt_code_scale_unit_count) + (jt_d_unit_countenum))) /\ (((exists fs_h_jt_unit_countenumsecondscale. fs_h_jt_unit_countenumsecondscale + S (jt_e_unit_countenum) = S ((S (jt_h_unit_countenum)) * jt_scale_scale_unit_count)) /\ exists fs_q_jt_unit_countenumsecondscale. jt_scales_unit_count = fs_q_jt_unit_countenumsecondscale * S ((S (jt_h_unit_countenum)) * jt_scale_scale_unit_count) + (jt_e_unit_countenum))))) -> (forall jt_index_unit_countenumsame jt_left_unit_countenumsame jt_right_unit_countenumsame. (exists jt_gap_unit_countenumsameindex. jt_gap_unit_countenumsameindex+S (jt_index_unit_countenumsame)=(k)) -> (((exists fs_h_jt_unit_countenumsameleft. fs_h_jt_unit_countenumsameleft + S (jt_left_unit_countenumsame) = S ((S (jt_index_unit_countenumsame)) * jt_c_unit_countenum)) /\ exists fs_q_jt_unit_countenumsameleft. jt_b_unit_countenum = fs_q_jt_unit_countenumsameleft * S ((S (jt_index_unit_countenumsame)) * jt_c_unit_countenum) + (jt_left_unit_countenumsame))) -> (((exists fs_h_jt_unit_countenumsameright. fs_h_jt_unit_countenumsameright + S (jt_right_unit_countenumsame) = S ((S (jt_index_unit_countenumsame)) * jt_e_unit_countenum)) /\ exists fs_q_jt_unit_countenumsameright. jt_d_unit_countenum = fs_q_jt_unit_countenumsameright * S ((S (jt_index_unit_countenumsame)) * jt_e_unit_countenum) + (jt_right_unit_countenumsame))) -> jt_left_unit_countenumsame=jt_right_unit_countenumsame) -> jt_i_unit_countenum=jt_h_unit_countenum)))))))))

Complete tactic proof in conservative notation

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

13 script commands · 7 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 unit modulus singleton enumeration
01Fix variables and assumptionsL1–2

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

  1. L1
    intro k
  2. L2
    intro hk
02Separate the logical casesL3–3

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

  1. L3
    split
03Use earlier factsL4–4

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

  1. L4
    exact hk
04Separate the logical casesL5–5

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

  1. L5
    split
05Use earlier factsL6–7

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

  1. L6
    specialize succ_ne_zero (0)
  2. L7
    apply succ_ne_zero
06Construct an explicit witnessL8–11

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

  1. L8
    exists 0
  2. L9
    exists 0
  3. L10
    exists 0
  4. L11
    exists 0
07Use earlier factsL12–13

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

  1. L12
    specialize jordan_unit_modulus_singleton_enumeration (k)
  2. L13
    apply jordan_unit_modulus_singleton_enumeration

Library-wide reading audit

Original defined command ledger · 13 lines
  1. 0001intro k
  2. 0002intro hk
  3. 0003split
  4. 0004exact hk
  5. 0005split
  6. 0006specialize succ_ne_zero (0)
  7. 0007apply succ_ne_zero
  8. 0008exists 0
  9. 0009exists 0
  10. 0010exists 0
  11. 0011exists 0
  12. 0012specialize jordan_unit_modulus_singleton_enumeration (k)
  13. 0013apply jordan_unit_modulus_singleton_enumeration