prove(polytime): close nontriviality certificate

[eliasjudin]

Aristotle-generated closure of the three isolated nontriviality-certificate gaps, with the accepted proof artifacts and local validation recorded in the branch.

The sole commit is explicitly co-authored with Aristotle (Harmonic).

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: prove(polytime): close nontriviality certificate

ℹ️ This PR modifies 1 file(s) under ToMathlib/ — consider whether a corresponding upstream PR is needed.

sorry delta: -3 (3 removed) — net proof progress

This PR closes the three remaining nontriviality certificate gaps in the polynomial-time formalization. It provides a full proof of exists_tmTable_of_card_le and a cardinality bound B d ^ 2 on RealizableLE n d using a new tablePairPred construction that reifies and runs machine pairs, relying on the new Relation.ReflTransGen.unique_of_deterministic lemma to establish output determinism for single‑tape machines. Also, exists_realizableLE_covering is proved via the image of tablePairPred. A new snocComputer machine and its polynomial-time lemmas are added, along with appendBit and exists_iterate lifting EncPolyTime, used to complete the proof of exists_poly_realizable_of_implements, which was previously sorry-ed. No new sorrys or admits are introduced; all previously marked placeholders are resolved.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	556
❌ Lines Removed	29

---

Lean Declarations

✏️ Added: 37 declaration(s)

ToMathlib/Computability/MachineCounting.lean (17)

