Delta Kernel Semantics Cons Lift Var

The shifting environment

In formal logic, a de Bruijn index is a way of naming variables by counting how many binders stand between the variable and its point of introduction, instead of giving each variable a name. The declaration cons_liftVar concerns what happens to these indices when a new binder is pushed onto the environment, the record that maps indices to their values. It states a commutation property: adding a new entry to the front of the environment and then shifting the old indices by a fixed amount gives the same result as first shifting the old indices and then adding the new entry.

The statement is precise. If v is the value bound by the new binder, d is the shift amount, c is the cutoff below which indices are untouched, and ρ is the old environment, then for every index n, the environment cons v ρ applied to liftVar d (c+1) n equals cons v applied to the shifted old environment fun m => ρ (liftVar d c m) at n. In words: shifting after adding a binder is the same as adding the binder after shifting, provided the cutoff is adjusted by one to account for the new entry at position zero.

This lemma is one of several commutation facts in the framework's ledger, the discrete record of formal derivations, that together let the soundness proof move binders in and out of scope. It is proved constructively, without appeal to classical logic, so the larger soundness theorem downstream can be audited as free of choice axioms. The proof itself is a direct case analysis on the index n, using the definitions of cons and liftVar.

What the lemma does not claim is any physical content. It is purely syntactic bookkeeping about a formal language's variable binding. It does not say that shifting variables is the same as substituting a term, nor does it establish any property of the framework's cost function or recognition cycle. Its role is narrower: it is one small gear in the machine that checks the framework's own reasoning.

/-- `liftVar` at a raised cutoff commutes with `cons`, pointwise. This is
the binder case of the lifting lemma. -/
theorem cons_liftVar (v d c : Nat) (ρ : Env) :
    ∀ n, Env.cons v ρ (liftVar d (c + 1) n) =
      Env.cons v (fun m => ρ (liftVar d c m)) n := by
  intro n
  cases n with
  | zero => simp [liftVar]
  | succ m =>
    by_cases h : m < c
    · have h' : m + 1 < c + 1 := by omega
      simp [liftVar, h, h']
    · have h' : ¬ (m + 1 < c + 1) := by omega
      have e : m + 1 + d = (m + d) + 1 := by omega
      simp [liftVar, h, h', e]

/-- `liftVar` at a raised cutoff commutes with `cons`, pointwise. This is
the binder case of the lifting lemma. -/
theorem cons_liftVar (v d c : Nat) (ρ : Env) :
    ∀ n, Env.cons v ρ (liftVar d (c + 1) n) =
      Env.cons v (fun m => ρ (liftVar d c m)) n := by
  intro n
  cases n with
  | zero => simp [liftVar]
  | succ m =>
    by_cases h : m < c
    · have h' : m + 1 < c + 1 := by omega
      simp [liftVar, h, h']
    · have h' : ¬ (m + 1 < c + 1) := by omega
      have e : m + 1 + d = (m + d) + 1 := by omega
      simp [liftVar, h, h', e]

What this page does not claim

The lemma does not establish any physical property of the framework's cost function or recognition cycle. The lemma does not state that shifting variables is the same as substituting a term.

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: