JT0009

jordan_order_zero_excluded

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

Jordan is intentionally restricted to positive tuple order.

Exact expanded first-order arithmetic statement

forall n j. ~(((~((0)=0)) /\ (((~((n)=0)) /\ (exists jt_codes_zeroorder jt_code_scale_zeroorder jt_scales_zeroorder jt_scale_scale_zeroorder. ((forall jt_i_zeroorderenum. (exists jt_gap_zeroorderenumsoundindex. jt_gap_zeroorderenumsoundindex+S (jt_i_zeroorderenum)=(j)) -> exists jt_b_zeroorderenum jt_c_zeroorderenum. ((((((exists fs_h_jt_zeroorderenumsoundcode. fs_h_jt_zeroorderenumsoundcode + S (jt_b_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumsoundcode. jt_codes_zeroorder = fs_q_jt_zeroorderenumsoundcode * S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder) + (jt_b_zeroorderenum))) /\ (((exists fs_h_jt_zeroorderenumsoundscale. fs_h_jt_zeroorderenumsoundscale + S (jt_c_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumsoundscale. jt_scales_zeroorder = fs_q_jt_zeroorderenumsoundscale * S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder) + (jt_c_zeroorderenum))))) /\ (((forall jt_index_zeroorderenumbound. (exists jt_gap_zeroorderenumboundindex. jt_gap_zeroorderenumboundindex+S (jt_index_zeroorderenumbound)=(0)) -> exists jt_value_zeroorderenumbound. ((((exists fs_h_jt_zeroorderenumboundat. fs_h_jt_zeroorderenumboundat + S (jt_value_zeroorderenumbound) = S ((S (jt_index_zeroorderenumbound)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumboundat. jt_b_zeroorderenum = fs_q_jt_zeroorderenumboundat * S ((S (jt_index_zeroorderenumbound)) * jt_c_zeroorderenum) + (jt_value_zeroorderenumbound))) /\ (exists jt_gap_zeroorderenumboundvalue. jt_gap_zeroorderenumboundvalue+S (jt_value_zeroorderenumbound)=(n)))) /\ (forall jt_divisor_zeroorderenumprimitive. (exists jt_factor_zeroorderenumprimitivemodulus. (n)=(jt_divisor_zeroorderenumprimitive)*jt_factor_zeroorderenumprimitivemodulus) -> (forall jt_index_zeroorderenumprimitivecoordinates jt_value_zeroorderenumprimitivecoordinates. (exists jt_gap_zeroorderenumprimitivecoordinatesindex. jt_gap_zeroorderenumprimitivecoordinatesindex+S (jt_index_zeroorderenumprimitivecoordinates)=(0)) -> (((exists fs_h_jt_zeroorderenumprimitivecoordinatesat. fs_h_jt_zeroorderenumprimitivecoordinatesat + S (jt_value_zeroorderenumprimitivecoordinates) = S ((S (jt_index_zeroorderenumprimitivecoordinates)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumprimitivecoordinatesat. jt_b_zeroorderenum = fs_q_jt_zeroorderenumprimitivecoordinatesat * S ((S (jt_index_zeroorderenumprimitivecoordinates)) * jt_c_zeroorderenum) + (jt_value_zeroorderenumprimitivecoordinates))) -> (exists jt_factor_zeroorderenumprimitivecoordinatesdivides. (jt_value_zeroorderenumprimitivecoordinates)=(jt_divisor_zeroorderenumprimitive)*jt_factor_zeroorderenumprimitivecoordinatesdivides)) -> jt_divisor_zeroorderenumprimitive=1))))) /\ (((forall jt_b_zeroorderenum jt_c_zeroorderenum. (forall jt_index_zeroorderenuminputbound. (exists jt_gap_zeroorderenuminputboundindex. jt_gap_zeroorderenuminputboundindex+S (jt_index_zeroorderenuminputbound)=(0)) -> exists jt_value_zeroorderenuminputbound. ((((exists fs_h_jt_zeroorderenuminputboundat. fs_h_jt_zeroorderenuminputboundat + S (jt_value_zeroorderenuminputbound) = S ((S (jt_index_zeroorderenuminputbound)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenuminputboundat. jt_b_zeroorderenum = fs_q_jt_zeroorderenuminputboundat * S ((S (jt_index_zeroorderenuminputbound)) * jt_c_zeroorderenum) + (jt_value_zeroorderenuminputbound))) /\ (exists jt_gap_zeroorderenuminputboundvalue. jt_gap_zeroorderenuminputboundvalue+S (jt_value_zeroorderenuminputbound)=(n)))) -> (forall jt_divisor_zeroorderenuminputprimitive. (exists jt_factor_zeroorderenuminputprimitivemodulus. (n)=(jt_divisor_zeroorderenuminputprimitive)*jt_factor_zeroorderenuminputprimitivemodulus) -> (forall jt_index_zeroorderenuminputprimitivecoordinates jt_value_zeroorderenuminputprimitivecoordinates. (exists jt_gap_zeroorderenuminputprimitivecoordinatesindex. jt_gap_zeroorderenuminputprimitivecoordinatesindex+S (jt_index_zeroorderenuminputprimitivecoordinates)=(0)) -> (((exists fs_h_jt_zeroorderenuminputprimitivecoordinatesat. fs_h_jt_zeroorderenuminputprimitivecoordinatesat + S (jt_value_zeroorderenuminputprimitivecoordinates) = S ((S (jt_index_zeroorderenuminputprimitivecoordinates)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenuminputprimitivecoordinatesat. jt_b_zeroorderenum = fs_q_jt_zeroorderenuminputprimitivecoordinatesat * S ((S (jt_index_zeroorderenuminputprimitivecoordinates)) * jt_c_zeroorderenum) + (jt_value_zeroorderenuminputprimitivecoordinates))) -> (exists jt_factor_zeroorderenuminputprimitivecoordinatesdivides. (jt_value_zeroorderenuminputprimitivecoordinates)=(jt_divisor_zeroorderenuminputprimitive)*jt_factor_zeroorderenuminputprimitivecoordinatesdivides)) -> jt_divisor_zeroorderenuminputprimitive=1) -> exists jt_i_zeroorderenum jt_d_zeroorderenum jt_e_zeroorderenum. ((exists jt_gap_zeroorderenumcompleteindex. jt_gap_zeroorderenumcompleteindex+S (jt_i_zeroorderenum)=(j)) /\ (((((((exists fs_h_jt_zeroorderenumcompletecode. fs_h_jt_zeroorderenumcompletecode + S (jt_d_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumcompletecode. jt_codes_zeroorder = fs_q_jt_zeroorderenumcompletecode * S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder) + (jt_d_zeroorderenum))) /\ (((exists fs_h_jt_zeroorderenumcompletescale. fs_h_jt_zeroorderenumcompletescale + S (jt_e_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumcompletescale. jt_scales_zeroorder = fs_q_jt_zeroorderenumcompletescale * S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder) + (jt_e_zeroorderenum))))) /\ (forall jt_index_zeroorderenumrepresented jt_left_zeroorderenumrepresented jt_right_zeroorderenumrepresented. (exists jt_gap_zeroorderenumrepresentedindex. jt_gap_zeroorderenumrepresentedindex+S (jt_index_zeroorderenumrepresented)=(0)) -> (((exists fs_h_jt_zeroorderenumrepresentedleft. fs_h_jt_zeroorderenumrepresentedleft + S (jt_left_zeroorderenumrepresented) = S ((S (jt_index_zeroorderenumrepresented)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumrepresentedleft. jt_b_zeroorderenum = fs_q_jt_zeroorderenumrepresentedleft * S ((S (jt_index_zeroorderenumrepresented)) * jt_c_zeroorderenum) + (jt_left_zeroorderenumrepresented))) -> (((exists fs_h_jt_zeroorderenumrepresentedright. fs_h_jt_zeroorderenumrepresentedright + S (jt_right_zeroorderenumrepresented) = S ((S (jt_index_zeroorderenumrepresented)) * jt_e_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumrepresentedright. jt_d_zeroorderenum = fs_q_jt_zeroorderenumrepresentedright * S ((S (jt_index_zeroorderenumrepresented)) * jt_e_zeroorderenum) + (jt_right_zeroorderenumrepresented))) -> jt_left_zeroorderenumrepresented=jt_right_zeroorderenumrepresented))))) /\ (forall jt_i_zeroorderenum jt_h_zeroorderenum jt_b_zeroorderenum jt_c_zeroorderenum jt_d_zeroorderenum jt_e_zeroorderenum. (exists jt_gap_zeroorderenumfirstindex. jt_gap_zeroorderenumfirstindex+S (jt_i_zeroorderenum)=(j)) -> (exists jt_gap_zeroorderenumsecondindex. jt_gap_zeroorderenumsecondindex+S (jt_h_zeroorderenum)=(j)) -> (((((exists fs_h_jt_zeroorderenumfirstcode. fs_h_jt_zeroorderenumfirstcode + S (jt_b_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumfirstcode. jt_codes_zeroorder = fs_q_jt_zeroorderenumfirstcode * S ((S (jt_i_zeroorderenum)) * jt_code_scale_zeroorder) + (jt_b_zeroorderenum))) /\ (((exists fs_h_jt_zeroorderenumfirstscale. fs_h_jt_zeroorderenumfirstscale + S (jt_c_zeroorderenum) = S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumfirstscale. jt_scales_zeroorder = fs_q_jt_zeroorderenumfirstscale * S ((S (jt_i_zeroorderenum)) * jt_scale_scale_zeroorder) + (jt_c_zeroorderenum))))) -> (((((exists fs_h_jt_zeroorderenumsecondcode. fs_h_jt_zeroorderenumsecondcode + S (jt_d_zeroorderenum) = S ((S (jt_h_zeroorderenum)) * jt_code_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumsecondcode. jt_codes_zeroorder = fs_q_jt_zeroorderenumsecondcode * S ((S (jt_h_zeroorderenum)) * jt_code_scale_zeroorder) + (jt_d_zeroorderenum))) /\ (((exists fs_h_jt_zeroorderenumsecondscale. fs_h_jt_zeroorderenumsecondscale + S (jt_e_zeroorderenum) = S ((S (jt_h_zeroorderenum)) * jt_scale_scale_zeroorder)) /\ exists fs_q_jt_zeroorderenumsecondscale. jt_scales_zeroorder = fs_q_jt_zeroorderenumsecondscale * S ((S (jt_h_zeroorderenum)) * jt_scale_scale_zeroorder) + (jt_e_zeroorderenum))))) -> (forall jt_index_zeroorderenumsame jt_left_zeroorderenumsame jt_right_zeroorderenumsame. (exists jt_gap_zeroorderenumsameindex. jt_gap_zeroorderenumsameindex+S (jt_index_zeroorderenumsame)=(0)) -> (((exists fs_h_jt_zeroorderenumsameleft. fs_h_jt_zeroorderenumsameleft + S (jt_left_zeroorderenumsame) = S ((S (jt_index_zeroorderenumsame)) * jt_c_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumsameleft. jt_b_zeroorderenum = fs_q_jt_zeroorderenumsameleft * S ((S (jt_index_zeroorderenumsame)) * jt_c_zeroorderenum) + (jt_left_zeroorderenumsame))) -> (((exists fs_h_jt_zeroorderenumsameright. fs_h_jt_zeroorderenumsameright + S (jt_right_zeroorderenumsame) = S ((S (jt_index_zeroorderenumsame)) * jt_e_zeroorderenum)) /\ exists fs_q_jt_zeroorderenumsameright. jt_d_zeroorderenum = fs_q_jt_zeroorderenumsameright * S ((S (jt_index_zeroorderenumsame)) * jt_e_zeroorderenum) + (jt_right_zeroorderenumsame))) -> jt_left_zeroorderenumsame=jt_right_zeroorderenumsame) -> jt_i_zeroorderenum=jt_h_zeroorderenum)))))))))

Constructive proof overview

Generated structural guide

Jordan is intentionally restricted to positive tuple order.

The unchanged tactic script uses 0 declared prerequisites and contains 6 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

none

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

6 script commands · 4 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro j
  3. L3
    intro h
02Separate the logical casesL4–4

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

  1. L4
    cases h
03Use earlier factsL5–5

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

  1. L5
    apply h_left
04Calculate and transport equalitiesL6–6

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L6
    refl

Library-wide reading audit

Original exact command ledger · 6 lines
  1. 0001intro n
  2. 0002intro j
  3. 0003intro h
  4. 0004cases h
  5. 0005apply h_left
  6. 0006refl