• lemma decFin_embFin {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) (s : α) :
• lemma embFin_injective {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) :
• lemma normCfg_injective (hemb : Function.Injective emb) :
• lemma normCfg_reflTransGen (hdec : ∀ s, dec (emb s) = some s) {c c' : tm.Cfg}
• lemma reflTransGen_normCfg_reverse (hdec : ∀ s, dec (emb s) = some s) {c : tm.Cfg}
• lemma step_normCfg (hdec : ∀ s, dec (emb s) = some s) (c : tm.Cfg) :
• noncomputable def decFin {α : Type*} [Fintype α] {d : ℕ} (i : Fin d) : Option α
• noncomputable def embFin {α : Type*} [Fintype α] {d : ℕ} (hd : Fintype.card α ≤ d) (s : α) :
• noncomputable def normCfg (c : tm.Cfg) : (reify (normTable tm emb dec)).Cfg
• noncomputable def normTable : TMTable d
• noncomputable def normTr : Fin d → Option Bool → SingleTapeTM.Stmt Bool × Option (Fin d)
• noncomputable def tablePairPred (n d : ℕ) (p : TMTable d × TMTable d) : BitVec n → Bool
• theorem Outputs_unique (tm : SingleTapeTM Symbol) {l l₁ l₂ : List Symbol}
• theorem PolyTimeComputable.outputs {f : List Symbol → List Symbol}
• theorem _root_.Relation.ReflTransGen.unique_of_deterministic
• theorem _root_.Turing.BiTape.mk₁_injective {Symbol : Type} :
• theorem not_transitionRelation_haltCfg (tm : SingleTapeTM Symbol) (l : List Symbol)

VCVio/OracleComp/Coinductive/PolyTimeNontrivial.lean (20)

• @[simp] private lemma snocPush_cons (L : StackTape Bool) (b : Bool) (t : List Bool) :
• @[simp] private lemma snocPush_nil (L : StackTape Bool) : snocPush L [] = L
• def snocComputer (c : Bool) : SingleTapeTM Bool where
• def snocTimeComputable (c : Bool) : TimeComputable (fun l => l ++ [c]) where
• lemma snocComputer_outputsWithinTime (c : Bool) (l : List Bool) :
• noncomputable def appendBit {σ : Type} (es : σ → List Bool) (c : Bool) :
• noncomputable def snocPolyTimeComputable (c : Bool) :
• private def snocPush : StackTape Bool → List Bool → StackTape Bool
• private lemma mapSome_head (l : List Bool) :
• private lemma mapSome_tail (l : List Bool) :
• private lemma mk₁_eq (s : List Bool) :
• private lemma snocComputer_phaseA (c : Bool) (L : StackTape Bool) : ∀ l : List Bool,
• private lemma snocComputer_phaseB (c : Bool) : ∀ (m : List Bool) (R : StackTape Bool),
• private lemma snocPush_empty (l : List Bool) :
• private lemma snocPush_final (c : Bool) (l : List Bool) :
• private lemma snocPush_toList (L : StackTape Bool) (l : List Bool) :
• private lemma stackTape_ext {a b : StackTape Bool} (h : a.toList = b.toList) : a = b
• theorem exists_iterate {σ : Type} (es : σ → List Bool) {g : σ → σ}
• theorem size_appendBit {σ : Type} (es : σ → List Bool) (c : Bool) :
• theorem size_snocPolyTimeComputable (c : Bool) :

---

sorry Tracking

✅ Removed: 3 `sorry`(s)

ToMathlib/Computability/MachineCounting.lean (2)

• theorem exists_realizableLE_covering (n d : ℕ) : (L155)
• theorem exists_tmTable_of_card_le {f : List Bool → List Bool} (h : PolyTimeComputable f) (L117)

VCVio/OracleComp/Coinductive/PolyTimeNontrivial.lean (1)

• theorem exists_poly_realizable_of_implements (L69)

---

📋 **Additional Analysis**

Review Findings

1. Attribution and File Headers

• No issues. The diff does not create new .lean files; it modifies existing files. The existing headers in MachineCounting.lean and PolyTimeNontrivial.lean are preserved, which is correct per the attribution policy (routine edits preserve existing headers).

2. Documentation Expectations

• Module docstrings: Both files have module docstrings. The diff updates the module docstring in MachineCounting.lean to remove sorry references and reflect the now-filled content, which is appropriate.
• Declaration docstrings: All new public definitions (embFin, decFin, normTr, normTable, normCfg, step_normCfg, normCfg_reflTransGen, reflTransGen_normCfg_reverse, tablePairPred, snocComputer, snocTimeComputable, snocPolyTimeComputable, appendBit, exists_iterate) have docstrings. This meets the expectation.
• Prose layout: The new Normalize and Determinism sections use /-! ## Section title -/ headers, not ASCII banners. Good.
• PolyTimeNontrivial.lean local support section: The docstring says "Local support: appending a fixed bit on a single-tape machine" — this is descriptive, which is fine.
• Potential docstring minor issue in snocPush: This is a private lemma with no docstring — acceptable.

3. sorry Removal

• exists_tmTable_of_card_le: The sorry is removed and replaced with a full proof. Meets the instruction: "Avoid leaving sorry in finished work unless the change is explicitly meant to preserve partial work."
• exists_realizableLE_covering: The sorry is removed and replaced with a full proof. Good.
• exists_poly_realizable_of_implements: The sorry is removed and replaced with a full proof. Good.

4. Lean Options and Linters

• No set_option changes in the diff. The diff does not introduce autoImplicit = false or linter suppressions. Complies.

5. Section Headers

• Both files use /-! ## Section title -/ (e.g., /-! ## State-relabeling normalization construction -/, /-! ## Determinism of machine runs -/, /-! ## State normalization -/, /-! ## Local support: appending a fixed bit on a single-tape machine -/). No ASCII banners. Good.

6. Naming Conventions

• Fintype.card usage: Fintype.card h.tm.State (in exists_tmTable_of_card_le) is a Nat term — fine.
• Theorem names: normCfg_reflTransGen, reflTransGen_normCfg_reverse, Outputs_unique, not_transitionRelation_haltCfg — these are snake_case (terms of Prop), correct.
• Definition names: embFin, decFin, normTr, normTable, normCfg, snocComputer — these are lowerCamelCase (terms of a type), correct.
• Type names: PolyTimeComputable, TimeComputable, EncPolyTime, MachineAdversary — these are UpperCamelCase, correct.
• One potential naming issue: decFin_embFin lemma name mixes snake_case with camelCase — this is fine (lemma names are snake_case; embFin is a definition).

7. Imports at Top of File

• The diff does not change import ordering; the existing imports are at the top. No violation.

8. Use of snocComputer Section Headers

• The snocComputer section uses /-! ## Local support: ... -/, which is correct. No ASCII banners.

9. Module Layering (per instructions to respect AGENTS.md)

• The diff does not appear to violate the layering (both files are in ToMathlib/Computability/ and VCVio/OracleComp/Coinductive/, which are plausible locations). No cross-layer imports introduced in the diff.

10. Progress Against Project Framework (Tier Transitions, Obligation Mappings)

• The diff removes the two sorry comments in MachineCounting.lean that were marked as "Isolated crux" and "Isolated counting crux", and the sorry in PolyTimeNontrivial.lean marked as "B-factor — isolated crux". This fills three known gaps/the sorries. The diff also provides the supporting lemmas (Outputs_unique, embFin, decFin, snocComputer) that enable the proofs.
• The summary lines in the module docstring of MachineCounting.lean are updated to reflect the now-completed state normalization and covering result.

Summary of Findings

• All sorry instances mentioned in the module docstring/placeholders are removed.
• Documentation and styling conform to the project's guide.
• No new linter suppressions, no unwanted set_option changes, no ASCII banners.
• Attribution headers are correctly preserved.
• The diff is directly relevant to the supplied instructions and addresses the stated goals.

---

📄 **Per-File Summaries**

• ToMathlib/Computability/MachineCounting.lean: The module-level documentation is updated to remove the two isolated sorry annotations. A new state-relabeling normalization construction (embFin, decFin, normTr, normTable, normCfg, plus lemmas step_normCfg, normCfg_reflTransGen, reflTransGen_normCfg_reverse) is added, which is used to prove the previously sorry-ed exists_tmTable_of_card_le theorem. A determinism section introduces Relation.ReflTransGen.unique_of_deterministic, BiTape.mk₁_injective, Outputs_unique, and PolyTimeComputable.outputs to establish that single‑tape machine runs are deterministic. The previously sorry-ed exists_realizableLE_covering is now proved: a new tablePairPred maps a pair of TMTable d to a BitVec n → Bool predicate by running the two reified machines and decoding the output using Outputs_unique, and the theorem shows that RealizableLE n d is covered by the image of tablePairPred on TMTable d × TMTable d, yielding the cardinality bound B d ^ 2 via card_tmTable.
• VCVio/OracleComp/Coinductive/PolyTimeNontrivial.lean: The diff adds a new snocComputer machine in Turing.SingleTapeTM (with lemmas snocComputer_outputsWithinTime, snocTimeComputable, snocPolyTimeComputable, size_snocPolyTimeComputable) that appends a fixed bit to a list, and adds appendBit and exists_iterate in Computability.EncPolyTime to lift this to the encoding level and iterate a self-map witness. The main change is that the previously sorry-marked theorem exists_poly_realizable_of_implements is now fully proved, replacing the placeholder with a complete argument that uses these new definitions to compile the deterministic run of the adversary and bound its description size.

---

Last updated: 2026-07-14 15:39 UTC.

[dtumad]

Thanks for the proofs, much appreciated! Depending how much the underlying #481 draft changes before final review we can either merge this directly or I can rebase off these commits to preserve authorship if those changes end up breaking something here.