JT0029

jordan_totient_exists

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

Obtain an actual finite tuple cardinality from independently constructed duplicate-free enumeration.

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

Constructive proof overview

Generated structural guide

Obtain an actual finite tuple cardinality from independently constructed duplicate-free enumeration.

The unchanged tactic script uses 3 declared prerequisites and contains 39 exact native proof lines.

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

Proof neighborhood

Direct dependencies

JT0028 jordan_tuple_representatives_exists JT0027 jordan_tuple_scan_exists JT0025 jordan_totient_from_complete_scan

Direct dependents

JT004B jordan_totient_multiplicativity_exists

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

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.

Named ingredients (3)
jordan tuple representatives existsjordan tuple scan existsjordan totient from complete scan

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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
  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
  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 exact command ledger · 39 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003intro hk
  4. 0004intro hn
  5. 0005have hbox : exists c T. forall jt_code_totalbox jt_scale_totalbox. (forall jt_index_totalboxbound. (exists jt_gap_totalboxboundindex. jt_gap_totalboxboundindex+S (jt_index_totalboxbound)=(k)) -> exists jt_value_totalboxbound. ((((exists fs_h_jt_totalboxboundat. fs_h_jt_totalboxboundat + S (jt_value_totalboxbound) = S ((S (jt_index_totalboxbound)) * jt_scale_totalbox)) /\ exists fs_q_jt_totalboxboundat. jt_code_totalbox = fs_q_jt_totalboxboundat * S ((S (jt_index_totalboxbound)) * jt_scale_totalbox) + (jt_value_totalboxbound))) /\ (exists jt_gap_totalboxboundvalue. jt_gap_totalboxboundvalue+S (jt_value_totalboxbound)=(n)))) -> exists jt_representative_totalbox. ((exists jt_gap_totalboxindex. jt_gap_totalboxindex+S (jt_representative_totalbox)=(T)) /\ (forall jt_index_totalboxequal jt_left_totalboxequal jt_right_totalboxequal. (exists jt_gap_totalboxequalindex. jt_gap_totalboxequalindex+S (jt_index_totalboxequal)=(k)) -> (((exists fs_h_jt_totalboxequalleft. fs_h_jt_totalboxequalleft + S (jt_left_totalboxequal) = S ((S (jt_index_totalboxequal)) * jt_scale_totalbox)) /\ exists fs_q_jt_totalboxequalleft. jt_code_totalbox = fs_q_jt_totalboxequalleft * S ((S (jt_index_totalboxequal)) * jt_scale_totalbox) + (jt_left_totalboxequal))) -> (((exists fs_h_jt_totalboxequalright. fs_h_jt_totalboxequalright + S (jt_right_totalboxequal) = S ((S (jt_index_totalboxequal)) * c)) /\ exists fs_q_jt_totalboxequalright. jt_representative_totalbox = fs_q_jt_totalboxequalright * S ((S (jt_index_totalboxequal)) * c) + (jt_right_totalboxequal))) -> jt_left_totalboxequal=jt_right_totalboxequal))
  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 : forall t. exists B C D E j. ((forall jt_i_totalfamily. (exists jt_gap_totalfamilysoundindex. jt_gap_totalfamilysoundindex+S (jt_i_totalfamily)=(j)) -> exists jt_b_totalfamily jt_e_totalfamily. ((((((exists fs_h_jt_totalfamilysoundcode. fs_h_jt_totalfamilysoundcode + S (jt_b_totalfamily) = S ((S (jt_i_totalfamily)) * C)) /\ exists fs_q_jt_totalfamilysoundcode. B = fs_q_jt_totalfamilysoundcode * S ((S (jt_i_totalfamily)) * C) + (jt_b_totalfamily))) /\ (((exists fs_h_jt_totalfamilysoundscale. fs_h_jt_totalfamilysoundscale + S (jt_e_totalfamily) = S ((S (jt_i_totalfamily)) * E)) /\ exists fs_q_jt_totalfamilysoundscale. D = fs_q_jt_totalfamilysoundscale * S ((S (jt_i_totalfamily)) * E) + (jt_e_totalfamily))))) /\ (((forall jt_index_totalfamilybound. (exists jt_gap_totalfamilyboundindex. jt_gap_totalfamilyboundindex+S (jt_index_totalfamilybound)=(k)) -> exists jt_value_totalfamilybound. ((((exists fs_h_jt_totalfamilyboundat. fs_h_jt_totalfamilyboundat + S (jt_value_totalfamilybound) = S ((S (jt_index_totalfamilybound)) * jt_e_totalfamily)) /\ exists fs_q_jt_totalfamilyboundat. jt_b_totalfamily = fs_q_jt_totalfamilyboundat * S ((S (jt_index_totalfamilybound)) * jt_e_totalfamily) + (jt_value_totalfamilybound))) /\ (exists jt_gap_totalfamilyboundvalue. jt_gap_totalfamilyboundvalue+S (jt_value_totalfamilybound)=(n)))) /\ (forall jt_divisor_totalfamilyprimitive. (exists jt_factor_totalfamilyprimitivemodulus. (n)=(jt_divisor_totalfamilyprimitive)*jt_factor_totalfamilyprimitivemodulus) -> (forall jt_index_totalfamilyprimitivecoordinates jt_value_totalfamilyprimitivecoordinates. (exists jt_gap_totalfamilyprimitivecoordinatesindex. jt_gap_totalfamilyprimitivecoordinatesindex+S (jt_index_totalfamilyprimitivecoordinates)=(k)) -> (((exists fs_h_jt_totalfamilyprimitivecoordinatesat. fs_h_jt_totalfamilyprimitivecoordinatesat + S (jt_value_totalfamilyprimitivecoordinates) = S ((S (jt_index_totalfamilyprimitivecoordinates)) * jt_e_totalfamily)) /\ exists fs_q_jt_totalfamilyprimitivecoordinatesat. jt_b_totalfamily = fs_q_jt_totalfamilyprimitivecoordinatesat * S ((S (jt_index_totalfamilyprimitivecoordinates)) * jt_e_totalfamily) + (jt_value_totalfamilyprimitivecoordinates))) -> (exists jt_factor_totalfamilyprimitivecoordinatesdivides. (jt_value_totalfamilyprimitivecoordinates)=(jt_divisor_totalfamilyprimitive)*jt_factor_totalfamilyprimitivecoordinatesdivides)) -> jt_divisor_totalfamilyprimitive=1))))) /\ (((forall jt_i_totalfamily jt_h_totalfamily jt_b_totalfamily jt_e_totalfamily jt_d_totalfamily jt_f_totalfamily. (exists jt_gap_totalfamilyfirstindex. jt_gap_totalfamilyfirstindex+S (jt_i_totalfamily)=(j)) -> (exists jt_gap_totalfamilysecondindex. jt_gap_totalfamilysecondindex+S (jt_h_totalfamily)=(j)) -> (((((exists fs_h_jt_totalfamilyfirstcode. fs_h_jt_totalfamilyfirstcode + S (jt_b_totalfamily) = S ((S (jt_i_totalfamily)) * C)) /\ exists fs_q_jt_totalfamilyfirstcode. B = fs_q_jt_totalfamilyfirstcode * S ((S (jt_i_totalfamily)) * C) + (jt_b_totalfamily))) /\ (((exists fs_h_jt_totalfamilyfirstscale. fs_h_jt_totalfamilyfirstscale + S (jt_e_totalfamily) = S ((S (jt_i_totalfamily)) * E)) /\ exists fs_q_jt_totalfamilyfirstscale. D = fs_q_jt_totalfamilyfirstscale * S ((S (jt_i_totalfamily)) * E) + (jt_e_totalfamily))))) -> (((((exists fs_h_jt_totalfamilysecondcode. fs_h_jt_totalfamilysecondcode + S (jt_d_totalfamily) = S ((S (jt_h_totalfamily)) * C)) /\ exists fs_q_jt_totalfamilysecondcode. B = fs_q_jt_totalfamilysecondcode * S ((S (jt_h_totalfamily)) * C) + (jt_d_totalfamily))) /\ (((exists fs_h_jt_totalfamilysecondscale. fs_h_jt_totalfamilysecondscale + S (jt_f_totalfamily) = S ((S (jt_h_totalfamily)) * E)) /\ exists fs_q_jt_totalfamilysecondscale. D = fs_q_jt_totalfamilysecondscale * S ((S (jt_h_totalfamily)) * E) + (jt_f_totalfamily))))) -> (forall jt_index_totalfamilysame jt_left_totalfamilysame jt_right_totalfamilysame. (exists jt_gap_totalfamilysameindex. jt_gap_totalfamilysameindex+S (jt_index_totalfamilysame)=(k)) -> (((exists fs_h_jt_totalfamilysameleft. fs_h_jt_totalfamilysameleft + S (jt_left_totalfamilysame) = S ((S (jt_index_totalfamilysame)) * jt_e_totalfamily)) /\ exists fs_q_jt_totalfamilysameleft. jt_b_totalfamily = fs_q_jt_totalfamilysameleft * S ((S (jt_index_totalfamilysame)) * jt_e_totalfamily) + (jt_left_totalfamilysame))) -> (((exists fs_h_jt_totalfamilysameright. fs_h_jt_totalfamilysameright + S (jt_right_totalfamilysame) = S ((S (jt_index_totalfamilysame)) * jt_f_totalfamily)) /\ exists fs_q_jt_totalfamilysameright. jt_d_totalfamily = fs_q_jt_totalfamilysameright * S ((S (jt_index_totalfamilysame)) * jt_f_totalfamily) + (jt_right_totalfamilysame))) -> jt_left_totalfamilysame=jt_right_totalfamilysame) -> jt_i_totalfamily=jt_h_totalfamily) /\ (forall jt_z_totalfamily. (exists jt_gap_totalfamilycodeindex. jt_gap_totalfamilycodeindex+S (jt_z_totalfamily)=(t)) -> (forall jt_index_totalfamilyinputbound. (exists jt_gap_totalfamilyinputboundindex. jt_gap_totalfamilyinputboundindex+S (jt_index_totalfamilyinputbound)=(k)) -> exists jt_value_totalfamilyinputbound. ((((exists fs_h_jt_totalfamilyinputboundat. fs_h_jt_totalfamilyinputboundat + S (jt_value_totalfamilyinputbound) = S ((S (jt_index_totalfamilyinputbound)) * x)) /\ exists fs_q_jt_totalfamilyinputboundat. jt_z_totalfamily = fs_q_jt_totalfamilyinputboundat * S ((S (jt_index_totalfamilyinputbound)) * x) + (jt_value_totalfamilyinputbound))) /\ (exists jt_gap_totalfamilyinputboundvalue. jt_gap_totalfamilyinputboundvalue+S (jt_value_totalfamilyinputbound)=(n)))) -> (forall jt_divisor_totalfamilyinputprimitive. (exists jt_factor_totalfamilyinputprimitivemodulus. (n)=(jt_divisor_totalfamilyinputprimitive)*jt_factor_totalfamilyinputprimitivemodulus) -> (forall jt_index_totalfamilyinputprimitivecoordinates jt_value_totalfamilyinputprimitivecoordinates. (exists jt_gap_totalfamilyinputprimitivecoordinatesindex. jt_gap_totalfamilyinputprimitivecoordinatesindex+S (jt_index_totalfamilyinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_totalfamilyinputprimitivecoordinatesat. fs_h_jt_totalfamilyinputprimitivecoordinatesat + S (jt_value_totalfamilyinputprimitivecoordinates) = S ((S (jt_index_totalfamilyinputprimitivecoordinates)) * x)) /\ exists fs_q_jt_totalfamilyinputprimitivecoordinatesat. jt_z_totalfamily = fs_q_jt_totalfamilyinputprimitivecoordinatesat * S ((S (jt_index_totalfamilyinputprimitivecoordinates)) * x) + (jt_value_totalfamilyinputprimitivecoordinates))) -> (exists jt_factor_totalfamilyinputprimitivecoordinatesdivides. (jt_value_totalfamilyinputprimitivecoordinates)=(jt_divisor_totalfamilyinputprimitive)*jt_factor_totalfamilyinputprimitivecoordinatesdivides)) -> jt_divisor_totalfamilyinputprimitive=1) -> (exists jt_index_totalfamilylisted jt_code_totalfamilylisted jt_scale_totalfamilylisted. ((exists jt_gap_totalfamilylistedindex. jt_gap_totalfamilylistedindex+S (jt_index_totalfamilylisted)=(j)) /\ (((((((exists fs_h_jt_totalfamilylistedcode. fs_h_jt_totalfamilylistedcode + S (jt_code_totalfamilylisted) = S ((S (jt_index_totalfamilylisted)) * C)) /\ exists fs_q_jt_totalfamilylistedcode. B = fs_q_jt_totalfamilylistedcode * S ((S (jt_index_totalfamilylisted)) * C) + (jt_code_totalfamilylisted))) /\ (((exists fs_h_jt_totalfamilylistedscale. fs_h_jt_totalfamilylistedscale + S (jt_scale_totalfamilylisted) = S ((S (jt_index_totalfamilylisted)) * E)) /\ exists fs_q_jt_totalfamilylistedscale. D = fs_q_jt_totalfamilylistedscale * S ((S (jt_index_totalfamilylisted)) * E) + (jt_scale_totalfamilylisted))))) /\ (forall jt_index_totalfamilylistedequal jt_left_totalfamilylistedequal jt_right_totalfamilylistedequal. (exists jt_gap_totalfamilylistedequalindex. jt_gap_totalfamilylistedequalindex+S (jt_index_totalfamilylistedequal)=(k)) -> (((exists fs_h_jt_totalfamilylistedequalleft. fs_h_jt_totalfamilylistedequalleft + S (jt_left_totalfamilylistedequal) = S ((S (jt_index_totalfamilylistedequal)) * x)) /\ exists fs_q_jt_totalfamilylistedequalleft. jt_z_totalfamily = fs_q_jt_totalfamilylistedequalleft * S ((S (jt_index_totalfamilylistedequal)) * x) + (jt_left_totalfamilylistedequal))) -> (((exists fs_h_jt_totalfamilylistedequalright. fs_h_jt_totalfamilylistedequalright + S (jt_right_totalfamilylistedequal) = S ((S (jt_index_totalfamilylistedequal)) * jt_scale_totalfamilylisted)) /\ exists fs_q_jt_totalfamilylistedequalright. jt_code_totalfamilylisted = fs_q_jt_totalfamilylistedequalright * S ((S (jt_index_totalfamilylistedequal)) * jt_scale_totalfamilylisted) + (jt_right_totalfamilylistedequal))) -> jt_left_totalfamilylistedequal=jt_right_totalfamilylistedequal)))))))))
  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 : exists B C D E j. ((forall jt_i_totalscan. (exists jt_gap_totalscansoundindex. jt_gap_totalscansoundindex+S (jt_i_totalscan)=(j)) -> exists jt_b_totalscan jt_e_totalscan. ((((((exists fs_h_jt_totalscansoundcode. fs_h_jt_totalscansoundcode + S (jt_b_totalscan) = S ((S (jt_i_totalscan)) * C)) /\ exists fs_q_jt_totalscansoundcode. B = fs_q_jt_totalscansoundcode * S ((S (jt_i_totalscan)) * C) + (jt_b_totalscan))) /\ (((exists fs_h_jt_totalscansoundscale. fs_h_jt_totalscansoundscale + S (jt_e_totalscan) = S ((S (jt_i_totalscan)) * E)) /\ exists fs_q_jt_totalscansoundscale. D = fs_q_jt_totalscansoundscale * S ((S (jt_i_totalscan)) * E) + (jt_e_totalscan))))) /\ (((forall jt_index_totalscanbound. (exists jt_gap_totalscanboundindex. jt_gap_totalscanboundindex+S (jt_index_totalscanbound)=(k)) -> exists jt_value_totalscanbound. ((((exists fs_h_jt_totalscanboundat. fs_h_jt_totalscanboundat + S (jt_value_totalscanbound) = S ((S (jt_index_totalscanbound)) * jt_e_totalscan)) /\ exists fs_q_jt_totalscanboundat. jt_b_totalscan = fs_q_jt_totalscanboundat * S ((S (jt_index_totalscanbound)) * jt_e_totalscan) + (jt_value_totalscanbound))) /\ (exists jt_gap_totalscanboundvalue. jt_gap_totalscanboundvalue+S (jt_value_totalscanbound)=(n)))) /\ (forall jt_divisor_totalscanprimitive. (exists jt_factor_totalscanprimitivemodulus. (n)=(jt_divisor_totalscanprimitive)*jt_factor_totalscanprimitivemodulus) -> (forall jt_index_totalscanprimitivecoordinates jt_value_totalscanprimitivecoordinates. (exists jt_gap_totalscanprimitivecoordinatesindex. jt_gap_totalscanprimitivecoordinatesindex+S (jt_index_totalscanprimitivecoordinates)=(k)) -> (((exists fs_h_jt_totalscanprimitivecoordinatesat. fs_h_jt_totalscanprimitivecoordinatesat + S (jt_value_totalscanprimitivecoordinates) = S ((S (jt_index_totalscanprimitivecoordinates)) * jt_e_totalscan)) /\ exists fs_q_jt_totalscanprimitivecoordinatesat. jt_b_totalscan = fs_q_jt_totalscanprimitivecoordinatesat * S ((S (jt_index_totalscanprimitivecoordinates)) * jt_e_totalscan) + (jt_value_totalscanprimitivecoordinates))) -> (exists jt_factor_totalscanprimitivecoordinatesdivides. (jt_value_totalscanprimitivecoordinates)=(jt_divisor_totalscanprimitive)*jt_factor_totalscanprimitivecoordinatesdivides)) -> jt_divisor_totalscanprimitive=1))))) /\ (((forall jt_i_totalscan jt_h_totalscan jt_b_totalscan jt_e_totalscan jt_d_totalscan jt_f_totalscan. (exists jt_gap_totalscanfirstindex. jt_gap_totalscanfirstindex+S (jt_i_totalscan)=(j)) -> (exists jt_gap_totalscansecondindex. jt_gap_totalscansecondindex+S (jt_h_totalscan)=(j)) -> (((((exists fs_h_jt_totalscanfirstcode. fs_h_jt_totalscanfirstcode + S (jt_b_totalscan) = S ((S (jt_i_totalscan)) * C)) /\ exists fs_q_jt_totalscanfirstcode. B = fs_q_jt_totalscanfirstcode * S ((S (jt_i_totalscan)) * C) + (jt_b_totalscan))) /\ (((exists fs_h_jt_totalscanfirstscale. fs_h_jt_totalscanfirstscale + S (jt_e_totalscan) = S ((S (jt_i_totalscan)) * E)) /\ exists fs_q_jt_totalscanfirstscale. D = fs_q_jt_totalscanfirstscale * S ((S (jt_i_totalscan)) * E) + (jt_e_totalscan))))) -> (((((exists fs_h_jt_totalscansecondcode. fs_h_jt_totalscansecondcode + S (jt_d_totalscan) = S ((S (jt_h_totalscan)) * C)) /\ exists fs_q_jt_totalscansecondcode. B = fs_q_jt_totalscansecondcode * S ((S (jt_h_totalscan)) * C) + (jt_d_totalscan))) /\ (((exists fs_h_jt_totalscansecondscale. fs_h_jt_totalscansecondscale + S (jt_f_totalscan) = S ((S (jt_h_totalscan)) * E)) /\ exists fs_q_jt_totalscansecondscale. D = fs_q_jt_totalscansecondscale * S ((S (jt_h_totalscan)) * E) + (jt_f_totalscan))))) -> (forall jt_index_totalscansame jt_left_totalscansame jt_right_totalscansame. (exists jt_gap_totalscansameindex. jt_gap_totalscansameindex+S (jt_index_totalscansame)=(k)) -> (((exists fs_h_jt_totalscansameleft. fs_h_jt_totalscansameleft + S (jt_left_totalscansame) = S ((S (jt_index_totalscansame)) * jt_e_totalscan)) /\ exists fs_q_jt_totalscansameleft. jt_b_totalscan = fs_q_jt_totalscansameleft * S ((S (jt_index_totalscansame)) * jt_e_totalscan) + (jt_left_totalscansame))) -> (((exists fs_h_jt_totalscansameright. fs_h_jt_totalscansameright + S (jt_right_totalscansame) = S ((S (jt_index_totalscansame)) * jt_f_totalscan)) /\ exists fs_q_jt_totalscansameright. jt_d_totalscan = fs_q_jt_totalscansameright * S ((S (jt_index_totalscansame)) * jt_f_totalscan) + (jt_right_totalscansame))) -> jt_left_totalscansame=jt_right_totalscansame) -> jt_i_totalscan=jt_h_totalscan) /\ (forall jt_z_totalscan. (exists jt_gap_totalscancodeindex. jt_gap_totalscancodeindex+S (jt_z_totalscan)=(x1)) -> (forall jt_index_totalscaninputbound. (exists jt_gap_totalscaninputboundindex. jt_gap_totalscaninputboundindex+S (jt_index_totalscaninputbound)=(k)) -> exists jt_value_totalscaninputbound. ((((exists fs_h_jt_totalscaninputboundat. fs_h_jt_totalscaninputboundat + S (jt_value_totalscaninputbound) = S ((S (jt_index_totalscaninputbound)) * x)) /\ exists fs_q_jt_totalscaninputboundat. jt_z_totalscan = fs_q_jt_totalscaninputboundat * S ((S (jt_index_totalscaninputbound)) * x) + (jt_value_totalscaninputbound))) /\ (exists jt_gap_totalscaninputboundvalue. jt_gap_totalscaninputboundvalue+S (jt_value_totalscaninputbound)=(n)))) -> (forall jt_divisor_totalscaninputprimitive. (exists jt_factor_totalscaninputprimitivemodulus. (n)=(jt_divisor_totalscaninputprimitive)*jt_factor_totalscaninputprimitivemodulus) -> (forall jt_index_totalscaninputprimitivecoordinates jt_value_totalscaninputprimitivecoordinates. (exists jt_gap_totalscaninputprimitivecoordinatesindex. jt_gap_totalscaninputprimitivecoordinatesindex+S (jt_index_totalscaninputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_totalscaninputprimitivecoordinatesat. fs_h_jt_totalscaninputprimitivecoordinatesat + S (jt_value_totalscaninputprimitivecoordinates) = S ((S (jt_index_totalscaninputprimitivecoordinates)) * x)) /\ exists fs_q_jt_totalscaninputprimitivecoordinatesat. jt_z_totalscan = fs_q_jt_totalscaninputprimitivecoordinatesat * S ((S (jt_index_totalscaninputprimitivecoordinates)) * x) + (jt_value_totalscaninputprimitivecoordinates))) -> (exists jt_factor_totalscaninputprimitivecoordinatesdivides. (jt_value_totalscaninputprimitivecoordinates)=(jt_divisor_totalscaninputprimitive)*jt_factor_totalscaninputprimitivecoordinatesdivides)) -> jt_divisor_totalscaninputprimitive=1) -> (exists jt_index_totalscanlisted jt_code_totalscanlisted jt_scale_totalscanlisted. ((exists jt_gap_totalscanlistedindex. jt_gap_totalscanlistedindex+S (jt_index_totalscanlisted)=(j)) /\ (((((((exists fs_h_jt_totalscanlistedcode. fs_h_jt_totalscanlistedcode + S (jt_code_totalscanlisted) = S ((S (jt_index_totalscanlisted)) * C)) /\ exists fs_q_jt_totalscanlistedcode. B = fs_q_jt_totalscanlistedcode * S ((S (jt_index_totalscanlisted)) * C) + (jt_code_totalscanlisted))) /\ (((exists fs_h_jt_totalscanlistedscale. fs_h_jt_totalscanlistedscale + S (jt_scale_totalscanlisted) = S ((S (jt_index_totalscanlisted)) * E)) /\ exists fs_q_jt_totalscanlistedscale. D = fs_q_jt_totalscanlistedscale * S ((S (jt_index_totalscanlisted)) * E) + (jt_scale_totalscanlisted))))) /\ (forall jt_index_totalscanlistedequal jt_left_totalscanlistedequal jt_right_totalscanlistedequal. (exists jt_gap_totalscanlistedequalindex. jt_gap_totalscanlistedequalindex+S (jt_index_totalscanlistedequal)=(k)) -> (((exists fs_h_jt_totalscanlistedequalleft. fs_h_jt_totalscanlistedequalleft + S (jt_left_totalscanlistedequal) = S ((S (jt_index_totalscanlistedequal)) * x)) /\ exists fs_q_jt_totalscanlistedequalleft. jt_z_totalscan = fs_q_jt_totalscanlistedequalleft * S ((S (jt_index_totalscanlistedequal)) * x) + (jt_left_totalscanlistedequal))) -> (((exists fs_h_jt_totalscanlistedequalright. fs_h_jt_totalscanlistedequalright + S (jt_right_totalscanlistedequal) = S ((S (jt_index_totalscanlistedequal)) * jt_scale_totalscanlisted)) /\ exists fs_q_jt_totalscanlistedequalright. jt_code_totalscanlisted = fs_q_jt_totalscanlistedequalright * S ((S (jt_index_totalscanlistedequal)) * jt_scale_totalscanlisted) + (jt_right_totalscanlistedequal))) -> jt_left_totalscanlistedequal=jt_right_totalscanlistedequal)))))))))
  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