BT010C

three_mul_le_square_of_three_le

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Every natural at least three dominates three times itself by its square.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall s. (exists bcf_le_gap_b5rbtmsts_source. bcf_le_gap_b5rbtmsts_source + (3) = s) -> (exists bcf_le_gap_b5rbtmsts_result. bcf_le_gap_b5rbtmsts_result + (3 * s) = s * s)

Structural proof guide

Every natural at least three dominates three times itself by its square.

Direct prerequisites: mul_le_mul_right. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT001M mul_le_mul_right

Direct dependents

BT010D floor_sqrt_three_mul_le_double

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

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

Named ingredients (1)
mul le mul right
01Fix variables and assumptionsL1–2

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

  1. L1
    intro s
  2. L2
    intro hthree
02Use earlier factsL3–7

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

  1. L3
    specialize mul_le_mul_right 3
  2. L4
    specialize mul_le_mul_right s
  3. L5
    specialize mul_le_mul_right s
  4. L6
    apply mul_le_mul_right
  5. L7
    exact hthree

Library-wide reading audit

Original exact command ledger · 7 lines
  1. 0001intro s
  2. 0002intro hthree
  3. 0003specialize mul_le_mul_right 3
  4. 0004specialize mul_le_mul_right s
  5. 0005specialize mul_le_mul_right s
  6. 0006apply mul_le_mul_right
  7. 0007exact hthree