JT0057

jordan_tuple_bounded_one_entry_zero

Every decoded coordinate in a tuple bounded by one equals zero.

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

∀ b. ∀ c. ∀ k. ∀ i. ∀ a. BetaPrefixInto(b,c,k,1) → Lt(i,k) → BetaAt(b,c,i,a) → a = 0

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

beta_at_unique · checked external prerequisitele_zero · checked external prerequisitele_of_succ_le_succ · checked external prerequisite
Original expanded first-order statement 
forall b c k i a. (forall jt_index_unit_tuple. (exists jt_gap_unit_tupleindex. jt_gap_unit_tupleindex+S (jt_index_unit_tuple)=(k)) -> exists jt_value_unit_tuple. ((((exists fs_h_jt_unit_tupleat. fs_h_jt_unit_tupleat + S (jt_value_unit_tuple) = S ((S (jt_index_unit_tuple)) * c)) /\ exists fs_q_jt_unit_tupleat. b = fs_q_jt_unit_tupleat * S ((S (jt_index_unit_tuple)) * c) + (jt_value_unit_tuple))) /\ (exists jt_gap_unit_tuplevalue. jt_gap_unit_tuplevalue+S (jt_value_unit_tuple)=(1)))) -> (exists jt_gap_unit_index. jt_gap_unit_index+S (i)=(k)) -> (((exists fs_h_jt_unit_entry. fs_h_jt_unit_entry + S (a) = S ((S (i)) * c)) /\ exists fs_q_jt_unit_entry. b = fs_q_jt_unit_entry * S ((S (i)) * c) + (a))) -> (a=0)

Complete tactic proof in conservative notation

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

26 script commands · 6 reading checkpoints · 1 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.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro k
  4. L4
    intro i
  5. L5
    intro a
  6. L6
    intro hBound
  7. L7
    intro hi
  8. L8
    intro ha
02Establish hValueL9–12

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

  1. L9
    have hValue : ∃ z. BetaAt(b,c,i,z) ∧ Lt(z,1)Definitions: BetaAt(b,c,i,z)Lt(z,1)Original native command in the exact edition
  2. L10
    specialize hBound (i)
  3. L11
    apply hBound
  4. L12
    exact hi
03Separate the logical casesL13–14

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

  1. L13
    cases hValue
  2. L14
    cases hValue_witness
04Calculate and transport equalitiesL15–15

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

  1. L15
    trans x
05Use earlier factsL16–25

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

  1. L16
    specialize beta_at_unique (b)
  2. L17
    specialize beta_at_unique (c)
  3. L18
    specialize beta_at_unique (i)
  4. L19
    specialize beta_at_unique (a)
  5. L20
    specialize beta_at_unique (x)
  6. L21
    apply beta_at_unique
  7. L22
    exact ha
  8. L23
    exact hValue_witness_left
  9. L24
    apply le_zero
  10. L25
    apply le_of_succ_le_succ
06Use earlier factsL26–26

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

  1. L26
    exact hValue_witness_right

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro k
  4. 0004intro i
  5. 0005intro a
  6. 0006intro hBound
  7. 0007intro hi
  8. 0008intro ha
  9. 0009have hValue : ∃ z. BetaAt(b,c,i,z) ∧ Lt(z,1)
  10. 0010specialize hBound (i)
  11. 0011apply hBound
  12. 0012exact hi
  13. 0013cases hValue
  14. 0014cases hValue_witness
  15. 0015trans x
  16. 0016specialize beta_at_unique (b)
  17. 0017specialize beta_at_unique (c)
  18. 0018specialize beta_at_unique (i)
  19. 0019specialize beta_at_unique (a)
  20. 0020specialize beta_at_unique (x)
  21. 0021apply beta_at_unique
  22. 0022exact ha
  23. 0023exact hValue_witness_left
  24. 0024apply le_zero
  25. 0025apply le_of_succ_le_succ
  26. 0026exact hValue_witness_right