Delta Kernel Semantics Eval Subst

Substitution without surprise

In formal logic, substitution is the operation of replacing a free variable in a term or formula by another term. The lemma eval_subst in the Recognition Science library establishes, for the framework's own kernel language, that substitution behaves exactly as intended: evaluating a term after substituting s for variable k gives the same result as evaluating the original term in an environment where variable k now holds the value of s. In symbols, for every term t, eval ρ (t.subst k s) = eval (Env.substAt k (s.eval ρ) ρ) t. This is a theorem in the machine-checked library: a formal proof, not a convention.

The statement is a commutation lemma: it says that two different routes to the same destination agree. One route performs the substitution first, then evaluates. The other route evaluates the replacement term, adjusts the environment, then evaluates the original term. The lemma proves these routes coincide for every term, every variable position, and every environment. Its proof in the library proceeds by induction on the structure of t, splitting on whether a variable is the substituted one, lies above it, or below it. The library records the proof as a theorem, which means it has been checked by the kernel's own rules.

Why does the framework care? The kernel language is the framework's own formal system, the one it uses to state and prove its results. The lemma eval_subst is one of the four commutation facts (with eval_lift, sat_lift, and sat_subst) that the soundness proof for the kernel's logic needs. Soundness, in turn, is what lets the framework trust that its proofs do not prove falsehoods. The docstring notes that all these lemmas are proved constructively, without classical logic, so the downstream soundness theorem can be audited as choice-free. That audit is the kernel's own ledger applied to the kernel.

The lemma does not claim that substitution is always safe in every logic, nor that the kernel's semantics is the only possible one. It claims a specific equality for the kernel's own evaluation function and substitution operation. It does not prove that the kernel is consistent, that its axioms are true, or that the framework's larger results are correct. Those are separate theorems, with their own proofs. The lemma is a precise, local fact: substitution commutes with evaluation in this one language.

/-- Substitution commutes with evaluation through `substAt`. -/
theorem eval_subst (k : Nat) (s : DTerm) (ρ : Env) : ∀ t : DTerm,
    eval ρ (DTerm.subst k s t) = eval (Env.substAt k (s.eval ρ) ρ) t
  | var n => by
      by_cases h1 : n = k
      · simp [subst, eval, Env.substAt, h1]
      · by_cases h2 : k < n
        · simp [subst, eval, Env.substAt, h1, h2]
        · simp [subst, eval, Env.substAt, h1, h2]
  | zero => rfl
  | succ t => by simp [subst, eval, eval_subst k s ρ t]
  | add t u => by simp [subst, eval, eval_subst k s ρ t, eval_subst k s ρ u]
  | mul t u => by simp [subst, eval, eval_subst k s ρ t, eval_subst k s ρ u]

/-- Substitution commutes with evaluation through `substAt`. -/
theorem eval_subst (k : Nat) (s : DTerm) (ρ : Env) : ∀ t : DTerm,
    eval ρ (DTerm.subst k s t) = eval (Env.substAt k (s.eval ρ) ρ) t
  | var n => by
      by_cases h1 : n = k
      · simp [subst, eval, Env.substAt, h1]
      · by_cases h2 : k < n
        · simp [subst, eval, Env.substAt, h1, h2]
        · simp [subst, eval, Env.substAt, h1, h2]
  | zero => rfl
  | succ t => by simp [subst, eval, eval_subst k s ρ t]
  | add t u => by simp [subst, eval, eval_subst k s ρ t, eval_subst k s ρ u]
  | mul t u => by simp [subst, eval, eval_subst k s ρ t, eval_subst k s ρ u]

What this page does not claim

The lemma does not prove that substitution is safe in every formal logic. The lemma does not establish the consistency of the kernel or the truth of its axioms. The lemma does not by itself prove any of the framework's physical or mathematical results.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/DeltaKernel/Semantics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: