JT005C

jordan_totient_at_one_unique

Every genuine Jordan count modulo one equals one, independently of its beta encoding.

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,1,j) → j = 1

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

Definition DAG

JordanTotient(k,n,j) · 1

Actual proof prerequisites

jordan_totient_count_uniquejordan_totient_at_one
Original expanded first-order statement 
forall k j. (((~((k)=0)) /\ (((~((1)=0)) /\ (exists jt_codes_unit_arbitrary_count jt_code_scale_unit_arbitrary_count jt_scales_unit_arbitrary_count jt_scale_scale_unit_arbitrary_count. ((forall jt_i_unit_arbitrary_countenum. (exists jt_gap_unit_arbitrary_countenumsoundindex. jt_gap_unit_arbitrary_countenumsoundindex+S (jt_i_unit_arbitrary_countenum)=(j)) -> exists jt_b_unit_arbitrary_countenum jt_c_unit_arbitrary_countenum. ((((((exists fs_h_jt_unit_arbitrary_countenumsoundcode. fs_h_jt_unit_arbitrary_countenumsoundcode + S (jt_b_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumsoundcode. jt_codes_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumsoundcode * S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count) + (jt_b_unit_arbitrary_countenum))) /\ (((exists fs_h_jt_unit_arbitrary_countenumsoundscale. fs_h_jt_unit_arbitrary_countenumsoundscale + S (jt_c_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumsoundscale. jt_scales_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumsoundscale * S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count) + (jt_c_unit_arbitrary_countenum))))) /\ (((forall jt_index_unit_arbitrary_countenumbound. (exists jt_gap_unit_arbitrary_countenumboundindex. jt_gap_unit_arbitrary_countenumboundindex+S (jt_index_unit_arbitrary_countenumbound)=(k)) -> exists jt_value_unit_arbitrary_countenumbound. ((((exists fs_h_jt_unit_arbitrary_countenumboundat. fs_h_jt_unit_arbitrary_countenumboundat + S (jt_value_unit_arbitrary_countenumbound) = S ((S (jt_index_unit_arbitrary_countenumbound)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumboundat. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumboundat * S ((S (jt_index_unit_arbitrary_countenumbound)) * jt_c_unit_arbitrary_countenum) + (jt_value_unit_arbitrary_countenumbound))) /\ (exists jt_gap_unit_arbitrary_countenumboundvalue. jt_gap_unit_arbitrary_countenumboundvalue+S (jt_value_unit_arbitrary_countenumbound)=(1)))) /\ (forall jt_divisor_unit_arbitrary_countenumprimitive. (exists jt_factor_unit_arbitrary_countenumprimitivemodulus. (1)=(jt_divisor_unit_arbitrary_countenumprimitive)*jt_factor_unit_arbitrary_countenumprimitivemodulus) -> (forall jt_index_unit_arbitrary_countenumprimitivecoordinates jt_value_unit_arbitrary_countenumprimitivecoordinates. (exists jt_gap_unit_arbitrary_countenumprimitivecoordinatesindex. jt_gap_unit_arbitrary_countenumprimitivecoordinatesindex+S (jt_index_unit_arbitrary_countenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unit_arbitrary_countenumprimitivecoordinatesat. fs_h_jt_unit_arbitrary_countenumprimitivecoordinatesat + S (jt_value_unit_arbitrary_countenumprimitivecoordinates) = S ((S (jt_index_unit_arbitrary_countenumprimitivecoordinates)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumprimitivecoordinatesat. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumprimitivecoordinatesat * S ((S (jt_index_unit_arbitrary_countenumprimitivecoordinates)) * jt_c_unit_arbitrary_countenum) + (jt_value_unit_arbitrary_countenumprimitivecoordinates))) -> (exists jt_factor_unit_arbitrary_countenumprimitivecoordinatesdivides. (jt_value_unit_arbitrary_countenumprimitivecoordinates)=(jt_divisor_unit_arbitrary_countenumprimitive)*jt_factor_unit_arbitrary_countenumprimitivecoordinatesdivides)) -> jt_divisor_unit_arbitrary_countenumprimitive=1))))) /\ (((forall jt_b_unit_arbitrary_countenum jt_c_unit_arbitrary_countenum. (forall jt_index_unit_arbitrary_countenuminputbound. (exists jt_gap_unit_arbitrary_countenuminputboundindex. jt_gap_unit_arbitrary_countenuminputboundindex+S (jt_index_unit_arbitrary_countenuminputbound)=(k)) -> exists jt_value_unit_arbitrary_countenuminputbound. ((((exists fs_h_jt_unit_arbitrary_countenuminputboundat. fs_h_jt_unit_arbitrary_countenuminputboundat + S (jt_value_unit_arbitrary_countenuminputbound) = S ((S (jt_index_unit_arbitrary_countenuminputbound)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenuminputboundat. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenuminputboundat * S ((S (jt_index_unit_arbitrary_countenuminputbound)) * jt_c_unit_arbitrary_countenum) + (jt_value_unit_arbitrary_countenuminputbound))) /\ (exists jt_gap_unit_arbitrary_countenuminputboundvalue. jt_gap_unit_arbitrary_countenuminputboundvalue+S (jt_value_unit_arbitrary_countenuminputbound)=(1)))) -> (forall jt_divisor_unit_arbitrary_countenuminputprimitive. (exists jt_factor_unit_arbitrary_countenuminputprimitivemodulus. (1)=(jt_divisor_unit_arbitrary_countenuminputprimitive)*jt_factor_unit_arbitrary_countenuminputprimitivemodulus) -> (forall jt_index_unit_arbitrary_countenuminputprimitivecoordinates jt_value_unit_arbitrary_countenuminputprimitivecoordinates. (exists jt_gap_unit_arbitrary_countenuminputprimitivecoordinatesindex. jt_gap_unit_arbitrary_countenuminputprimitivecoordinatesindex+S (jt_index_unit_arbitrary_countenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unit_arbitrary_countenuminputprimitivecoordinatesat. fs_h_jt_unit_arbitrary_countenuminputprimitivecoordinatesat + S (jt_value_unit_arbitrary_countenuminputprimitivecoordinates) = S ((S (jt_index_unit_arbitrary_countenuminputprimitivecoordinates)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenuminputprimitivecoordinatesat. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenuminputprimitivecoordinatesat * S ((S (jt_index_unit_arbitrary_countenuminputprimitivecoordinates)) * jt_c_unit_arbitrary_countenum) + (jt_value_unit_arbitrary_countenuminputprimitivecoordinates))) -> (exists jt_factor_unit_arbitrary_countenuminputprimitivecoordinatesdivides. (jt_value_unit_arbitrary_countenuminputprimitivecoordinates)=(jt_divisor_unit_arbitrary_countenuminputprimitive)*jt_factor_unit_arbitrary_countenuminputprimitivecoordinatesdivides)) -> jt_divisor_unit_arbitrary_countenuminputprimitive=1) -> exists jt_i_unit_arbitrary_countenum jt_d_unit_arbitrary_countenum jt_e_unit_arbitrary_countenum. ((exists jt_gap_unit_arbitrary_countenumcompleteindex. jt_gap_unit_arbitrary_countenumcompleteindex+S (jt_i_unit_arbitrary_countenum)=(j)) /\ (((((((exists fs_h_jt_unit_arbitrary_countenumcompletecode. fs_h_jt_unit_arbitrary_countenumcompletecode + S (jt_d_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumcompletecode. jt_codes_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumcompletecode * S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count) + (jt_d_unit_arbitrary_countenum))) /\ (((exists fs_h_jt_unit_arbitrary_countenumcompletescale. fs_h_jt_unit_arbitrary_countenumcompletescale + S (jt_e_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumcompletescale. jt_scales_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumcompletescale * S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count) + (jt_e_unit_arbitrary_countenum))))) /\ (forall jt_index_unit_arbitrary_countenumrepresented jt_left_unit_arbitrary_countenumrepresented jt_right_unit_arbitrary_countenumrepresented. (exists jt_gap_unit_arbitrary_countenumrepresentedindex. jt_gap_unit_arbitrary_countenumrepresentedindex+S (jt_index_unit_arbitrary_countenumrepresented)=(k)) -> (((exists fs_h_jt_unit_arbitrary_countenumrepresentedleft. fs_h_jt_unit_arbitrary_countenumrepresentedleft + S (jt_left_unit_arbitrary_countenumrepresented) = S ((S (jt_index_unit_arbitrary_countenumrepresented)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumrepresentedleft. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumrepresentedleft * S ((S (jt_index_unit_arbitrary_countenumrepresented)) * jt_c_unit_arbitrary_countenum) + (jt_left_unit_arbitrary_countenumrepresented))) -> (((exists fs_h_jt_unit_arbitrary_countenumrepresentedright. fs_h_jt_unit_arbitrary_countenumrepresentedright + S (jt_right_unit_arbitrary_countenumrepresented) = S ((S (jt_index_unit_arbitrary_countenumrepresented)) * jt_e_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumrepresentedright. jt_d_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumrepresentedright * S ((S (jt_index_unit_arbitrary_countenumrepresented)) * jt_e_unit_arbitrary_countenum) + (jt_right_unit_arbitrary_countenumrepresented))) -> jt_left_unit_arbitrary_countenumrepresented=jt_right_unit_arbitrary_countenumrepresented))))) /\ (forall jt_i_unit_arbitrary_countenum jt_h_unit_arbitrary_countenum jt_b_unit_arbitrary_countenum jt_c_unit_arbitrary_countenum jt_d_unit_arbitrary_countenum jt_e_unit_arbitrary_countenum. (exists jt_gap_unit_arbitrary_countenumfirstindex. jt_gap_unit_arbitrary_countenumfirstindex+S (jt_i_unit_arbitrary_countenum)=(j)) -> (exists jt_gap_unit_arbitrary_countenumsecondindex. jt_gap_unit_arbitrary_countenumsecondindex+S (jt_h_unit_arbitrary_countenum)=(j)) -> (((((exists fs_h_jt_unit_arbitrary_countenumfirstcode. fs_h_jt_unit_arbitrary_countenumfirstcode + S (jt_b_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumfirstcode. jt_codes_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumfirstcode * S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count) + (jt_b_unit_arbitrary_countenum))) /\ (((exists fs_h_jt_unit_arbitrary_countenumfirstscale. fs_h_jt_unit_arbitrary_countenumfirstscale + S (jt_c_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumfirstscale. jt_scales_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumfirstscale * S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count) + (jt_c_unit_arbitrary_countenum))))) -> (((((exists fs_h_jt_unit_arbitrary_countenumsecondcode. fs_h_jt_unit_arbitrary_countenumsecondcode + S (jt_d_unit_arbitrary_countenum) = S ((S (jt_h_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumsecondcode. jt_codes_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumsecondcode * S ((S (jt_h_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count) + (jt_d_unit_arbitrary_countenum))) /\ (((exists fs_h_jt_unit_arbitrary_countenumsecondscale. fs_h_jt_unit_arbitrary_countenumsecondscale + S (jt_e_unit_arbitrary_countenum) = S ((S (jt_h_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumsecondscale. jt_scales_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumsecondscale * S ((S (jt_h_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count) + (jt_e_unit_arbitrary_countenum))))) -> (forall jt_index_unit_arbitrary_countenumsame jt_left_unit_arbitrary_countenumsame jt_right_unit_arbitrary_countenumsame. (exists jt_gap_unit_arbitrary_countenumsameindex. jt_gap_unit_arbitrary_countenumsameindex+S (jt_index_unit_arbitrary_countenumsame)=(k)) -> (((exists fs_h_jt_unit_arbitrary_countenumsameleft. fs_h_jt_unit_arbitrary_countenumsameleft + S (jt_left_unit_arbitrary_countenumsame) = S ((S (jt_index_unit_arbitrary_countenumsame)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumsameleft. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumsameleft * S ((S (jt_index_unit_arbitrary_countenumsame)) * jt_c_unit_arbitrary_countenum) + (jt_left_unit_arbitrary_countenumsame))) -> (((exists fs_h_jt_unit_arbitrary_countenumsameright. fs_h_jt_unit_arbitrary_countenumsameright + S (jt_right_unit_arbitrary_countenumsame) = S ((S (jt_index_unit_arbitrary_countenumsame)) * jt_e_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumsameright. jt_d_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumsameright * S ((S (jt_index_unit_arbitrary_countenumsame)) * jt_e_unit_arbitrary_countenum) + (jt_right_unit_arbitrary_countenumsame))) -> jt_left_unit_arbitrary_countenumsame=jt_right_unit_arbitrary_countenumsame) -> jt_i_unit_arbitrary_countenum=jt_h_unit_arbitrary_countenum))))))))) -> (j=1)

Complete tactic proof in conservative notation

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

15 script commands · 4 reading checkpoints · 1 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 (2)
jordan totient count uniquejordan totient at one
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 hCount
02Establish hPositiveL4–4

Establish this local claim before using it. It is not an additional assumption.

  1. L4
    have hPositive : ~(k=0)
03Separate the logical casesL5–5

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

  1. L5
    cases hCount
04Use earlier factsL6–15

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

  1. L6
    exact hCount_left
  2. L7
    specialize jordan_totient_count_unique (k)
  3. L8
    specialize jordan_totient_count_unique (1)
  4. L9
    specialize jordan_totient_count_unique (j)
  5. L10
    specialize jordan_totient_count_unique (1)
  6. L11
    apply jordan_totient_count_unique
  7. L12
    exact hCount
  8. L13
    specialize jordan_totient_at_one (k)
  9. L14
    apply jordan_totient_at_one
  10. L15
    exact hPositive

Library-wide reading audit

Original defined command ledger · 15 lines
  1. 0001intro k
  2. 0002intro j
  3. 0003intro hCount
  4. 0004have hPositive : ~(k=0)
  5. 0005cases hCount
  6. 0006exact hCount_left
  7. 0007specialize jordan_totient_count_unique (k)
  8. 0008specialize jordan_totient_count_unique (1)
  9. 0009specialize jordan_totient_count_unique (j)
  10. 0010specialize jordan_totient_count_unique (1)
  11. 0011apply jordan_totient_count_unique
  12. 0012exact hCount
  13. 0013specialize jordan_totient_at_one (k)
  14. 0014apply jordan_totient_at_one
  15. 0015exact hPositive