Gradient At-Issueness and Projectivity

@cite{roberts-2012} @cite{tonhauser-beaver-degen-2018}

At-issueness and projectivity are gradient, not binary, and anti-correlated. @cite{tonhauser-beaver-degen-2018} report r = .85 (9 expression types) and r = .99 (12 predicates) for the positive correlation between not-at-issueness and projectivity, equivalently a negative correlation between at-issueness and projectivity. This module lifts at-issueness from a binary enum to a bounded rational degree with threshold semantics, mirroring the pattern used for gradable adjectives (degree > θ → positive meaning).

Design

All four degree/threshold types are Rat01 (= ↥(Set.Icc (0 : ℚ) 1)) from Core.Scales.Scale. The type aliases document intent but share infrastructure (order instances, smart constructors, etc.).

Adjective	At-issueness
Degree max (Fin)	AtIssuenessDegree (Rat01)
Threshold max	AtIssuenessThreshold (Rat01)
positiveMeaning d θ	isAtIssue d θ

@[reducible, inline]

abbrev Core.Discourse.AtIssueness.AtIssuenessDegree : Type

A degree of at-issueness ∈ [0, 1]. 0 = fully backgrounded (not at-issue), 1 = fully at-issue.

Equations

• Core.Discourse.AtIssueness.AtIssuenessDegree = Core.Scale.Rat01

@[reducible, inline]

abbrev Core.Discourse.AtIssueness.ProjectivityDegree : Type

A degree of projectivity ∈ [0, 1]. 0 = no projection, 1 = obligatory projection.

Equations

• Core.Discourse.AtIssueness.ProjectivityDegree = Core.Scale.Rat01

@[reducible, inline]

abbrev Core.Discourse.AtIssueness.AtIssuenessThreshold : Type

Contextual threshold for at-issueness classification. Content with degree above this threshold counts as at-issue.

Equations

• Core.Discourse.AtIssueness.AtIssuenessThreshold = Core.Scale.Rat01

@[reducible, inline]

abbrev Core.Discourse.AtIssueness.ProjectivityThreshold : Type

Contextual threshold for projectivity classification.

Equations

• Core.Discourse.AtIssueness.ProjectivityThreshold = Core.Scale.Rat01

def Core.Discourse.AtIssueness.isAtIssue (d : AtIssuenessDegree) (θ : AtIssuenessThreshold) : Bool

Content is at-issue when its at-issueness degree exceeds the threshold. Mirrors positiveMeaning from Adjective/Theory.lean.

Equations

• Core.Discourse.AtIssueness.isAtIssue d θ = Core.Scale.Rat01.exceeds d θ

def Core.Discourse.AtIssueness.isProjective (d : ProjectivityDegree) (θ : ProjectivityThreshold) : Bool

Content is projective when its projectivity degree exceeds the threshold.

Equations

• Core.Discourse.AtIssueness.isProjective d θ = Core.Scale.Rat01.exceeds d θ

inductive Core.Discourse.AtIssueness.AtIssuenessClassical : Type

Binary at-issueness, recoverable from gradient degree + threshold. This is the same enum as in ProjectiveContent.lean, now derived.

• atIssue : AtIssuenessClassical
• notAtIssue : AtIssuenessClassical

instance Core.Discourse.AtIssueness.instDecidableEqAtIssuenessClassical : DecidableEq AtIssuenessClassical

Equations

• Core.Discourse.AtIssueness.instDecidableEqAtIssuenessClassical x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Discourse.AtIssueness.instReprAtIssuenessClassical : Repr AtIssuenessClassical

Equations

• Core.Discourse.AtIssueness.instReprAtIssuenessClassical = { reprPrec := Core.Discourse.AtIssueness.instReprAtIssuenessClassical.repr }

def Core.Discourse.AtIssueness.instReprAtIssuenessClassical.repr : AtIssuenessClassical → ℕ → Std.Format

Equations

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

def Core.Discourse.AtIssueness.instBEqAtIssuenessClassical.beq : AtIssuenessClassical → AtIssuenessClassical → Bool

Equations

