Generalizations.Projectivity — cross-paper prediction target

The Gradient Projection Principle of [TBD18] — content projects to the extent that it is not at-issue — predicts a per-expression projectivity from its at-issueness. This file is the theory-neutral pool against which rival accounts of that relationship are run.

The empirical generalisation (projectivity is gradient and tracks not-at-issueness across triggers) predates any one formal account and spans ≥ 2 papers contributing generated Data.Examples rows ([TBD18]: 9 + 12 English expressions; [SB24]: occasion + psychological verbs in German), with ≥ 2 rival accounts consuming the ProjectionAccount signature in their study files (gppProjection and pottsProjection in Studies/TonhauserBeaverDegen2018).

Main declarations

• ProjectionAccount — the prediction signature any account implements: given a content's at-issueness, predict its projectivity (Rat01 → Rat01).
• ProjectionDatum — a typed observed datum (projectivity, atIssueness), lifted from a paper-anchored LinguisticExample by fromExample.
• allData — the pooled test set: every projectivity row from the contributing papers' generated Examples.all.
• predictionError / predictsWithin — score an account against an observation.

Implementation notes

The means are continuous (proportions in [0, 1]), so an account is run over allData by computation; the kernel-checkable content is each account's systematic error, proved in the study files (string-keyed paperFeatures and ℚ comparison do not reduce in the kernel). Papers may store either atIssueness or notAtIssueness in paperFeatures; readAtIssueness normalises both to at-issueness (the accounts' input). Import rule (Core + Data only): accounts and divergence theorems live in the consuming study files.

Prediction signature

@[reducible, inline]

abbrev Generalizations.Projectivity.ProjectionAccount : Type

A theory of projection: predict a content's projectivity from its at-issueness. Rival accounts (gppProjection, pottsProjection) live in the study files and are run against allData.

Equations

• Generalizations.Projectivity.ProjectionAccount = (Core.Order.Rat01 → Core.Order.Rat01)

structure Generalizations.Projectivity.ProjectionDatum : Type

An observed datum: mean projectivity and at-issueness for one expression, with its originating SourceRef.

• expression : String
• projectivity : Core.Order.Rat01
• atIssueness : Core.Order.Rat01
• source : Data.Examples.SourceRef

def Generalizations.Projectivity.instReprProjectionDatum.repr : ProjectionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Generalizations.Projectivity.instReprProjectionDatum : Repr ProjectionDatum

Equations

• Generalizations.Projectivity.instReprProjectionDatum = { reprPrec := Generalizations.Projectivity.instReprProjectionDatum.repr }

def Generalizations.Projectivity.ProjectionDatum.notAtIssueness (d : ProjectionDatum) : Core.Order.Rat01

Not-at-issueness is the complement of at-issueness — the quantity the GPP equates with projectivity.

Equations

• d.notAtIssueness = d.atIssueness.compl

LinguisticExample adapter

def Generalizations.Projectivity.parsePercent (s : String) : Option Core.Order.Rat01

Parse a percent-integer string (e.g. "96") into a Rat01; none if non-numeric or out of range.

Equations

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

def Generalizations.Projectivity.readAtIssueness (pf : List (String × String)) : Option Core.Order.Rat01

Read at-issueness from paperFeatures: directly from the atIssueness key, or as the complement of notAtIssueness.

Equations

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

def Generalizations.Projectivity.fromExample (e : Data.Examples.LinguisticExample) : Option ProjectionDatum

Lift a LinguisticExample to a ProjectionDatum via its expression, projectivity, and (atIssueness or notAtIssueness) keys; none if any is missing.

Equations

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

Pool

def Generalizations.Projectivity.allData : List ProjectionDatum

The pooled cross-paper projection data. Each rival ProjectionAccount is run against this list in the study files.

Equations

• Generalizations.Projectivity.allData = List.filterMap Generalizations.Projectivity.fromExample (TonhauserBeaverDegen2018.Examples.all ++ SolstadBott2024.Examples.all)

Scoring

def Generalizations.Projectivity.predictionError (acc : ProjectionAccount) (d : ProjectionDatum) : ℚ

An account's absolute error on an observation: the gap between its predicted projectivity (from the observed at-issueness) and the observed projectivity.

Equations

• Generalizations.Projectivity.predictionError acc d = |↑(acc d.atIssueness) - ↑d.projectivity|

def Generalizations.Projectivity.predictsWithin (ε : ℚ) (acc : ProjectionAccount) (d : ProjectionDatum) : Prop

An account predicts an observation within tolerance ε.

Equations

• Generalizations.Projectivity.predictsWithin ε acc d = (Generalizations.Projectivity.predictionError acc d ≤ ε)

@[implicit_reducible]

instance Generalizations.Projectivity.instDecidablePredictsWithin (ε : ℚ) (acc : ProjectionAccount) (d : ProjectionDatum) : Decidable (predictsWithin ε acc d)

Equations

• Generalizations.Projectivity.instDecidablePredictsWithin ε acc d = Generalizations.Projectivity.instDecidablePredictsWithin._aux_1 ε acc d