Charlow (2025) — Staged updates: lifted interpretations for DNE in dynamic semantics

@cite{charlow-2025-staged-updates} @cite{groenendijk-stokhof-1991} @cite{krahmer-muskens-1995} @cite{gotham-2019-ac22} @cite{mandelkern-2022} @cite{hofmann-2025} @cite{spector-2025} @cite{charlow-2014}

Charlow's @cite{charlow-2025-staged-updates} (SALT 35 proceedings) gives an algebraic characterization of how to lift a non-DNE-validating dynamic substrate δ (e.g. DPL) into a richer Δ that does validate double-negation elimination. Three operations (up : δ → Δ, down : Δ → δ, invneg : Δ → Δ) plus three equational laws (Emb, Inv, Neg) suffice. Charlow's Fact 4 (the headline) says: any two lawful lifts of the same substrate are isomorphic on the image of the lifted interpretation.

Architectural placement

Per linglib anchoring discipline (CLAUDE.md), framework substrate originating with a paper lives in the originating Studies file until ≥ 2 paper-anchored consumers exist. Currently only this file consumes the lift framework, so the typeclasses live here. Promotion to Theories/Semantics/Dynamic/Lift.lean is queued for when a Mandelkern2022 or Gotham2019 study lands.

The framework is strictly more general than Core.Logic.Bilateral.IsBilateral: the Krahmer-Muskens (Instance 1) lift is bilateral and derives its laws from IsBilateral, but the other three instances (Gotham decomposed, Staged updates, Canonical) have non-bilateral shapes. IsLawfulDNELift does not extend IsBilateral; it consumes it where applicable.

Connection to existing linglib infrastructure

@cite{charlow-2014}'s AnaphoraFramework (Linglib/Studies/Anaphora/Charlow2014.lean) formalizes the partition of dynamic-anaphora frameworks into RepStrategy.stateThreading (DRT, DPL, CDRT, BUS) vs .typeStructure (TTR). Charlow 2025 strengthens the state-threading side: any two lifts that satisfy Emb/Inv/Neg over the same substrate δ are isomorphic on the image of liftInterp. This subsumes the prose "three incompatible DNE solutions" table in Theories/Semantics/Dynamic/Connectives/Defs.lean §49-78 for the state-threading row — bilateral and ICDRT-bilateral are not incompatible choices, they are isomorphic presentations once the substrate is fixed. TTR remains genuinely outside the lift framework (its classical metalanguage gives DNE statically, so there is no non-DNE substrate to lift from).

Scope of this file

