JT0058

jordan_zero_tuple_bounded_one

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

The literal beta tuple (0,0) has every coordinate below one, at every length.

Exact expanded first-order arithmetic statement

forall k. (forall jt_index_unit_zero_tuple. (exists jt_gap_unit_zero_tupleindex. jt_gap_unit_zero_tupleindex+S (jt_index_unit_zero_tuple)=(k)) -> exists jt_value_unit_zero_tuple. ((((exists fs_h_jt_unit_zero_tupleat. fs_h_jt_unit_zero_tupleat + S (jt_value_unit_zero_tuple) = S ((S (jt_index_unit_zero_tuple)) * 0)) /\ exists fs_q_jt_unit_zero_tupleat. 0 = fs_q_jt_unit_zero_tupleat * S ((S (jt_index_unit_zero_tuple)) * 0) + (jt_value_unit_zero_tuple))) /\ (exists jt_gap_unit_zero_tuplevalue. jt_gap_unit_zero_tuplevalue+S (jt_value_unit_zero_tuple)=(1))))

Constructive proof overview

Generated structural guide

The literal beta tuple (0,0) has every coordinate below one, at every length.

The unchanged tactic script uses 1 declared prerequisite and contains 9 exact native proof lines.

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

Proof neighborhood

Direct dependencies

finite_beta_zero_code Alpha theorem; checked-use authorized

Direct dependents

JT005A jordan_unit_modulus_singleton_enumeration

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

9 script commands · 6 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 k
  2. L2
    intro i
  3. L3
    intro hi
02Construct an explicit witnessL4–4

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

  1. L4
    exists 0
03Separate the logical casesL5–5

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

  1. L5
    split
04Use earlier factsL6–7

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

  1. L6
    specialize finite_beta_zero_code (i)
  2. L7
    apply finite_beta_zero_code
05Construct an explicit witnessL8–8

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

  1. L8
    exists 0
06Calculate and transport equalitiesL9–9

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

  1. L9
    simp

Library-wide reading audit

Original exact command ledger · 9 lines
  1. 0001intro k
  2. 0002intro i
  3. 0003intro hi
  4. 0004exists 0
  5. 0005split
  6. 0006specialize finite_beta_zero_code (i)
  7. 0007apply finite_beta_zero_code
  8. 0008exists 0
  9. 0009simp