JT0029

jordan_totient_exists

Obtain an actual finite tuple cardinality from independently constructed duplicate-free 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. ∀ n. ¬k = 0 → ¬n = 0 → ∃ x. JordanTotient(k,n,x)

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

Definition DAG

JordanTotient(k,n,j) · 1JordanTupleScan(k,n,c,limit,B,C,D,E,j) · 2JordanTupleRepresentatives(k,n,c,T) · 1

Actual proof prerequisites

jordan_tuple_representatives_existsjordan_tuple_scan_existsjordan_totient_from_complete_scan
Original expanded first-order statement 
forall k n. ~(k=0) -> ~(n=0) -> exists j. ((~((k)=0)) /\ (((~((n)=0)) /\ (exists jt_codes_jordanexists jt_code_scale_jordanexists jt_scales_jordanexists jt_scale_scale_jordanexists. ((forall jt_i_jordanexistsenum. (exists jt_gap_jordanexistsenumsoundindex. jt_gap_jordanexistsenumsoundindex+S (jt_i_jordanexistsenum)=(j)) -> exists jt_b_jordanexistsenum jt_c_jordanexistsenum. ((((((exists fs_h_jt_jordanexistsenumsoundcode. fs_h_jt_jordanexistsenumsoundcode + S (jt_b_jordanexistsenum) = S ((S (jt_i_jordanexistsenum)) * jt_code_scale_jordanexists)) /\ exists fs_q_jt_jordanexistsenumsoundcode. jt_codes_jordanexists = fs_q_jt_jordanexistsenumsoundcode * S ((S (jt_i_jordanexistsenum)) * jt_code_scale_jordanexists) + (jt_b_jordanexistsenum))) /\ (((exists fs_h_jt_jordanexistsenumsoundscale. fs_h_jt_jordanexistsenumsoundscale + S (jt_c_jordanexistsenum) = S ((S (jt_i_jordanexistsenum)) * jt_scale_scale_jordanexists)) /\ exists fs_q_jt_jordanexistsenumsoundscale. jt_scales_jordanexists = fs_q_jt_jordanexistsenumsoundscale * S ((S (jt_i_jordanexistsenum)) * jt_scale_scale_jordanexists) + (jt_c_jordanexistsenum))))) /\ (((forall jt_index_jordanexistsenumbound. (exists jt_gap_jordanexistsenumboundindex. jt_gap_jordanexistsenumboundindex+S (jt_index_jordanexistsenumbound)=(k)) -> exists jt_value_jordanexistsenumbound. ((((exists fs_h_jt_jordanexistsenumboundat. fs_h_jt_jordanexistsenumboundat + S (jt_value_jordanexistsenumbound) = S ((S (jt_index_jordanexistsenumbound)) * jt_c_jordanexistsenum)) /\ exists fs_q_jt_jordanexistsenumboundat. jt_b_jordanexistsenum = fs_q_jt_jordanexistsenumboundat * S ((S (jt_index_jordanexistsenumbound)) * jt_c_jordanexistsenum) + (jt_value_jordanexistsenumbound))) /\ (exists jt_gap_jordanexistsenumboundvalue. jt_gap_jordanexistsenumboundvalue+S (jt_value_jordanexistsenumbound)=(n)))) /\ (forall jt_divisor_jordanexistsenumprimitive. (exists jt_factor_jordanexistsenumprimitivemodulus. (n)=(jt_divisor_jordanexistsenumprimitive)*jt_factor_jordanexistsenumprimitivemodulus) -> (forall jt_index_jordanexistsenumprimitivecoordinates jt_value_jordanexistsenumprimitivecoordinates. (exists jt_gap_jordanexistsenumprimitivecoordinatesindex. jt_gap_jordanexistsenumprimitivecoordinatesindex+S (jt_index_jordanexistsenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jordanexistsenumprimitivecoordinatesat. fs_h_jt_jordanexistsenumprimitivecoordinatesat + S (jt_value_jordanexistsenumprimitivecoordinates) = S ((S (jt_index_jordanexistsenumprimitivecoordinates)) * jt_c_jordanexistsenum)) /\ exists fs_q_jt_jordanexistsenumprimitivecoordinatesat. jt_b_jordanexistsenum = fs_q_jt_jordanexistsenumprimitivecoordinatesat * S ((S (jt_index_jordanexistsenumprimitivecoordinates)) * jt_c_jordanexistsenum) + (jt_value_jordanexistsenumprimitivecoordinates))) -> (exists jt_factor_jordanexistsenumprimitivecoordinatesdivides. (jt_value_jordanexistsenumprimitivecoordinates)=(jt_divisor_jordanexistsenumprimitive)*jt_factor_jordanexistsenumprimitivecoordinatesdivides)) -> jt_divisor_jordanexistsenumprimitive=1))))) /\ (((forall jt_b_jordanexistsenum jt_c_jordanexistsenum. (forall jt_index_jordanexistsenuminputbound. (exists jt_gap_jordanexistsenuminputboundindex. jt_gap_jordanexistsenuminputboundindex+S (jt_index_jordanexistsenuminputbound)=(k)) -> exists jt_value_jordanexistsenuminputbound. ((((exists fs_h_jt_jordanexistsenuminputboundat. fs_h_jt_jordanexistsenuminputboundat + S (jt_value_jordanexistsenuminputbound) = S ((S (jt_index_jordanexistsenuminputbound)) * jt_c_jordanexistsenum)) /\ exists fs_q_jt_jordanexistsenuminputboundat. jt_b_jordanexistsenum = fs_q_jt_jordanexistsenuminputboundat * S ((S (jt_index_jordanexistsenuminputbound)) * jt_c_jordanexistsenum) + (jt_value_jordanexistsenuminputbound))) /\ (exists jt_gap_jordanexistsenuminputboundvalue. jt_gap_jordanexistsenuminputboundvalue+S (jt_value_jordanexistsenuminputbound)=(n)))) -> (forall jt_divisor_jordanexistsenuminputprimitive. (exists jt_factor_jordanexistsenuminputprimitivemodulus. (n)=(jt_divisor_jordanexistsenuminputprimitive)*jt_factor_jordanexistsenuminputprimitivemodulus) -> (forall jt_index_jordanexistsenuminputprimitivecoordinates jt_value_jordanexistsenuminputprimitivecoordinates. (exists jt_gap_jordanexistsenuminputprimitivecoordinatesindex. jt_gap_jordanexistsenuminputprimitivecoordinatesindex+S (jt_index_jordanexistsenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jordanexistsenuminputprimitivecoordinatesat. fs_h_jt_jordanexistsenuminputprimitivecoordinatesat + S (jt_value_jordanexistsenuminputprimitivecoordinates) = S ((S (jt_index_jordanexistsenuminputprimitivecoordinates)) * jt_c_jordanexistsenum)) /\ exists fs_q_jt_jordanexistsenuminputprimitivecoordinatesat. jt_b_jordanexistsenum = fs_q_jt_jordanexistsenuminputprimitivecoordinatesat * S ((S (jt_index_jordanexistsenuminputprimitivecoordinates)) * jt_c_jordanexistsenum) + (jt_value_jordanexistsenuminputprimitivecoordinates))) -> (exists jt_factor_jordanexistsenuminputprimitivecoordinatesdivides. (jt_value_jordanexistsenuminputprimitivecoordinates)=(jt_divisor_jordanexistsenuminputprimitive)*jt_factor_jordanexistsenuminputprimitivecoordinatesdivides)) -> jt_divisor_jordanexistsenuminputprimitive=1) -> exists jt_i_jordanexistsenum jt_d_jordanexistsenum jt_e_jordanexistsenum. ((exists jt_gap_jordanexistsenumcompleteindex. jt_gap_jordanexistsenumcompleteindex+S (jt_i_jordanexistsenum)=(j)) /\ (((((((exists fs_h_jt_jordanexistsenumcompletecode. fs_h_jt_jordanexistsenumcompletecode + S (jt_d_jordanexistsenum) = S ((S (jt_i_jordanexistsenum)) * jt_code_scale_jordanexists)) /\ exists fs_q_jt_jordanexistsenumcompletecode. jt_codes_jordanexists = fs_q_jt_jordanexistsenumcompletecode * S ((S (jt_i_jordanexistsenum)) * jt_code_scale_jordanexists) + (jt_d_jordanexistsenum))) /\ (((exists fs_h_jt_jordanexistsenumcompletescale. fs_h_jt_jordanexistsenumcompletescale + S (jt_e_jordanexistsenum) = S ((S (jt_i_jordanexistsenum)) * jt_scale_scale_jordanexists)) /\ exists fs_q_jt_jordanexistsenumcompletescale. jt_scales_jordanexists = fs_q_jt_jordanexistsenumcompletescale * S ((S (jt_i_jordanexistsenum)) * jt_scale_scale_jordanexists) + (jt_e_jordanexistsenum))))) /\ (forall jt_index_jordanexistsenumrepresented jt_left_jordanexistsenumrepresented jt_right_jordanexistsenumrepresented. (exists jt_gap_jordanexistsenumrepresentedindex. jt_gap_jordanexistsenumrepresentedindex+S (jt_index_jordanexistsenumrepresented)=(k)) -> (((exists fs_h_jt_jordanexistsenumrepresentedleft. fs_h_jt_jordanexistsenumrepresentedleft + S (jt_left_jordanexistsenumrepresented) = S ((S (jt_index_jordanexistsenumrepresented)) * jt_c_jordanexistsenum)) /\ exists fs_q_jt_jordanexistsenumrepresentedleft. jt_b_jordanexistsenum = fs_q_jt_jordanexistsenumrepresentedleft * S ((S (jt_index_jordanexistsenumrepresented)) * jt_c_jordanexistsenum) + (jt_left_jordanexistsenumrepresented))) -> (((exists fs_h_jt_jordanexistsenumrepresentedright. fs_h_jt_jordanexistsenumrepresentedright + S (jt_right_jordanexistsenumrepresented) = S ((S (jt_index_jordanexistsenumrepresented)) * jt_e_jordanexistsenum)) /\ exists fs_q_jt_jordanexistsenumrepresentedright. jt_d_jordanexistsenum = fs_q_jt_jordanexistsenumrepresentedright * S ((S (jt_index_jordanexistsenumrepresented)) * jt_e_jordanexistsenum) + (jt_right_jordanexistsenumrepresented))) -> jt_left_jordanexistsenumrepresented=jt_right_jordanexistsenumrepresented))))) /\ (forall jt_i_jordanexistsenum jt_h_jordanexistsenum jt_b_jordanexistsenum jt_c_jordanexistsenum jt_d_jordanexistsenum jt_e_jordanexistsenum. (exists jt_gap_jordanexistsenumfirstindex. jt_gap_jordanexistsenumfirstindex+S (jt_i_jordanexistsenum)=(j)) -> (exists jt_gap_jordanexistsenumsecondindex. jt_gap_jordanexistsenumsecondindex+S (jt_h_jordanexistsenum)=(j)) -> (((((exists fs_h_jt_jordanexistsenumfirstcode. fs_h_jt_jordanexistsenumfirstcode + S (jt_b_jordanexistsenum) = S ((S (jt_i_jordanexistsenum)) * jt_code_scale_jordanexists)) /\ exists fs_q_jt_jordanexistsenumfirstcode. jt_codes_jordanexists = fs_q_jt_jordanexistsenumfirstcode * S ((S (jt_i_jordanexistsenum)) * jt_code_scale_jordanexists) + (jt_b_jordanexistsenum))) /\ (((exists fs_h_jt_jordanexistsenumfirstscale. fs_h_jt_jordanexistsenumfirstscale + S (jt_c_jordanexistsenum) = S ((S (jt_i_jordanexistsenum)) * jt_scale_scale_jordanexists)) /\ exists fs_q_jt_jordanexistsenumfirstscale. jt_scales_jordanexists = fs_q_jt_jordanexistsenumfirstscale * S ((S (jt_i_jordanexistsenum)) * jt_scale_scale_jordanexists) + (jt_c_jordanexistsenum))))) -> (((((exists fs_h_jt_jordanexistsenumsecondcode. fs_h_jt_jordanexistsenumsecondcode + S (jt_d_jordanexistsenum) = S ((S (jt_h_jordanexistsenum)) * jt_code_scale_jordanexists)) /\ exists fs_q_jt_jordanexistsenumsecondcode. jt_codes_jordanexists = fs_q_jt_jordanexistsenumsecondcode * S ((S (jt_h_jordanexistsenum)) * jt_code_scale_jordanexists) + (jt_d_jordanexistsenum))) /\ (((exists fs_h_jt_jordanexistsenumsecondscale. fs_h_jt_jordanexistsenumsecondscale + S (jt_e_jordanexistsenum) = S ((S (jt_h_jordanexistsenum)) * jt_scale_scale_jordanexists)) /\ exists fs_q_jt_jordanexistsenumsecondscale. jt_scales_jordanexists = fs_q_jt_jordanexistsenumsecondscale * S ((S (jt_h_jordanexistsenum)) * jt_scale_scale_jordanexists) + (jt_e_jordanexistsenum))))) -> (forall jt_index_jordanexistsenumsame jt_left_jordanexistsenumsame jt_right_jordanexistsenumsame. (exists jt_gap_jordanexistsenumsameindex. jt_gap_jordanexistsenumsameindex+S (jt_index_jordanexistsenumsame)=(k)) -> (((exists fs_h_jt_jordanexistsenumsameleft. fs_h_jt_jordanexistsenumsameleft + S (jt_left_jordanexistsenumsame) = S ((S (jt_index_jordanexistsenumsame)) * jt_c_jordanexistsenum)) /\ exists fs_q_jt_jordanexistsenumsameleft. jt_b_jordanexistsenum = fs_q_jt_jordanexistsenumsameleft * S ((S (jt_index_jordanexistsenumsame)) * jt_c_jordanexistsenum) + (jt_left_jordanexistsenumsame))) -> (((exists fs_h_jt_jordanexistsenumsameright. fs_h_jt_jordanexistsenumsameright + S (jt_right_jordanexistsenumsame) = S ((S (jt_index_jordanexistsenumsame)) * jt_e_jordanexistsenum)) /\ exists fs_q_jt_jordanexistsenumsameright. jt_d_jordanexistsenum = fs_q_jt_jordanexistsenumsameright * S ((S (jt_index_jordanexistsenumsame)) * jt_e_jordanexistsenum) + (jt_right_jordanexistsenumsame))) -> jt_left_jordanexistsenumsame=jt_right_jordanexistsenumsame) -> jt_i_jordanexistsenum=jt_h_jordanexistsenum))))))))

