EXACT FORMAL CONTRACT AND ITS FOUNDATION
Verbatim source excerpts (complete files); authoritative paths shown below.
The source-file checksums are pinned in validation/contract.json.

===== TC10/Syntax.lean =====
import Mathlib.Algebra.Ring.Hom.Defs
import Mathlib.Tactic

/-!
Actual formula trees and strict evaluation. No simplification is performed:
both children of multiplication must evaluate, even if one evaluates to zero.
-/

namespace TC10

universe u v w

inductive Formula (F : Type u) (n : ℕ) : Type u where
  | var : Fin n → Formula F n
  | const : F → Formula F n
  | add : Formula F n → Formula F n → Formula F n
  | mul : Formula F n → Formula F n → Formula F n
  | inv : Formula F n → Formula F n

namespace Formula

variable {F : Type u} {n m : ℕ}

def size : Formula F n → ℕ
  | .var _ | .const _ => 1
  | .add f g | .mul f g => f.size + g.size + 1
  | .inv f => f.size + 1

def height : Formula F n → ℕ
  | .var _ | .const _ => 0
  | .add f g | .mul f g => max f.height g.height
  | .inv f => f.height + 1

theorem size_pos (f : Formula F n) : 0 < f.size := by
  cases f <;> simp [size]

theorem height_lt_size (f : Formula F n) : f.height < f.size := by
  induction f <;> simp_all [height, size] <;> omega

/-- Ordered substitution of actual trees. -/
def subst (σ : Fin n → Formula F m) : Formula F n → Formula F m
  | .var i => σ i
  | .const a => .const a
  | .add f g => .add (f.subst σ) (g.subst σ)
  | .mul f g => .mul (f.subst σ) (g.subst σ)
  | .inv f => .inv (f.subst σ)

variable {R : Type v} [Ring F] [Ring R]

/-- An inverse is an actual two-sided inverse in the target ring. -/
inductive Eval (c : F →+* R) (X : Fin n → R) : Formula F n → R → Prop where
  | var (i) : Eval c X (.var i) (X i)
  | const (a) : Eval c X (.const a) (c a)
  | add {f g a b} : Eval c X f a → Eval c X g b → Eval c X (.add f g) (a + b)
  | mul {f g a b} : Eval c X f a → Eval c X g b → Eval c X (.mul f g) (a * b)
  | inv {f a b} : Eval c X f a → a * b = 1 → b * a = 1 → Eval c X (.inv f) b

def Defined (c : F →+* R) (X : Fin n → R) (f : Formula F n) : Prop :=
  ∃ a, f.Eval c X a

variable {c : F →+* R} {X : Fin n → R} {f g : Formula F n} {a b : R}

theorem Eval.unique (ha : f.Eval c X a) (hb : f.Eval c X b) : a = b := by
  induction ha generalizing b with
  | var i => cases hb; rfl
  | const t => cases hb; rfl
  | add ha₁ ha₂ ih₁ ih₂ =>
      cases hb with
      | add hb₁ hb₂ => rw [ih₁ hb₁, ih₂ hb₂]
  | mul ha₁ ha₂ ih₁ ih₂ =>
      cases hb with
      | mul hb₁ hb₂ => rw [ih₁ hb₁, ih₂ hb₂]
  | @inv f a a' ha hright hleft ih =>
      cases hb with
      | inv hb hright' hleft' =>
          have hab := ih hb
          subst_vars
          exact left_inv_eq_right_inv hleft hright'

theorem defined_add_iff : (f.add g).Defined c X ↔ f.Defined c X ∧ g.Defined c X := by
  constructor
  · rintro ⟨_, h⟩; cases h with
    | add hf hg => exact ⟨⟨_, hf⟩, ⟨_, hg⟩⟩
  · rintro ⟨⟨a, hf⟩, ⟨b, hg⟩⟩
    exact ⟨a + b, .add hf hg⟩

theorem defined_mul_iff : (f.mul g).Defined c X ↔ f.Defined c X ∧ g.Defined c X := by
  constructor
  · rintro ⟨_, h⟩; cases h with
    | mul hf hg => exact ⟨⟨_, hf⟩, ⟨_, hg⟩⟩
  · rintro ⟨⟨a, hf⟩, ⟨b, hg⟩⟩
    exact ⟨a * b, .mul hf hg⟩

