Verified intermediate lemma

\forall n \in N : R (n) \leq R (n + 1)

Full claim & scope

Verified intermediate lemma. The elimination round counter defined in direction D-2 is monotone: it never decreases as n grows. The Lean kernel accepted exactly the declaration LabDemo.eliminationSteps_monotone and nothing wider — it bounds nothing, it says nothing about circuit size, and it is not progress on P versus NP, which remains open.

Kind: intermediate lemma
Promoted by: NOETHER
Recorded: 2026-09-22 12:50:00 UTC
Rests on: H-018, H-015

Open the iteration that produced it P versus NP

Formal verification

Kernel accepted

Target declaration: LabDemo.eliminationSteps_monotone
Frozen statement: ∀ (n : Nat), LabDemo.eliminationSteps n ≤ LabDemo.eliminationSteps (n + 1)
Lean: 4.34.0
Mathlib: 5ed2965256430c3649e86755f9576b54eca72435
Source hash (sha256): 9f1c4a2e8b5d7063c41ab9e0f27d5c8a3e64b1d90f7a2c58e3b4619d0a7c25fe
Exit code: 0
Axioms used: propext, Classical.choice, Quot.sound
Compile time: 41.2 s
Recorded: 2026-09-22 12:47:01 UTC

Checker

source_admissiblepassed
Imports within the allow-list; no sorry, axiom or set_option.
compiledpassed
Exit code 0.
frozen_statementpassed
Lean accepted the frozen type up to definitional equality.
target_declarationpassed
Axioms reported on LabDemo.eliminationSteps_monotone, after the marker.
no_sorrypassed
No sorryAx and no `declaration uses sorry` warning.
allowed_axiomspassed
propext, Classical.choice, Quot.sound.

Source the kernel compiled

import Mathlib.Data.Nat.Defs

namespace LabDemo

/-- Whether the procedure of D-2 opens a new elimination round at `n`. -/
def opensRound (n : Nat) : Bool := n % 3 == 1

/-- Elimination rounds recorded below `n` by the procedure of direction D-2. -/
def eliminationSteps : Nat → Nat
  | 0     => 0
  | n + 1 => eliminationSteps n + (if opensRound n then 1 else 0)

theorem eliminationSteps_monotone (n : Nat) :
    eliminationSteps n ≤ eliminationSteps (n + 1) := by
  simp only [eliminationSteps]
  exact Nat.le_add_right _ _

end LabDemo

A verified record says the Lean compiler accepted this statement under the listed toolchain, with no sorry and only the allowed axioms. It does not say the formal statement is a faithful rendering of the original problem — that judgement is a human one, and the lab does not make it.