Complete tactic proof in conservative notation

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

39 script commands · 9 reading checkpoints · 3 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 (3)
jordan tuple representatives existsjordan tuple scan existsjordan totient from complete scan
01Fix variables and assumptionsL1–4

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

  1. L1
    intro k
  2. L2
    intro n
  3. L3
    intro hk
  4. L4
    intro hn
02Establish hboxL5–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple representatives exists.

  1. L5
    have hbox : ∃ c. ∃ T. JordanTupleRepresentatives(k,n,c,T)Definitions: JordanTupleRepresentatives(k,n,c,T)Original native command in the exact edition
  2. L6
    specialize jordan_tuple_representatives_exists (k)
  3. L7
    specialize jordan_tuple_representatives_exists (n)
  4. L8
    apply jordan_tuple_representatives_exists
03Separate the logical casesL9–10

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

  1. L9
    cases hbox
  2. L10
    cases hbox_witness
04Establish hfamilyL11–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply jordan tuple scan exists.

  1. L11
    have hfamily : ∀ t. ∃ B. ∃ C. ∃ D. ∃ E. ∃ j. JordanTupleScan(k,n,x,t,B,C,D,E,j)Definitions: JordanTupleScan(k,n,x,t,B,C,D,E,j)Original native command in the exact edition
  2. L12
    specialize jordan_tuple_scan_exists (k)
  3. L13
    specialize jordan_tuple_scan_exists (n)
  4. L14
    specialize jordan_tuple_scan_exists (x)
  5. L15
    apply jordan_tuple_scan_exists
  6. L16
    exact hn
