Reference: ContextTower

@cite{anand-nevins-2004} @cite{banfield-1982} @cite{kaplan-1989} @cite{schlenker-2003}

End-to-end derivation chain connecting the ContextTower infrastructure to the direct reference and indexical shift data in Phenomena.Reference.DirectReference.

Derivation Chain

Core.Context.Tower (ContextTower, push, origin, innermost)
    ↓
Core.Context.Shifts (attitudeShift, perspectiveShift, identityShift)
    ↓
Theories.Semantics.Reference.FreeIndirectDiscourse (FIDProfile)
    ↓
This file: tower operations model Kaplan's thesis and its violations
    ↓
Phenomena.Reference.DirectReference (MonsterThesis, shift languages)

Key Results

1. Kaplan's thesis = identityShift: English attitude verbs push identity shifts, so embedded indexicals read from origin (speaker's context)
2. Indexical shift = perspectiveShift: shift languages (Amharic, Zazaki) push perspective shifts, so embedded "I" reads from local (attitude holder's context)
3. FID = mixed access: Classic FID reads agent from origin (narrator) but time/world from local (character) — the hallmark mixed perspective
4. Direct speech = full local access: All coordinates from the embedded context (full perspective shift)

inductive AnandNevins2004.Agent : Type

A context with distinguishable agents (for testing identity).

• narrator : Agent
• character : Agent

@[implicit_reducible]

instance AnandNevins2004.instDecidableEqAgent : DecidableEq Agent

Equations

• AnandNevins2004.instDecidableEqAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AnandNevins2004.instReprAgent : Repr Agent

Equations

• AnandNevins2004.instReprAgent = { reprPrec := AnandNevins2004.instReprAgent.repr }

def AnandNevins2004.instReprAgent.repr : Agent → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev AnandNevins2004.RefCtx : Type

Equations

• AnandNevins2004.RefCtx = Core.Context.KContext Unit AnandNevins2004.Agent Unit ℤ

def AnandNevins2004.speechCtx : RefCtx

Speech-act context: narrator speaking at time 0.

Equations

• AnandNevins2004.speechCtx = { agent := AnandNevins2004.Agent.narrator, addressee := AnandNevins2004.Agent.character, world := (), time := 0, position := () }

def AnandNevins2004.rootTower : Core.Context.ContextTower RefCtx

Root tower at the speech-act context.

Equations

• AnandNevins2004.rootTower = Core.Context.ContextTower.root AnandNevins2004.speechCtx

def AnandNevins2004.englishAttitudeTower : Core.Context.ContextTower RefCtx

English attitude verbs push identity shifts (Kaplan's thesis). "John said that I am here now" — "I", "here", "now" all refer to the speaker, not to John.

Equations

• AnandNevins2004.englishAttitudeTower = AnandNevins2004.rootTower.push Core.Context.identityShift

theorem AnandNevins2004.english_I_is_narrator : englishAttitudeTower.innermost.agent = Agent.narrator

Under an identity shift, the embedded agent is still the narrator. This is Kaplan's thesis: English indexicals are not shifted.

theorem AnandNevins2004.english_now_is_speech_time : englishAttitudeTower.innermost.time = 0

Under an identity shift, the embedded time is still 0. "Now" refers to the speech time, not the attitude time.

theorem AnandNevins2004.kaplan_holds_english : Phenomena.Reference.DirectReference.monsterThesis.holdsForEnglish = true

Kaplan's thesis holds for English — consistent with monsterThesis.holdsForEnglish.

def AnandNevins2004.shiftLanguageTower : Core.Context.ContextTower RefCtx

Shift languages (Amharic, Zazaki, etc.) push perspective shifts. The attitude verb shifts the agent to the attitude holder and the time to the attitude time.

Equations

• AnandNevins2004.shiftLanguageTower = AnandNevins2004.rootTower.push (Core.Context.perspectiveShift AnandNevins2004.Agent.character (-3) ())

theorem AnandNevins2004.shifted_I_is_character : shiftLanguageTower.innermost.agent = Agent.character

Under a perspective shift, the embedded agent is the character. "I" in Amharic under an attitude verb refers to the attitude holder.

theorem AnandNevins2004.shifted_now_is_attitude_time : shiftLanguageTower.innermost.time = -3

Under a perspective shift, the embedded time is the attitude time. "Now" in a shifted language refers to the attitude time, not speech time.

theorem AnandNevins2004.monsters_exist : Phenomena.Reference.DirectReference.monsterThesis.challengedCrossLinguistically = true

The monster thesis IS challenged cross-linguistically — consistent with monsterThesis.challengedCrossLinguistically.

def AnandNevins2004.fidTower : Core.Context.ContextTower RefCtx

Classic FID pushes a perspective shift (character's time/world) but reads the agent from origin (narrator). The FIDProfile encodes this per-coordinate depth specification.

Equations

• AnandNevins2004.fidTower = AnandNevins2004.rootTower.push (Core.Context.perspectiveShift AnandNevins2004.Agent.character (-5) ())

def AnandNevins2004.classicFIDProfile : Semantics.Reference.FreeIndirectDiscourse.FIDProfile

Classic FID profile: agent from origin, everything else from local.

Equations

• AnandNevins2004.classicFIDProfile = Semantics.Reference.FreeIndirectDiscourse.classicFID

theorem AnandNevins2004.fid_agent_is_narrator : classicFIDProfile.resolveAgent fidTower = Agent.narrator

In FID, the agent is the narrator (read from origin).

theorem AnandNevins2004.fid_time_is_character : classicFIDProfile.resolveTime fidTower = -5

In FID, the time is the character's (read from local).

theorem AnandNevins2004.fid_is_mixed_perspective : classicFIDProfile.resolveAgent fidTower ≠ fidTower.innermost.agent

FID is genuinely mixed: agent ≠ what perspectiveShift gives.

def AnandNevins2004.indirectProfile : Semantics.Reference.FreeIndirectDiscourse.FIDProfile

Indirect speech: all coordinates from origin (Kaplan-compliant).

Equations

• AnandNevins2004.indirectProfile = Semantics.Reference.FreeIndirectDiscourse.indirectSpeech

def AnandNevins2004.directProfile : Semantics.Reference.FreeIndirectDiscourse.FIDProfile

Direct speech: all coordinates from local (full shift).

Equations

• AnandNevins2004.directProfile = Semantics.Reference.FreeIndirectDiscourse.directSpeech

theorem AnandNevins2004.indirect_agent_narrator : indirectProfile.resolveAgent fidTower = Agent.narrator

In indirect speech, agent is narrator (from origin).

theorem AnandNevins2004.direct_agent_character : directProfile.resolveAgent fidTower = Agent.character

In direct speech, agent is character (from local).

theorem AnandNevins2004.fid_agent_eq_indirect : classicFIDProfile.resolveAgent fidTower = indirectProfile.resolveAgent fidTower

FID agent agrees with indirect speech (both from origin).

theorem AnandNevins2004.fid_time_eq_direct : classicFIDProfile.resolveTime fidTower = directProfile.resolveTime fidTower

FID time agrees with direct speech (both from local).

Bridge from @cite{anand-nevins-2004}'s shifty-operator framework to Semantics.Tense.DeRe.EntityConcept — the substrate's individual-side de re intension. The existing FIDProfile-based formalization above and the substrate's EntityConcept-based formalization are two perspectives on the same phenomenon; the substrate's Intension.IsRigid predicate distinguishes Kaplan-compliant from shifty indexicals at the type level.

The architectural payoff: this is **exactly parallel** to how
`Intension.IsRigid` distinguishes Abusch-style wide-scope rigid
time-references from de dicto descriptive time-concepts in
`Phenomena/TenseAspect/Studies/Abusch1997.lean` (`TimeConcept`).
The polymorphism in `Intension W τ` is non-trivial: individual
de re (this file) and temporal de re (Abusch) are *the same
machinery* at different `Res` types. The
`entityConcept_and_timeConcept_share_isRigid_substrate` theorem
below makes that claim kernel-checked. 

def AnandNevins2004.kaplanI : Semantics.Tense.DeRe.EntityConcept Unit Agent Unit ℤ

Kaplan-compliant "I" as a rigid EntityConcept.

The substrate's EntityConcept Intension (KContext) E is at Kaplan's content level — the result of applying his character to a context. Kaplan's I is technically a character (function from context to content) that returns c.author for any context; the content at a fixed actual context IS rigid. The substrate captures this content rigidity by modeling kaplanI as a constant intension at the speaker (here .narrator); the character-level structure is elided. This matches @cite{anand-nevins-2004}'s framing of English I as AUTH(c*) (sticky to actual context), contrasted with shifty languages where the operator can override the context parameter (yielding non-rigid agent-projection — see shiftedI).

Equations

• AnandNevins2004.kaplanI = Core.Intension.rigid AnandNevins2004.Agent.narrator

def AnandNevins2004.shiftedI : Semantics.Tense.DeRe.EntityConcept Unit Agent Unit ℤ

Anand-Nevins (2004 §1, eq. 2a) shifted "I" (Zazaki under OP_V): the operator overwrites the context parameter with the index parameter ([[OP_V[α]]]^{c,i} = [[α]]^{i,i}), so an embedded I reads the AUTHOR of whichever centered context is locally supplied. As an EntityConcept, this is the agent-projection function — non-rigid: it varies with whatever KContext is plugged in.

Equations

• AnandNevins2004.shiftedI c = c.agent

theorem AnandNevins2004.kaplanI_isRigid : Core.Intension.IsRigid kaplanI

Kaplan's "I" is rigid (entity-side analog of Abusch's "rigid time-concept" being the de re reading).

theorem AnandNevins2004.shiftedI_not_isRigid : ¬Core.Intension.IsRigid shiftedI

@cite{anand-nevins-2004}'s shifted "I" is non-rigid — discriminating witness from contexts with different agents. Entity-side analog of Abusch's "descriptive time-concept" being the de dicto reading.

theorem AnandNevins2004.shiftedI_at_shiftLanguageTower : shiftedI shiftLanguageTower.innermost = directProfile.resolveAgent shiftLanguageTower

Bridge to FIDProfile: the shifted I entity-concept evaluated at the embedded layer of shiftLanguageTower (perspective-shifted to .character) equals directProfile.resolveAgent shiftLanguageTower. Both formalize the "shifted indexical reads from local context" claim; the substrate exposes it as concept non-rigidity, the FIDProfile mechanism exposes it as .local depth access.

theorem AnandNevins2004.kaplanI_at_englishAttitudeTower (c : RefCtx) : kaplanI c = indirectProfile.resolveAgent englishAttitudeTower

Bridge to FIDProfile: Kaplan's I evaluated at any context equals indirectProfile.resolveAgent englishAttitudeTower. Both formalize the "Kaplan-compliant indexical reads from origin" claim; the substrate exposes it as concept rigidity, the FIDProfile mechanism exposes it as .origin depth access.

theorem AnandNevins2004.kaplanI_lifts_rigidly_to_timeConcept (f : Agent → ℤ) : Core.Intension.IsRigid fun (c : RefCtx) => f (kaplanI c)

Architectural payoff via Intension functoriality (the deep structural claim). Rigidity transfers across Res types via post-composition with ANY function — by the general Intension.IsRigid.map lemma in Core/Logic/Intensional/Rigidity.lean.

Concretely: @cite{anand-nevins-2004}'s Kaplan-compliant kaplanI (rigid at Res = Agent) yields, for any f : Agent → ℤ (e.g. "birth year of the speaker"), a rigid TimeConcept f ∘ kaplanI at Res = ℤ — proved by kaplanI_isRigid.map f. The parallel between individual de re (this file) and temporal de re (Studies/Abusch1997.lean) is the covariant action of Intension RefCtx on its target type: a one-line corollary of Intension.IsRigid.map, not a list of two facts.

@cite{abusch-1997}'s prose claim at p. 6 ("To apply the same machinery to de re belief, a further constraint is required... the same parallel as for tenses") is now functorially true: @cite{lewis-1979-attitudes} + @cite{cresswell-vonstechow-1982}'s centered-world reduction is formalized once and applies uniformly across all Res types via the same closure lemma.

theorem AnandNevins2004.entityConcept_rigid_iff_image_rigid_under_injective {f : Agent → ℤ} (hf : Function.Injective f) (c : Semantics.Tense.DeRe.EntityConcept Unit Agent Unit ℤ) : Core.Intension.IsRigid c ↔ Core.Intension.IsRigid fun (ctx : RefCtx) => f (c ctx)

Bidirectional structural equivalence under injective lifting: when f : Agent → ℤ is injective (e.g., a unique-birth-year function), rigidity of the lifted time-concept f ∘ c is EQUIVALENT to rigidity of the underlying entity-concept c. Both directions are corollaries of substrate-level functoriality: Intension.IsRigid.map (forward) and Intension.IsRigid.of_map_injective (reverse).

This establishes that the parallel between Anand-Nevins entity-concepts and Abusch time-concepts is not just a one-way mapping but a structural equivalence under any injective f — rigidity-classifying entity-concepts and their image time-concepts are the same problem up to the choice of injective lifting.