theorem defined_inv_iff : f.inv.Defined c X ↔ ∃ a, f.Eval c X a ∧ IsUnit a := by
  constructor
  · rintro ⟨b, h⟩; cases h with
    | @inv _ a _ h hab hba => exact ⟨a, h, ⟨⟨a, b, hab, hba⟩, rfl⟩⟩
  · rintro ⟨a, ha, u, rfl⟩
    exact ⟨↑u⁻¹, .inv ha u.val_inv u.inv_val⟩

/-- Explicitly rules out simplification of `0 * inverse(g)` in the domain model. -/
theorem zero_mul_inv_defined_iff :
    ((Formula.const 0).mul f.inv).Defined c X ↔ ∃ a, f.Eval c X a ∧ IsUnit a := by
  rw [defined_mul_iff, defined_inv_iff]
  exact and_iff_right ⟨c 0, .const 0⟩

theorem Eval.map {S : Type w} [Ring S] (φ : R →+* S) (h : f.Eval c X a) :
    f.Eval (φ.comp c) (fun i => φ (X i)) (φ a) := by
  induction h with
  | var i => exact .var i
  | const a => exact .const a
  | add _ _ ih₁ ih₂ => simpa using Eval.add ih₁ ih₂
  | mul _ _ ih₁ ih₂ => simpa using Eval.mul ih₁ ih₂
  | inv h hab hba ih =>
      exact .inv ih (by simpa using congrArg φ hab) (by simpa using congrArg φ hba)

theorem Eval.subst (σ : Fin n → Formula F m) (Y : Fin m → R)
    (hσ : ∀ i, (σ i).Eval c Y (X i)) (hf : f.Eval c X a) :
    (f.subst σ).Eval c Y a := by
  induction hf with
  | var i => exact hσ i
  | const a => exact .const a
  | add _ _ ih₁ ih₂ => exact .add ih₁ ih₂
  | mul _ _ ih₁ ih₂ => exact .mul ih₁ ih₂
  | inv _ hab hba ih => exact .inv ih hab hba

end Formula
end TC10

===== TC10/MatrixSemantics.lean =====
import TC10.Syntax
import Mathlib.LinearAlgebra.Matrix.Rank
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

namespace TC10

universe u v

abbrev Mat (F : Type u) (d : ℕ) := Matrix (Fin d) (Fin d) F
abbrev Tuple (F : Type u) (n d : ℕ) := Fin n → Mat F d

def scalarEmbedding {F : Type u} {E : Type v} [Ring F] [Ring E]
    (ι : F →+* E) (d : ℕ) : F →+* Mat E d :=
  (Matrix.scalar (Fin d)).comp ι

def Evaluates {F : Type u} {E : Type v} [Ring F] [Ring E]
    {n d : ℕ} (ι : F →+* E) (f : Formula F n) (X : Tuple E n d) (A : Mat E d) : Prop :=
  f.Eval (scalarEmbedding ι d) X A

/-- Every entry is an actual tree; positive rectangular shapes are part of the type. -/
structure ExprMatrix (F : Type u) (n : ℕ) where
  rows : ℕ
  cols : ℕ
  rows_pos : 0 < rows
  cols_pos : 0 < cols
  entry : Fin rows → Fin cols → Formula F n

namespace ExprMatrix

variable {F : Type u} {n : ℕ}

def size (M : ExprMatrix F n) : ℕ :=
  ∑ i, ∑ j, (M.entry i j).size

def HeightLE (M : ExprMatrix F n) (h : ℕ) : Prop :=
  ∀ i j, (M.entry i j).height ≤ h

abbrev Value (M : ExprMatrix F n) (E : Type v) (d : ℕ) :=
  Matrix (Fin M.rows × Fin d) (Fin M.cols × Fin d) E

/-- A value is the ordinary expanded block matrix, not a matrix over an abstract skew field. -/
def Eval {E : Type v} [Ring F] [Ring E] (M : ExprMatrix F n)
    {d : ℕ} (ι : F →+* E) (X : Tuple E n d) (A : M.Value E d) : Prop :=
  ∀ i j, Evaluates ι (M.entry i j) X (fun a b => A (i, a) (j, b))