05Establish hsL17–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hfamily.

  1. L17
    have hs : ∃ B. ∃ C. ∃ D. ∃ E. ∃ j. JordanTupleScan(k,n,x,x1,B,C,D,E,j)Definitions: JordanTupleScan(k,n,x,x1,B,C,D,E,j)Original native command in the exact edition
  2. L18
    specialize hfamily (x1)
  3. L19
    apply hfamily
06Separate the logical casesL20–24

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

  1. L20
    cases hs
  2. L21
    cases hs_witness
  3. L22
    cases hs_witness_witness
  4. L23
    cases hs_witness_witness_witness
  5. L24
    cases hs_witness_witness_witness_witness
07Construct an explicit witnessL25–25

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

  1. L25
    exists x6
08Use earlier factsL26–35

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

  1. L26
    specialize jordan_totient_from_complete_scan (k)
  2. L27
    specialize jordan_totient_from_complete_scan (n)
  3. L28
    specialize jordan_totient_from_complete_scan (x)
  4. L29
    specialize jordan_totient_from_complete_scan (x1)
  5. L30
    specialize jordan_totient_from_complete_scan (x2)
  6. L31
    specialize jordan_totient_from_complete_scan (x3)
  7. L32
    specialize jordan_totient_from_complete_scan (x4)
  8. L33
    specialize jordan_totient_from_complete_scan (x5)
  9. L34
    specialize jordan_totient_from_complete_scan (x6)
  10. L35
    apply jordan_totient_from_complete_scan
09Use earlier factsL36–39

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

  1. L36
    exact hk
  2. L37
    exact hn
  3. L38
    exact hbox_witness_witness
  4. L39
    exact hs_witness_witness_witness_witness_witness

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003intro hk
  4. 0004intro hn
  5. 0005have hbox : ∃ c. ∃ T. JordanTupleRepresentatives(k,n,c,T)
  6. 0006specialize jordan_tuple_representatives_exists (k)
  7. 0007specialize jordan_tuple_representatives_exists (n)
  8. 0008apply jordan_tuple_representatives_exists
  9. 0009cases hbox
  10. 0010cases hbox_witness
  11. 0011have hfamily : ∀ t. ∃ B. ∃ C. ∃ D. ∃ E. ∃ j. JordanTupleScan(k,n,x,t,B,C,D,E,j)
  12. 0012specialize jordan_tuple_scan_exists (k)
  13. 0013specialize jordan_tuple_scan_exists (n)
  14. 0014specialize jordan_tuple_scan_exists (x)
  15. 0015apply jordan_tuple_scan_exists
  16. 0016exact hn
  17. 0017have hs : ∃ B. ∃ C. ∃ D. ∃ E. ∃ j. JordanTupleScan(k,n,x,x1,B,C,D,E,j)
  18. 0018specialize hfamily (x1)
  19. 0019apply hfamily
  20. 0020cases hs
  21. 0021cases hs_witness
  22. 0022cases hs_witness_witness
  23. 0023cases hs_witness_witness_witness
  24. 0024cases hs_witness_witness_witness_witness
  25. 0025exists x6
  26. 0026specialize jordan_totient_from_complete_scan (k)
  27. 0027specialize jordan_totient_from_complete_scan (n)
  28. 0028specialize jordan_totient_from_complete_scan (x)
  29. 0029specialize jordan_totient_from_complete_scan (x1)
  30. 0030specialize jordan_totient_from_complete_scan (x2)
  31. 0031specialize jordan_totient_from_complete_scan (x3)
  32. 0032specialize jordan_totient_from_complete_scan (x4)
  33. 0033specialize jordan_totient_from_complete_scan (x5)
  34. 0034specialize jordan_totient_from_complete_scan (x6)
  35. 0035apply jordan_totient_from_complete_scan
  36. 0036exact hk
  37. 0037exact hn
  38. 0038exact hbox_witness_witness
  39. 0039exact hs_witness_witness_witness_witness_witness