• §1 DynamicSubstrate δ — algebraic interface (conj + neg)
• §2 DynForm Atom — paper's ℒ ::= Atom | ∃x | φ ∧ ψ | ¬φ
• §3 DNELift δ Δ (data) + IsLawfulDNELift δ Δ (Prop, three laws)
• §4 primInterp and liftInterp (paper's [·] and ⟨·⟩, Definition 4)
• §5 Fact 1 (DNE validation) — proved
• §6 Fact 2 (conservativity over the substrate) — proved
• §7 Fact 4 (lifts factor through canonical form δ ⊕ δ via lawful_lifts_factor_through_canonical; kernel congruence via canonical form via lawful_lifts_canonicalize_eq_implies — both proved unconditionally; the literal "kernel iff" requires substrate non-degeneracy which Charlow's Appendix A proof implicitly assumes)
• §8 Auxiliary DynamicProgramDisj, DynamicTruth typeclasses
• §9-12 Four lift constructions (KM, Gotham, Staged, Canonical) over the DPL substrate
• §13 Sanity tests

The Spector 2025 weak-meaning prediction (donkey example, p. 871 of paper) that discriminates bounded meanings from staged updates is not formalized here — it requires the Mandelkern2022 study file as scaffolding.

The Section 6 exceptional-scope D_σ framework is also out of scope; it requires the separate JoS @cite{charlow-2014} successor "Static and dynamic exceptional scope" which has its own study file pending.

class Studies.Anaphora.Charlow2025.DynamicSubstrate (δ : Type u) : Type u

A dynamic substrate is a carrier with binary conjunction and unary negation. The paper's δ. Concrete instances: DPL DPLRel E, CDRT DProp, ICDRT contexts, etc. The interpretation function [·] : ℒ → δ is supplied per-call as interpAtom and interpExi rather than as a typeclass field (no shared Language type exists across linglib's dynamic theories yet).

• conj : δ → δ → δ

  Substrate conjunction (paper's ∧_δ).

• neg : δ → δ

  Substrate negation (paper's ¬_δ). Should fail DNE on its own; the lift framework adds DNE without requiring it of the substrate.

inductive Studies.Anaphora.Charlow2025.DynForm (Atom : Type v) : Type v

The paper's ℒ ::= Atom | ∃x | φ ∧ ψ | ¬φ. The existential ∃x is a primitive zero-place atom: ∃x.φ is sugar for ∃x ∧ φ (paper §1, footnote on dynamic interpretation of ∃x).

• atom {Atom : Type v} : Atom → DynForm Atom
• exi {Atom : Type v} : ℕ → DynForm Atom
• conj {Atom : Type v} : DynForm Atom → DynForm Atom → DynForm Atom
• neg {Atom : Type v} : DynForm Atom → DynForm Atom

@[implicit_reducible]

instance Studies.Anaphora.Charlow2025.instReprDynForm {Atom✝ : Type u_1} [Repr Atom✝] : Repr (DynForm Atom✝)

Equations

• Studies.Anaphora.Charlow2025.instReprDynForm = { reprPrec := Studies.Anaphora.Charlow2025.instReprDynForm.repr }

def Studies.Anaphora.Charlow2025.instReprDynForm.repr {Atom✝ : Type u_1} [Repr Atom✝] : DynForm Atom✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

class Studies.Anaphora.Charlow2025.DNELift (δ : Type u) (Δ : Type w) [DynamicSubstrate δ] : Type (max u w)

DNELift data (paper's Definition 3 signatures): a richer type Δ equipped with up : δ → Δ, down : Δ → δ, and invneg : Δ → Δ. The laws live in IsLawfulDNELift; this class only carries the data so that the same δ × δ-shaped Δ can support multiple competing instances (Krahmer-Muskens vs. Gotham) without typeclass diamond.

• up : δ → Δ
• down : Δ → δ
• invneg : Δ → Δ

class Studies.Anaphora.Charlow2025.IsLawfulDNELift (δ : Type u) (Δ : Type w) [DynamicSubstrate δ] [self : DNELift δ Δ] : Prop

Lawful DNE lift (paper's Definition 3 laws): the three equational constraints that make a lift "lawful" in the paper's sense.

Following mathlib's Mul/IsLeftCancelMul convention, the data class DNELift is split from the Prop class IsLawfulDNELift. This avoids the 0.230.649 anti-pattern that deleted a prior bundled-typeclass attempt for bilateral logic; consumers can construct candidate DNELift instances without committing to lawfulness.

Field names use the descriptive down_X_up-style mathlib idiom rather than the paper's terse Emb/Inv/Neg to avoid name collisions and parser ambiguity.

• down_up (m : δ) : DNELift.down (DNELift.up m) = m

  Emb (paper): down ∘ up = id. The substrate embeds faithfully.

• invneg_invneg (M : Δ) : DNELift.invneg δ (DNELift.invneg δ M) = M

  Inv (paper): invneg ∘ invneg = id. The lifted negation is involutive.

• down_invneg_up (m : δ) : DNELift.down (DNELift.invneg δ (DNELift.up m)) = DynamicSubstrate.neg m

  Neg (paper): down ∘ invneg ∘ up = neg. Conjugation by lift recovers the substrate negation.

def Studies.Anaphora.Charlow2025.primInterp {Atom : Type v} {δ : Type u} [DynamicSubstrate δ] (interpAtom : Atom → δ) (interpExi : ℕ → δ) : DynForm Atom → δ

The substrate's primitive interpretation [·] : ℒ → δ. Recursive on the form structure, using only substrate operations.

Equations

• One or more equations did not get rendered due to their size.
• Studies.Anaphora.Charlow2025.primInterp interpAtom interpExi (Studies.Anaphora.Charlow2025.DynForm.atom a) = interpAtom a
• Studies.Anaphora.Charlow2025.primInterp interpAtom interpExi (Studies.Anaphora.Charlow2025.DynForm.exi a) = interpExi a
• Studies.Anaphora.Charlow2025.primInterp interpAtom interpExi a.neg = Studies.Anaphora.Charlow2025.DynamicSubstrate.neg (Studies.Anaphora.Charlow2025.primInterp interpAtom interpExi a)

def Studies.Anaphora.Charlow2025.liftInterp {Atom : Type v} {δ : Type u} {Δ : Type w} [DynamicSubstrate δ] [self : DNELift δ Δ] (interpAtom : Atom → δ) (interpExi : ℕ → δ) : DynForm Atom → Δ

The lifted interpretation ⟨·⟩ : ℒ → Δ (paper Definition 4). The only type-correct recursion given the lift signatures; conjunction sequences via up ∘ ∧_δ ∘ (down ⟨φ⟩, down ⟨ψ⟩), negation via ∼ directly.

Equations

• One or more equations did not get rendered due to their size.
• Studies.Anaphora.Charlow2025.liftInterp interpAtom interpExi (Studies.Anaphora.Charlow2025.DynForm.atom a) = Studies.Anaphora.Charlow2025.DNELift.up (interpAtom a)
• Studies.Anaphora.Charlow2025.liftInterp interpAtom interpExi (Studies.Anaphora.Charlow2025.DynForm.exi a) = Studies.Anaphora.Charlow2025.DNELift.up (interpExi a)
• Studies.Anaphora.Charlow2025.liftInterp interpAtom interpExi a.neg = Studies.Anaphora.Charlow2025.DNELift.invneg δ (Studies.Anaphora.Charlow2025.liftInterp interpAtom interpExi a)

theorem Studies.Anaphora.Charlow2025.liftInterp_dneg {Atom : Type v} {δ : Type u} {Δ : Type w} [DynamicSubstrate δ] [DNELift δ Δ] [IsLawfulDNELift δ Δ] (ia : Atom → δ) (ie : ℕ → δ) (φ : DynForm Atom) : liftInterp ia ie φ.neg.neg = liftInterp ia ie φ

Fact 1 (paper, p. 864): the lifted interpretation validates double negation elimination. ⟨¬¬φ⟩ = ⟨φ⟩ for any φ, by the involutive law on ∼.

inductive Studies.Anaphora.Charlow2025.NegFree {Atom : Type v} : DynForm Atom → Prop

A formula is negation-free if it contains no ¬.

• atom {Atom : Type v} (a : Atom) : NegFree (DynForm.atom a)
• exi {Atom : Type v} (n : ℕ) : NegFree (DynForm.exi n)
• conj {Atom : Type v} {φ ψ : DynForm Atom} : NegFree φ → NegFree ψ → NegFree (φ.conj ψ)

inductive Studies.Anaphora.Charlow2025.DNegFree {Atom : Type v} : DynForm Atom → Prop

A formula is double-negation-free if no subformula has the shape ¬¬ψ. The constructors enumerate the allowed ¬-prefixed shapes (atom, exi, conj of dneg-frees), excluding .neg (.neg ψ).

• atom {Atom : Type v} (a : Atom) : DNegFree (DynForm.atom a)
• exi {Atom : Type v} (n : ℕ) : DNegFree (DynForm.exi n)
• conj {Atom : Type v} {φ ψ : DynForm Atom} : DNegFree φ → DNegFree ψ → DNegFree (φ.conj ψ)
• neg_atom {Atom : Type v} (a : Atom) : DNegFree (DynForm.atom a).neg
• neg_exi {Atom : Type v} (n : ℕ) : DNegFree (DynForm.exi n).neg
• neg_conj {Atom : Type v} {φ ψ : DynForm Atom} : DNegFree φ → DNegFree ψ → DNegFree (φ.conj ψ).neg

theorem Studies.Anaphora.Charlow2025.liftInterp_eq_up_primInterp_of_negFree {Atom : Type v} {δ : Type u} {Δ : Type w} [DynamicSubstrate δ] [DNELift δ Δ] [IsLawfulDNELift δ Δ] (ia : Atom → δ) (ie : ℕ → δ) {φ : DynForm Atom} (h : NegFree φ) : liftInterp ia ie φ = DNELift.up (primInterp ia ie φ)

Fact 2.i (paper, p. 864): for ¬-free φ, the lifted interpretation is literally the up-lift of the substrate interpretation.

theorem Studies.Anaphora.Charlow2025.down_liftInterp_eq_primInterp_of_dnegFree {Atom : Type v} {δ : Type u} {Δ : Type w} [DynamicSubstrate δ] [DNELift δ Δ] [IsLawfulDNELift δ Δ] (ia : Atom → δ) (ie : ℕ → δ) {φ : DynForm Atom} (h : DNegFree φ) : DNELift.down (liftInterp ia ie φ) = primInterp ia ie φ

Fact 2.ii (paper, p. 864): for ¬¬-free φ, lowering the lifted interpretation recovers the substrate interpretation exactly.

Canonical form of a lifted formula

Each lawful-lift value ⟨φ⟩_Δ decomposes into (substrate value, parity bit) where the parity tracks the residual negation count after DNE collapse. Following mathlib's structural-typing idiom for binary-tagged values, we encode the parity as Sum δ δ: Sum.inl m is "positive m" (even negations), Sum.inr m is "negative m" (odd). Sum.swap is the canonical involution implementing parity flip — directly mirroring IsLawfulDNELift.invneg_invneg.

def Studies.Anaphora.Charlow2025.canonicalize {Atom : Type v} {δ : Type u} [DynamicSubstrate δ] (ia : Atom → δ) (ie : ℕ → δ) : DynForm Atom → δ ⊕ δ

Canonical form of a formula's lifted interpretation. Depends only on the substrate δ and interpretations ia/ie, not on the lift Δ.

Equations

• One or more equations did not get rendered due to their size.
• Studies.Anaphora.Charlow2025.canonicalize ia ie (Studies.Anaphora.Charlow2025.DynForm.atom a) = Sum.inl (ia a)
• Studies.Anaphora.Charlow2025.canonicalize ia ie (Studies.Anaphora.Charlow2025.DynForm.exi a) = Sum.inl (ie a)
• Studies.Anaphora.Charlow2025.canonicalize ia ie a.neg = (Studies.Anaphora.Charlow2025.canonicalize ia ie a).swap

def Studies.Anaphora.Charlow2025.encodeCanonical (Δ : Type w) {δ : Type u} [DynamicSubstrate δ] [self : DNELift δ Δ] : δ ⊕ δ → Δ

Encoding the canonical form into any lawful lift Δ: positive m is up m; negative m is invneg (up m). Δ is explicit because the input δ ⊕ δ doesn't constrain it for inference. The self named binding on the DNELift δ Δ instance makes Lean use the in-scope instance for the body's up/invneg calls (rather than searching afresh).

Equations

• Studies.Anaphora.Charlow2025.encodeCanonical Δ (Sum.inl m) = Studies.Anaphora.Charlow2025.DNELift.up m
• Studies.Anaphora.Charlow2025.encodeCanonical Δ (Sum.inr m) = Studies.Anaphora.Charlow2025.DNELift.invneg δ (Studies.Anaphora.Charlow2025.DNELift.up m)

theorem Studies.Anaphora.Charlow2025.down_encodeCanonical {δ : Type u} (Δ : Type w) [DynamicSubstrate δ] [DNELift δ Δ] [IsLawfulDNELift δ Δ] (s : δ ⊕ δ) : DNELift.down (encodeCanonical Δ s) = Sum.elim id DynamicSubstrate.neg s

Down-projection of an encoded canonical form: s.elim id neg. Direct from Emb (down ∘ up = id) and Neg (down ∘ invneg ∘ up = neg).

theorem Studies.Anaphora.Charlow2025.encodeCanonical_swap {δ : Type u} (Δ : Type w) [DynamicSubstrate δ] [self : DNELift δ Δ] [IsLawfulDNELift δ Δ] (s : δ ⊕ δ) : encodeCanonical Δ s.swap = DNELift.invneg δ (encodeCanonical Δ s)

Inv law for the canonical encoding: encodeCanonical ∘ Sum.swap = invneg ∘ encodeCanonical. The structural counterpart of IsLawfulDNELift.invneg_invneg.

theorem Studies.Anaphora.Charlow2025.lawful_lifts_factor_through_canonical {Atom : Type v} {δ : Type u} (Δ : Type w) [DynamicSubstrate δ] [self : DNELift δ Δ] [IsLawfulDNELift δ Δ] (ia : Atom → δ) (ie : ℕ → δ) (φ : DynForm Atom) : liftInterp ia ie φ = encodeCanonical Δ (canonicalize ia ie φ)

Fact 4 (paper, p. 869) — factor-through-canonical form.

For any lawful lift Δ, the lifted interpretation ⟨·⟩ : ℒ → Δ factors through a canonical form δ ⊕ δ that depends only on the substrate, not on the lift: ⟨φ⟩_Δ = encodeCanonical (canonicalize φ).

This is the substantive content of Charlow's Fact 4. The bijection f : Im(⟨·⟩)₁ → Im(⟨·⟩)₂ Charlow constructs in Appendix A is the natural transformation between encodings of the same canonical form in different Δs: f ∘ encodeCanonical_1 = encodeCanonical_2.

The corollary canonicalize φ = canonicalize ψ → ⟨φ⟩_Δ = ⟨ψ⟩_Δ (one direction of the literal "kernel congruence iff" Charlow states) follows immediately — see lawful_lifts_canonicalize_eq_implies below.

The other direction of the iff (⟨φ⟩₁ = ⟨ψ⟩₁ → ⟨φ⟩₂ = ⟨ψ⟩₂) requires substrate non-degeneracy (no m : δ with m = neg m, since with such m the KMLift collapses formulas the CanonicalLift distinguishes — paper Appendix A's well-definedness check implicitly assumes this). For "real" substrates like DPL the iff holds; the abstract iff is genuinely substrate-dependent. The factor-through formulation is what's provable unconditionally.

theorem Studies.Anaphora.Charlow2025.lawful_lifts_canonicalize_eq_implies {Atom : Type v} {δ : Type u} {Δ₁ Δ₂ : Type w} [DynamicSubstrate δ] [DNELift δ Δ₁] [IsLawfulDNELift δ Δ₁] [DNELift δ Δ₂] [IsLawfulDNELift δ Δ₂] (ia : Atom → δ) (ie : ℕ → δ) (φ ψ : DynForm Atom) (h : canonicalize ia ie φ = canonicalize ia ie ψ) : liftInterp ia ie φ = liftInterp ia ie ψ ∧ liftInterp ia ie φ = liftInterp ia ie ψ

Kernel congruence via canonical form (paper Fact 4, the unconditionally-provable direction). If two formulas have the same canonical form, every lawful lift identifies them.

class Studies.Anaphora.Charlow2025.DynamicProgramDisj (δ : Type u) [DynamicSubstrate δ] : Type u

Program disjunction (paper's m ∪ n, Definition 6 / §3): the externally-dynamic union of two updates. Needed by Gotham (Instance 2) and Staged updates (Instance 3); not needed by KM (Instance 1) or Canonical (Instance 4). Separate typeclass to avoid burdening the basic substrate with operations its non-DNE-extending consumers do not need.

• pdisj : δ → δ → δ

  Program disjunction m ∪ n. For DPL: λ g h => m g h ∨ n g h.

class Studies.Anaphora.Charlow2025.DynamicTruth (δ : Type u) (i : outParam (Type v)) [DynamicSubstrate δ] : Type (max u v)

Truth as a static proposition (paper's True_δ(m), Definition 2 / Definition 5): the set of indices where m succeeds. Indexed by the substrate's index type i. Needed by Staged updates (Instance 3).

• truth : δ → i → Prop

  True_δ(m) := { i | i[m] ≠ ∅ }. For DPL: λ g, ∃ h, m g h.

• restrict : δ → (i → Prop) → δ

  m|_p: restrict m to inputs in p. For DPL: λ g h, p g ∧ m g h.

@[implicit_reducible]

instance Studies.Anaphora.Charlow2025.instDynamicSubstrateDPLRel (E : Type u) : DynamicSubstrate (Semantics.Dynamic.DPL.DPLRel E)

The DPL relational meaning type (DPLRel E := (Nat → E) → (Nat → E) → Prop) is a DynamicSubstrate via its native conjunction and negation.

Equations

• Studies.Anaphora.Charlow2025.instDynamicSubstrateDPLRel E = { conj := Semantics.Dynamic.DPL.conj, neg := Semantics.Dynamic.DPL.neg }

def Studies.Anaphora.Charlow2025.dplProgramDisj {E : Type u} (φ ψ : Semantics.Dynamic.DPL.DPLRel E) : Semantics.Dynamic.DPL.DPLRel E

Program disjunction on DPLRel: pointwise OR. Note this differs from DPL's DPLRel.disj (which is externally-static, clearing the assignment); program disjunction preserves output bindings.

Equations

• Studies.Anaphora.Charlow2025.dplProgramDisj φ ψ g h = (φ g h ∨ ψ g h)

@[implicit_reducible]

instance Studies.Anaphora.Charlow2025.instDynamicProgramDisjDPLRel (E : Type u) : DynamicProgramDisj (Semantics.Dynamic.DPL.DPLRel E)

Equations

• Studies.Anaphora.Charlow2025.instDynamicProgramDisjDPLRel E = { pdisj := Studies.Anaphora.Charlow2025.dplProgramDisj }

@[implicit_reducible]

instance Studies.Anaphora.Charlow2025.instDynamicTruthDPLRel (E : Type u) : DynamicTruth (Semantics.Dynamic.DPL.DPLRel E) (ℕ → E)

Equations

• One or more equations did not get rendered due to their size.

Instance 1: 2D DPL (Krahmer-Muskens 1995)

Δ ::= δ × δ (pairs of updates). The lift m^↑ := (m, ¬_δ m) pairs every update with its substrate negation. down projects the first component; invneg swaps. Charlow notes (p. 865, footnote 5) that this is his own reconstruction of @cite{krahmer-muskens-1995} as a lifted interpretation — the original K&M presentation interprets DRSs, not first-order formulas, and is distinguished syntactically from static conditions.

This instance derives IsLawfulDNELift directly from the algebraic shape of Prod: down (up m) = m is Prod.fst_mk; invneg (invneg M) = M is Prod.swap_swap; down (invneg (up m)) = neg m is by computation. The swap-axiom witness is also packaged as a Core.Logic.Bilateral.IsBilateral proof (see kmIsBilateral below), making the connection to existing linglib bilateral substrate explicit.

structure Studies.Anaphora.Charlow2025.KMLift (δ : Type u) : Type u

Instance 1's carrier: pairs of updates over the same substrate. Implemented as a structure (not a def := δ × δ alias) so that typeclass search treats it as a distinct type from GothamLift δ (which has the same underlying shape).

• positive : δ

  Positive update component (the substrate update itself).

• negative : δ

  Negative update component (the substrate's negation of the positive).

@[implicit_reducible]

instance Studies.Anaphora.Charlow2025.KMLift.instDNELift {δ : Type u} [DynamicSubstrate δ] : DNELift δ (KMLift δ)

Equations

• One or more equations did not get rendered due to their size.

instance Studies.Anaphora.Charlow2025.KMLift.instIsLawfulDNELift {δ : Type u} [DynamicSubstrate δ] : IsLawfulDNELift δ (KMLift δ)

theorem Studies.Anaphora.Charlow2025.KMLift.kmIsBilateral {δ : Type u} : Core.Logic.Bilateral.IsBilateral positive negative fun (M : KMLift δ) => { positive := M.negative, negative := M.positive }

Connection to Core.Logic.Bilateral.IsBilateral: the KM lift's projections witness the paraconsistent-bilateral pattern, with positive as the positive interpretation, negative as the negative interpretation, and a swap-style negate. Demonstrates linglib interconnection density.

The leading omit [DynamicSubstrate δ] clears the namespace-scoped variable that this lemma doesn't use (bilaterality of projection-and-swap is a Prod-shape fact, not a substrate fact).

Instance 2: Decomposed updates (Gotham 2019)

Δ ::= δ × δ, but with a different lift: m^↑ := (¬¬m, m ∪ ¬_δ m). The first component is the doubly-negated (truth-conditional) half; the second is a "dynamic tautology" m ∪ ¬m that introduces drefs in either horn. down is conjunction; invneg negates the truth-conditional half.

The full IsLawfulDNELift instance is not declared here — Gotham's Emb law (¬¬m) ∧_δ (m ∪ ¬m) = m is provable for the DPL substrate by unfolding conj, neg, pdisj definitions (paper p. 867 sketches the argument), but does not hold for arbitrary DynamicSubstrate + DynamicProgramDisj. A future PR formalising Gotham 2019 as its own study should add the DPL-specific instance + the substrate axioms required for generality.

The lift data is provided so that liftInterp (Δ := GothamLift δ) can be typed; IsLawfulDNELift synthesis fails (correctly) so dependent theorems do not silently accept un-proved laws.

structure Studies.Anaphora.Charlow2025.GothamLift (δ : Type u) : Type u

Instance 2's carrier: pairs of (truth-conditional, dynamic-tautology) halves. Distinct structure from KMLift despite the same shape — different field names + different lift operations.

• truthCond : δ

  Doubly-negated, truth-conditional half (¬¬m).

• tautology : δ

  Dynamic-tautology half (m ∪ ¬m), introduces drefs in either horn.

@[implicit_reducible]

instance Studies.Anaphora.Charlow2025.GothamLift.instDNELift {δ : Type u} [DynamicSubstrate δ] [DynamicProgramDisj δ] : DNELift δ (GothamLift δ)

Equations

• One or more equations did not get rendered due to their size.

Instance 3: Staged updates (Charlow 2025)

Δ ::= (i → Prop) × δ (pairs of static propositional content and updates). The lift m^↑ := (True_δ(m), m ∪ ¬_δ m) decomposes a δ-meaning into its truth-conditional content plus a dynamic tautology. down reconstitutes by restriction; invneg flips the static-proposition half.

Like Gotham, the full IsLawfulDNELift instance is not declared here — the laws hold over the DPL substrate (paper p. 868) but require unfolding truth, restrict, and pdisj definitions. Future PR for Mandelkern2022 or Charlow's own §6 will add the DPL-specific lawfulness proof.

structure Studies.Anaphora.Charlow2025.StagedLift (δ : Type u) (i : Type v) : Type (max u v)

Instance 3's carrier: pairs of static propositions and updates.

• staticContent : i → Prop

  Static propositional content (True_δ(m) shape).

• update : δ

  Update component carrying the dynamic tautology.

@[implicit_reducible]

instance Studies.Anaphora.Charlow2025.StagedLift.instDNELift {δ : Type u} {i : Type v} [DynamicSubstrate δ] [DynamicProgramDisj δ] [DynamicTruth δ i] : DNELift δ (StagedLift δ i)

Equations

• One or more equations did not get rendered due to their size.

Instance 4: Canonical Δ = Bool × δ (Fact 3, p. 868)

The minimal/canonical lift: tag each substrate value with a Boolean indicating whether to apply ¬_δ on lowering. Generic over any DynamicSubstrate — no program disjunction or truth needed.

m^↑ := (true, m); (b, m)^↓ := if b then m else ¬_δ m; ∼(b, m) := (¬b, m). All three laws hold by case analysis on the Bool. Lawful in full generality; unique among the four instances in being so.

structure Studies.Anaphora.Charlow2025.CanonicalLift (δ : Type u) : Type u

Instance 4's carrier: pairs of booleans and updates.

• flag : Bool

  Polarity flag: true means "apply m as-is", false means "negate m".

• update : δ

  The underlying substrate update.

@[implicit_reducible]

instance Studies.Anaphora.Charlow2025.CanonicalLift.instDNELift {δ : Type u} [DynamicSubstrate δ] : DNELift δ (CanonicalLift δ)

Equations

• One or more equations did not get rendered due to their size.

instance Studies.Anaphora.Charlow2025.CanonicalLift.instIsLawfulDNELift {δ : Type u} [DynamicSubstrate δ] : IsLawfulDNELift δ (CanonicalLift δ)