def Defined {E : Type v} [Ring F] [Ring E] (M : ExprMatrix F n)
    {d : ℕ} (ι : F →+* E) (X : Tuple E n d) : Prop := ∃ A, M.Eval ι X A

/-- Extensions are explicit field embeddings; no common initial witness is required. -/
def Admissible [Field F] (M : ExprMatrix F n) : Prop :=
  ∃ (E : Type u) (_ : Field E) (ι : F →+* E) (d : ℕ),
    0 < d ∧ ∃ (X : Tuple E n d) (A : M.Value E d), M.Eval ι X A

theorem Eval.unique {E : Type v} [Ring F] [Ring E] {M : ExprMatrix F n}
    {d : ℕ} {ι : F →+* E} {X : Tuple E n d} {A B : M.Value E d}
    (hA : M.Eval ι X A) (hB : M.Eval ι X B) : A = B := by
  funext ⟨i, a⟩ ⟨j, b⟩
  exact congrFun (congrFun (Formula.Eval.unique (R := Mat E d) (hA i j) (hB i j)) a) b

def scalar (f : Formula F n) : ExprMatrix F n := ⟨1, 1, by omega, by omega, fun _ _ => f⟩

@[simp] theorem scalar_size (f : Formula F n) : (scalar f).size = f.size := by
  change (∑ _ : Fin 1, ∑ _ : Fin 1, f.size) = f.size
  simp

@[simp] theorem scalar_height (f : Formula F n) (h : ℕ) :
    (scalar f).HeightLE h ↔ f.height ≤ h := by
  simp [HeightLE, scalar]

end ExprMatrix

/-- A separate size budget for each member would be a different theorem. -/
def familySize {F : Type u} {n : ℕ} (Ms : List (ExprMatrix F n)) : ℕ :=
  (Ms.map ExprMatrix.size).sum

/-- Supremum-free universal upper rank, including every positive dimension and extension. -/
def UpperRank {F : Type u} [Field F] {n : ℕ} (M : ExprMatrix F n) (ρ : ℕ) : Prop :=
  ∀ (E : Type u) [Field E] (ι : F →+* E) (d : ℕ), 0 < d →
    ∀ (X : Tuple E n d) (A : M.Value E d), M.Eval ι X A → A.rank ≤ d * ρ

/-- A single evaluation with an integral attained rank and a universal upper bound. -/
def Attains {F : Type u} [Field F] {n D : ℕ} (M : ExprMatrix F n)
    (X : Tuple F n D) (ρ : ℕ) : Prop :=
  ρ ≤ min M.rows M.cols ∧
  (∃ A, M.Eval (RingHom.id F) X A ∧ A.rank = D * ρ) ∧ UpperRank M ρ

theorem attained_rank_unique {F : Type u} [Field F] {n D : ℕ}
    {M : ExprMatrix F n} {X : Tuple F n D} {ρ σ : ℕ} (hD : 0 < D)
    (hρ : Attains M X ρ) (hσ : Attains M X σ) : ρ = σ := by
  obtain ⟨_, ⟨A, hA, hrA⟩, _⟩ := hρ
  obtain ⟨_, ⟨B, hB, hrB⟩, _⟩ := hσ
  have h := hA.unique hB
  subst B
  exact Nat.eq_of_mul_eq_mul_left hD (hrA.symm.trans hrB)

/-- The normalized integer is intrinsic, even for different tuples and dimensions. -/
theorem attained_rank_independent {F : Type u} [Field F] {n D D' : ℕ}
    {M : ExprMatrix F n} {X : Tuple F n D} {Y : Tuple F n D'} {ρ σ : ℕ}
    (hD : 0 < D) (hD' : 0 < D') (hρ : Attains M X ρ) (hσ : Attains M Y σ) : ρ = σ := by
  obtain ⟨_, ⟨A, hA, hrA⟩, huρ⟩ := hρ
  obtain ⟨_, ⟨B, hB, hrB⟩, huσ⟩ := hσ
  have ha := huσ F (RingHom.id F) D hD X A hA
  have hb := huρ F (RingHom.id F) D' hD' Y B hB
  rw [hrA] at ha
  rw [hrB] at hb
  exact Nat.le_antisymm (Nat.le_of_mul_le_mul_left ha hD)
    (Nat.le_of_mul_le_mul_left hb hD')

end TC10

===== TC10/PrimeField.lean =====
import TC10.MatrixSemantics
import Mathlib.Data.ZMod.Basic

namespace TC10

universe u

/-- Only promised characteristics are inputs; no primality test is charged to the generator. -/
inductive Characteristic where
  | zero
  | prime (p : ℕ) (isPrime : p.Prime)

namespace Characteristic

def tag : Characteristic → ℕ
  | .zero => 0
  | .prime p _ => p

def PrimeField : Characteristic → Type
  | .zero => ℚ
  | .prime p _ => ZMod p

noncomputable instance primeFieldField (p : Characteristic) : Field p.PrimeField := by
  cases p with
  | zero => exact inferInstanceAs (Field ℚ)
  | prime p hp =>
      letI : Fact p.Prime := ⟨hp⟩
      exact inferInstanceAs (Field (ZMod p))

instance primeFieldChar (p : Characteristic) : CharP p.PrimeField p.tag := by
  cases p with
  | zero => exact inferInstanceAs (CharP ℚ 0)
  | prime p hp =>
      let : Fact p.Prime := ⟨hp⟩
      exact inferInstanceAs (CharP (ZMod p) p)

def embedding (p : Characteristic) (F : Type u) [Field F] [CharP F p.tag] :
    p.PrimeField →+* F := by
  cases p with
  | zero =>
      letI : CharZero F := CharP.charP_to_charZero F
      exact Rat.castHom F
  | prime p hp => exact ZMod.castHom (dvd_refl p) F

def mapTuple (p : Characteristic) {n D : ℕ} (F : Type u) [Field F] [CharP F p.tag]
    (X : Tuple p.PrimeField n D) : Tuple F n D :=
  fun i a b => p.embedding F (X i a b)

end Characteristic
end TC10

===== TC10/Encoding.lean =====
import TC10.PrimeField
import Mathlib.Data.Nat.Digits.Defs
import Mathlib.Data.Nat.Log
import Mathlib.Computability.TuringMachine.PostTuringMachine

namespace TC10

/-! Literal encodings in the paper, including the one-bit representation of zero. -/

def binaryDigits (t : ℕ) : List Bool :=
  if t = 0 then [false] else ((Nat.digits 2 t).reverse.map (fun b => b != 0))

def encodeNat (t : ℕ) : List Bool :=
  List.replicate (binaryDigits t).length true ++ [false] ++ binaryDigits t

def encodeRat (q : ℚ) : List Bool :=
  [decide (q.num < 0)] ++ encodeNat q.num.natAbs ++ encodeNat q.den

def encodeScalar : (p : Characteristic) → p.PrimeField → List Bool
  | .zero, q => encodeRat q
  | .prime _ _, z => encodeNat z.val

def encodeTuple (p : Characteristic) {n D : ℕ} (X : Tuple p.PrimeField n D) : List Bool :=
  (List.finRange n).flatMap fun i =>
    (List.finRange D).flatMap fun a =>
      (List.finRange D).flatMap fun b => encodeScalar p (X i a b)

structure Output (p : Characteristic) (n D : ℕ) where
  dimension_pos : 0 < D
  tuples : List (Tuple p.PrimeField n D)
  nonempty : tuples ≠ []

def encodeOutput {p : Characteristic} {n D : ℕ} (H : Output p n D) : List Bool :=
  encodeNat D ++ encodeNat H.tuples.length ++ H.tuples.flatMap (encodeTuple p)

def encodeInput (p : Characteristic) (n s h : ℕ) : List Bool :=
  encodeNat p.tag ++ List.replicate n true ++ [false] ++
    List.replicate s true ++ [false] ++ List.replicate h true ++ [false]

def logBound (t : ℕ) : ℕ := Nat.clog 2 (t + 2)

/-- Blank, zero, one, work symbol; finite alphabet independent of every input. -/
abbrev Alphabet := Fin 4
abbrev Machine (m : ℕ) := Turing.TM0.Machine Alphabet (Fin (m + 1))
abbrev Configuration (m : ℕ) := Turing.TM0.Cfg Alphabet (Fin (m + 1))

def tapeBit (b : Bool) : Alphabet := if b then 2 else 1

def run {m : ℕ} (G : Machine m) : ℕ → Configuration m → Option (Configuration m)
  | 0, a => some a
  | t + 1, a => (Turing.TM0.step G a).bind (run G t)

/-- Ordinary deterministic transitions, halting, and the complete literal output. -/
def OutputsWithin {m : ℕ} (G : Machine m) (p : Characteristic) (n s h bound : ℕ)
    {D : ℕ} (H : Output p n D) : Prop :=
  ∃ t ≤ bound, ∃ a : Configuration m,
    run G t (Turing.TM0.init ((encodeInput p n s h).map tapeBit)) = some a ∧
    Turing.TM0.step G a = none ∧
    a.Tape.right₀ = Turing.ListBlank.mk ((encodeOutput H).map tapeBit)

end TC10

===== TC10/MainTheorem.lean =====
import TC10.Encoding

/-!
# Exact target of the main theorem

`MainStatement` fixes the target independently of its proof. The unconditional
proof is `TC10.Runtime.MainGenerator.main`; `Runtime.FixedGenerator.specification`
also exposes one named machine and constants shared by every field universe.
The proposition and encoding are unchanged from the original specification.
-/

namespace TC10

universe u

def Structured {p : Characteristic} {n D : ℕ} (H : Output p n D) : Prop :=
  ∀ X ∈ H.tuples,
    (∀ i, IsUnit (X i)) ∧
    ∀ i j, ∃ U : (Mat p.PrimeField D)ˣ,
      X i = (U : Mat p.PrimeField D) * X j * (↑U⁻¹ : Mat p.PrimeField D)

/-- The same point works for the whole family; the family has one total budget. -/
def SimultaneousRanks {p : Characteristic} {n D : ℕ} (s h : ℕ)
    (H : Output p n D) : Prop :=
  ∀ (F : Type u) [Field F] [CharP F p.tag] (Ms : List (ExprMatrix F n)),
    Ms ≠ [] → familySize Ms ≤ s →
    (∀ M ∈ Ms, M.HeightLE h) → (∀ M ∈ Ms, M.Admissible) →
    ∃ X ∈ H.tuples, ∀ M ∈ Ms,
      ∃ ρ : ℕ, Attains M (p.mapTuple F X) ρ

def dimensionBound (p : Characteristic) (C s : ℕ) : ℕ :=
  if p.tag = 2 then C * s ^ 2 * logBound s ^ 3
  else C * s ^ 4 * logBound s ^ 4

def lengthBound (p : Characteristic) (C n s h : ℕ) : ℕ :=
  if p.tag = 2 then C * (h + 1) * s ^ 8 * logBound s ^ 6 * logBound n
  else C * (h + 1) * s ^ 10 * logBound s ^ 7 * logBound n

def bitBound (p : Characteristic) (C k n s : ℕ) : ℕ :=
  C * (n + s + logBound p.tag + 1) ^ k

/-- Source: `thm:paperMain`, manuscript SHA-256
`a5ade9ab6b987f26c9384fb2d0753e3a3c2afb139f76bfd6246f458ced3d1589`.
This is the historical target-source hash. The current paper, comment-only
specification revision, and semantic continuity are recorded in
`validation/contract.json`; the older hash is deliberately retained as provenance.

The dimension function has no variable-count or height argument. The machine
and absolute constants precede every characteristic and every input. The output
precedes every coefficient field and target family. Field extensions are explicit
embeddings; the statement is universe-polymorphic in coefficient fields.
-/
def MainStatement : Prop :=
  ∃ (m : ℕ) (G : Machine m) (D : Characteristic → ℕ → ℕ) (C k : ℕ),
    0 < C ∧ 0 < k ∧
    ∀ (p : Characteristic) (n s h : ℕ), 0 < n → 0 < s → h ≤ s →
      ∃ H : Output p n (D p s),
        D p s ≤ dimensionBound p C s ∧
        H.tuples.length ≤ lengthBound p C n s h ∧
        (encodeOutput H).length ≤ bitBound p C k n s ∧
        OutputsWithin G p n s h (bitBound p C k n s) H ∧
        Structured H ∧ SimultaneousRanks.{u} s h H

/-- The semantic subgoal; proved unconditionally by `TC10.SharpSemantic.semantic`.
It is also an immediate consequence of either completed main theorem. -/
def SemanticConstruction : Prop :=
  ∃ (D : Characteristic → ℕ → ℕ) (C : ℕ), 0 < C ∧
    ∀ (p : Characteristic) (n s h : ℕ), 0 < n → 0 < s → h ≤ s →
      ∃ H : Output p n (D p s),
        D p s ≤ dimensionBound p C s ∧
        H.tuples.length ≤ lengthBound p C n s h ∧
        Structured H ∧ SimultaneousRanks.{u} s h H

/-- A checked implication between specifications, not an existence proof. -/
theorem main_implies_semantic (hMain : MainStatement.{u}) : SemanticConstruction.{u} := by
  obtain ⟨m, G, D, C, k, hC, hk, h⟩ := hMain
  refine ⟨D, C, hC, ?_⟩
  intro p n s hgt hn hs hh
  obtain ⟨H, hD, hL, hbits, htime, hstruct, hranks⟩ := h p n s hgt hn hs hh
  exact ⟨H, hD, hL, hstruct, hranks⟩

end TC10

===== TC10/PaperContract.lean =====
import TC10.Runtime.MainGenerator
import TC10.Runtime.FixedGenerator
import TC10.GenericEvaluation

/-!
# Audit-facing expansion of the paper's main theorem

This corollary leaves the pinned specification unchanged. It expands the rank,
structure, budget and machine predicates, uses an actual common list index, and
allows the coefficient field, admissibility witnesses and upper-rank test fields
to live in three independent universes. The latter is justified by generic
specialization, rather than assumed as a universe convention.
-/
namespace TC10.PaperContract

universe u v w

/-- Trailing binary zeroes cannot disappear in the blank-tape quotient: both
bit symbols are nonblank. Thus literal output equality preserves every bit. -/
theorem tape_word_injective : Function.Injective
    (fun bits : List Bool => Turing.ListBlank.mk (bits.map tapeBit)) := by
  intro xs
  induction xs with
  | nil =>
    intro ys h
    cases ys with
    | nil => rfl
    | cons b ys =>
      have hh := congrArg Turing.ListBlank.head h
      cases b <;> simp [tapeBit] at hh
  | cons a xs ih =>
    intro ys h
    cases ys with
    | nil =>
      have hh := congrArg Turing.ListBlank.head h
      cases a <;> simp [tapeBit] at hh
    | cons b ys =>
      have hh := congrArg Turing.ListBlank.head h
      change tapeBit a = tapeBit b at hh
      have hab : a = b := by
        cases a <;> cases b
        all_goals first | rfl | norm_num [tapeBit] at hh
      have ht := congrArg Turing.ListBlank.tail h
      exact congrArg₂ List.cons hab (ih ht)

/-- A strict witness in any universe supplies a witness in the coefficient
field's universe. No assumption of a common witness is needed. -/
theorem admissible_of_witness {F : Type u} [Field F] {E : Type v} [Field E]
    {n d : ℕ} (M : ExprMatrix F n) (ι : F →+* E) (hd : 0 < d)
    (X : Tuple E n d) (A : M.Value E d) (hA : M.Eval ι X A) : M.Admissible := by
  obtain ⟨B, hB, _⟩ := GenericEvaluation.rank_lift ι M X A hA
  exact ⟨GenericEvaluation.GenericField F n d, inferInstance,
    GenericEvaluation.coefficients F n d, d, hd,
    GenericEvaluation.tuple F n d, B, hB⟩

/-- The original upper-rank predicate bounds evaluations over extension fields
in any universe, not just the one used in its definition. -/
theorem upperRank_any_universe {F : Type u} [Field F] {E : Type v} [Field E]
    {n d ρ : ℕ} {M : ExprMatrix F n} (h : UpperRank M ρ)
    (ι : F →+* E) (hd : 0 < d) (X : Tuple E n d) (A : M.Value E d)
    (hA : M.Eval ι X A) : A.rank ≤ d * ρ := by
  obtain ⟨B, hB, hr⟩ := GenericEvaluation.rank_lift ι M X A hA
  exact hr.trans (h (GenericEvaluation.GenericField F n d)
    (GenericEvaluation.coefficients F n d) d hd
    (GenericEvaluation.tuple F n d) B hB)

/-- The paper contract with its substantial shorthand expanded. In particular,
there are no generator, arithmetic, honesty, hitting or runtime hypotheses. -/
theorem main :
    ∃ (m : ℕ) (G : Machine m) (D : Characteristic → ℕ → ℕ) (C k : ℕ),
      0 < C ∧ 0 < k ∧
      ∀ (p : Characteristic) (n s h : ℕ), 0 < n → 0 < s → h ≤ s →
        ∃ H : Output p n (D p s),
          D p s ≤ (if p.tag = 2 then C * s ^ 2 * (Nat.clog 2 (s + 2)) ^ 3
            else C * s ^ 4 * (Nat.clog 2 (s + 2)) ^ 4) ∧
          H.tuples.length ≤ (if p.tag = 2 then
            C * (h + 1) * s ^ 8 * (Nat.clog 2 (s + 2)) ^ 6 * Nat.clog 2 (n + 2)
            else C * (h + 1) * s ^ 10 * (Nat.clog 2 (s + 2)) ^ 7 * Nat.clog 2 (n + 2)) ∧
          (encodeOutput H).length ≤ C * (n + s + Nat.clog 2 (p.tag + 2) + 1) ^ k ∧
          (∃ t ≤ C * (n + s + Nat.clog 2 (p.tag + 2) + 1) ^ k,
            ∃ a : Configuration m,
              run G t (Turing.TM0.init ((encodeInput p n s h).map tapeBit)) = some a ∧
              Turing.TM0.step G a = none ∧
              a.Tape.right₀ = Turing.ListBlank.mk ((encodeOutput H).map tapeBit)) ∧
          (∀ X ∈ H.tuples, (∀ i, IsUnit (X i)) ∧
            ∀ i j, ∃ U : (Mat p.PrimeField (D p s))ˣ,
              X i = (U : Mat p.PrimeField (D p s)) * X j *
                (↑U⁻¹ : Mat p.PrimeField (D p s))) ∧
          (∀ (F : Type u) [Field F] [CharP F p.tag] (Ms : List (ExprMatrix F n)),
            Ms ≠ [] →
            (Ms.map (fun M => ∑ i, ∑ j, (M.entry i j).size)).sum ≤ s →
            (∀ M ∈ Ms, ∀ i j, (M.entry i j).height ≤ h) →
            (∀ M ∈ Ms, ∃ (E : Type v) (_ : Field E) (ι : F →+* E) (d : ℕ),
              0 < d ∧ ∃ (X : Tuple E n d) (A : M.Value E d), M.Eval ι X A) →
            ∃ j : Fin H.tuples.length, ∀ i : Fin Ms.length, ∃ ρ : ℕ,
              ρ ≤ min (Ms.get i).rows (Ms.get i).cols ∧
              (∃ A, (Ms.get i).Eval (RingHom.id F)
                (p.mapTuple F (H.tuples.get j)) A ∧ A.rank = D p s * ρ) ∧
              (∀ (E : Type w) [Field E] (ι : F →+* E) (d : ℕ), 0 < d →
                ∀ (X : Tuple E n d) (A : (Ms.get i).Value E d),
                  (Ms.get i).Eval ι X A → A.rank ≤ d * ρ)) := by
  obtain ⟨m, G, D, C, k, hC, hk, hmain⟩ := Runtime.FixedGenerator.main.{u}
  refine ⟨m, G, D, C, k, hC, hk, ?_⟩
  intro p n s h hn hs hh
  obtain ⟨H, hD, hL, hbits, htime, hstruct, hranks⟩ := hmain p n s h hn hs hh
  refine ⟨H, hD, hL, hbits, htime, hstruct, ?_⟩
  intro F _ _ Ms hne hsize hheight hadm
  have hadm' : ∀ M ∈ Ms, M.Admissible := by
    intro M hM
    obtain ⟨E, _, ι, d, hd, X, A, hA⟩ := hadm M hM
    exact admissible_of_witness M ι hd X A hA
  obtain ⟨X, hX, hρ⟩ := hranks F Ms hne hsize hheight hadm'
  obtain ⟨j, hj⟩ := List.mem_iff_get.mp hX
  refine ⟨j, ?_⟩
  intro i
  obtain ⟨ρ, hshape, hvalue, hupper⟩ := hρ (Ms.get i) (List.get_mem Ms i)
  refine ⟨ρ, hshape, ?_, ?_⟩
  · simpa only [hj] using hvalue
  · intro E _ ι d hd Y A hA
    exact upperRank_any_universe hupper ι hd Y A hA

end TC10.PaperContract

===== TC10/Runtime/FixedGenerator.lean =====
import TC10.Runtime.MainGenerator

/-! One named finite machine, chosen independently of all field universes.
The unchanged MainStatement is recovered below. The new specification exposes
the same witnesses at every universe level without changing the generator,
the semantic predicates, the output encoding, or any quantitative bound. -/
namespace TC10.Runtime.FixedGenerator
universe u
noncomputable section

/-- A compilation certificate has no coefficient-field or universe parameter. -/
structure Compilation where
  states : ℕ
  machine : TC10.Machine states
  C : ℕ
  k : ℕ
  C_pos : 0 < C
  k_pos : 0 < k
  correct : ∀ (p : Characteristic) (n s h : ℕ), h ≤ s →
    let w := (MainGenerator.finish (p.tag,⟨n⟩,⟨s⟩,⟨h⟩)).val
    w.length ≤ bitBound p C k n s ∧
    ∃ t ≤ bitBound p C k n s, ∃ cfg,
      run machine t (Turing.TM0.init ((encodeInput p n s h).map tapeBit)) = some cfg ∧
      Turing.TM0.step machine cfg = none ∧
      cfg.Tape.right₀ = Turing.ListBlank.mk (w.map tapeBit)

theorem compilation_exists : Nonempty Compilation := by
  obtain ⟨m,G,C,k,hC,hk,hG⟩ := LiteralGenerator.compile MainGenerator.data_poly
  exact ⟨⟨m,G,C,k,hC,hk,hG⟩⟩

noncomputable def program : Compilation := Classical.choice compilation_exists
def stateCount : ℕ := program.states
noncomputable def generator : TC10.Machine stateCount := program.machine
def constant : ℕ := program.C + MainGenerator.boundConstant
def exponent : ℕ := program.k
def dimension : Characteristic → ℕ → ℕ := MainGenerator.dimension

theorem constant_pos : 0 < constant := by
  have := program.C_pos
  unfold constant
  omega
theorem exponent_pos : 0 < exponent := program.k_pos

/-- The witnesses in this statement are the same named constants at every
coefficient-field universe. No universe-dependent choice of machine occurs. -/
theorem specification (p : Characteristic) (n s h : ℕ)
    (_hn : 0 < n) (hs : 0 < s) (hh : h ≤ s) :
    ∃ H : Output p n (dimension p s),
      dimension p s ≤ dimensionBound p constant s ∧
      H.tuples.length ≤ lengthBound p constant n s h ∧
      (encodeOutput H).length ≤ bitBound p constant exponent n s ∧
      OutputsWithin generator p n s h (bitBound p constant exponent n s) H ∧
      Structured H ∧ SimultaneousRanks.{u} s h H := by
  obtain ⟨H,hD,hL,hS,hR,hE⟩ := MainGenerator.output.{u} p n s h hs hh
  obtain ⟨hbits,t,ht,cfg,hr,hhalt,hout⟩ := program.correct p n s h hh
  change (MainGenerator.finish (p.tag,⟨n⟩,⟨s⟩,⟨h⟩)).val.length ≤ _ at hbits
  change cfg.Tape.right₀ = Turing.ListBlank.mk
    ((MainGenerator.finish (p.tag,⟨n⟩,⟨s⟩,⟨h⟩)).val.map tapeBit) at hout
  rw [hE] at hbits hout
  have hbb : bitBound p program.C exponent n s ≤ bitBound p constant exponent n s :=
    Nat.mul_le_mul_right _ (Nat.le_add_right _ _)
  refine ⟨H,?_,?_,hbits.trans hbb,⟨t,ht.trans hbb,cfg,hr,hhalt,hout⟩,hS,hR⟩
  · apply hD.trans
    unfold dimensionBound constant
    split_ifs <;> gcongr <;> omega
  · apply hL.trans
    unfold lengthBound constant
    split_ifs <;> gcongr <;> omega

/-- The original theorem follows with these fixed, universe-free witnesses. -/
theorem main : MainStatement.{u} :=
  ⟨stateCount,generator,dimension,constant,exponent,constant_pos,exponent_pos,specification⟩

end
end TC10.Runtime.FixedGenerator