• Core.Discourse.AtIssueness.instBEqAtIssuenessClassical.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Discourse.AtIssueness.instBEqAtIssuenessClassical : BEq AtIssuenessClassical

Equations

• Core.Discourse.AtIssueness.instBEqAtIssuenessClassical = { beq := Core.Discourse.AtIssueness.instBEqAtIssuenessClassical.beq }

def Core.Discourse.AtIssueness.toClassical (d : AtIssuenessDegree) (θ : AtIssuenessThreshold) : AtIssuenessClassical

Recover binary classification from gradient degree and threshold.

Equations

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

def Core.Discourse.AtIssueness.defaultThreshold : AtIssuenessThreshold

Default threshold at 0.5, matching the midpoint of the [0, 1] scale.

Equations

• Core.Discourse.AtIssueness.defaultThreshold = Core.Scale.Rat01.half

def Core.Discourse.AtIssueness.defaultProjectivityThreshold : ProjectivityThreshold

Default projectivity threshold at 0.5.

Equations

• Core.Discourse.AtIssueness.defaultProjectivityThreshold = Core.Scale.Rat01.half

structure Core.Discourse.AtIssueness.GradientPair : Type

A pair of at-issueness and projectivity ratings for a single expression.

• atIssueness : ℚ
• projectivity : ℚ

def Core.Discourse.AtIssueness.instReprGradientPair.repr : GradientPair → ℕ → Std.Format

Equations

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

instance Core.Discourse.AtIssueness.instReprGradientPair : Repr GradientPair

Equations

• Core.Discourse.AtIssueness.instReprGradientPair = { reprPrec := Core.Discourse.AtIssueness.instReprGradientPair.repr }

structure Core.Discourse.AtIssueness.AntiCorrelation : Type

Anti-correlation property: across a list of expression ratings, higher at-issueness systematically co-occurs with lower projectivity.

@cite{tonhauser-beaver-degen-2018} report r = .85 across 9 expression types (Exp 1a) and r = .99 across 12 clause-embedding predicates (Exp 1b), for the positive correlation between not-at-issueness and projectivity. This is equivalent to an anti-correlation between at-issueness and projectivity.

This structure captures the deterministic (monotone) version of the Gradient Projection Principle. The statistical version uses Pearson r.

• pairs : List GradientPair

  The paired ratings

• anticorrelated (i j : Fin self.pairs.length) : (self.pairs.get i).atIssueness < (self.pairs.get j).atIssueness → (self.pairs.get j).projectivity ≤ (self.pairs.get i).projectivity

  For any two items, if one has higher at-issueness, it should have lower projectivity (qualitative anti-correlation).

def Core.Discourse.AtIssueness.atIssuenessFromQUD {M : Type u_1} (q : QUD M) (content : M → Bool) (worlds : List M) : AtIssuenessDegree

Qualitative connection between QUD and at-issueness: content that doesn't distinguish QUD cells has low at-issueness.

@cite{roberts-2012}: at-issue content is content that addresses the QUD. Content that yields the same truth value across all worlds within each QUD cell is backgrounded (not at-issue).

The full measure-theoretic version would compute mutual information between content and QUD partition.

Equations

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

def Core.Discourse.AtIssueness.atIssuenessBoundedness : Scale.Boundedness

Both at-issueness and projectivity are closed-bounded scales on [0, 1].

Equations

• Core.Discourse.AtIssueness.atIssuenessBoundedness = Core.Scale.Boundedness.closed

def Core.Discourse.AtIssueness.projectivityBoundedness : Scale.Boundedness

Equations

• Core.Discourse.AtIssueness.projectivityBoundedness = Core.Scale.Boundedness.closed

def Core.Discourse.AtIssueness.ofPercent (n : ℚ) (h0 : 0 ≤ n) (h1 : n ≤ 100) : Scale.Rat01

Construct a degree from a rational in [0, 100], normalizing to [0, 1]. Useful for entering experimental ratings.

Equations

• Core.Discourse.AtIssueness.ofPercent n h0 h1 = ⟨n / 100, ⋯⟩