JT005B

jordan_totient_at_one

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

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

Exact expanded first-order arithmetic 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)))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 13 exact native proof lines.

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

Proof neighborhood

Direct dependencies

succ_ne_zero Alpha theorem; checked-use authorized JT005A jordan_unit_modulus_singleton_enumeration

Direct dependents

JT005C jordan_totient_at_one_unique

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

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.

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