Gradient At-Issueness and Projectivity

[Rob12] [TBD18] Tonhauser-Beaver-Degen 2018's gradient at-issueness model: degrees and thresholds in Rat01, with at-issueness anti-correlated with projectivity. Mirrors the gradable-adjective pattern (degree > θ → positive meaning).

Degree Types

@[reducible, inline]

abbrev Discourse.AtIssueness.AtIssuenessDegree : Type

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

Equations

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

@[reducible, inline]

abbrev Discourse.AtIssueness.ProjectivityDegree : Type

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

Equations

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

@[reducible, inline]

abbrev Discourse.AtIssueness.AtIssuenessThreshold : Type

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

Equations

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

@[reducible, inline]

abbrev Discourse.AtIssueness.ProjectivityThreshold : Type

Contextual threshold for projectivity classification.

Equations

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

Threshold Semantics

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

Content is at-issue when its degree exceeds the threshold.

Equations

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

@[implicit_reducible]

instance Discourse.AtIssueness.instDecidableIsAtIssue (d : AtIssuenessDegree) (θ : AtIssuenessThreshold) : Decidable (isAtIssue d θ)

Equations

• Discourse.AtIssueness.instDecidableIsAtIssue d θ = Discourse.AtIssueness.instDecidableIsAtIssue._aux_1 d θ

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

Content is projective when its projectivity degree exceeds the threshold.

Equations

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

@[implicit_reducible]

instance Discourse.AtIssueness.instDecidableIsProjective (d : ProjectivityDegree) (θ : ProjectivityThreshold) : Decidable (isProjective d θ)

Equations

• Discourse.AtIssueness.instDecidableIsProjective d θ = Discourse.AtIssueness.instDecidableIsProjective._aux_1 d θ

Classical Recovery

inductive Discourse.AtIssueness.AtIssuenessClassical : Type

Binary at-issueness, recoverable from gradient degree + threshold.

• atIssue : AtIssuenessClassical
• notAtIssue : AtIssuenessClassical

@[implicit_reducible]

instance Discourse.AtIssueness.instDecidableEqAtIssuenessClassical : DecidableEq AtIssuenessClassical

Equations

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

@[implicit_reducible]

instance Discourse.AtIssueness.instReprAtIssuenessClassical : Repr AtIssuenessClassical

Equations

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

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

Equations

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

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

Recover binary classification from gradient degree and threshold.

Equations

• Discourse.AtIssueness.toClassical d θ = if Discourse.AtIssueness.isAtIssue d θ then Discourse.AtIssueness.AtIssuenessClassical.atIssue else Discourse.AtIssueness.AtIssuenessClassical.notAtIssue

def Discourse.AtIssueness.defaultThreshold : AtIssuenessThreshold

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

Equations

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

def Discourse.AtIssueness.defaultProjectivityThreshold : ProjectivityThreshold

Default projectivity threshold at 0.5.

Equations

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

Anti-Correlation

structure Discourse.AtIssueness.GradientPair : Type

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

• atIssueness : ℚ
• projectivity : ℚ

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

Equations

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

@[implicit_reducible]

instance Discourse.AtIssueness.instReprGradientPair : Repr GradientPair

Equations

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

structure Discourse.AtIssueness.MonotoneAntiCorrelation : Type

A monotone-anti-correlation bundle: every pair ordering on at-issueness forces the reverse weak ordering on projectivity. This is a structural strengthening of the empirical Gradient Projection Principle of [TBD18], who establish a gradient negative correlation across content classes (with substantial within-class and item-level variance), not a deterministic monotone pairing across every stimulus pair. Suitable for analytical scenarios where the strict-monotone fragment is the object of study; not a faithful summary of the paper's empirical claim.

• pairs : List GradientPair
• 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

QUD Connection

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

Qualitative QUD-based at-issueness: content varying within QUD cells counts as at-issue ([Rob12]).

Equations

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

Boundedness

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

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

Equations

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

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

Equations

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

Smart Constructors

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

Construct a degree from [0, 100], normalizing to [0, 1].

Equations

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