PVC–DOC Structural Priming

@cite{haddican-tamminga-dendikken-wade-2026} @cite{dendikken-1995} @cite{halle-marantz-1993} @cite{johnson-1991} @cite{aarts-1989} @cite{bruening-2010a}

English Particle Verbs Prime Double Object Constructions in Production. Linguistic Inquiry. doi:10.1162/LING.a.558

Production priming experiment (N=238) testing whether PVCs prime DOCs.

Design

Sentence completion task. Two subdesigns (Table 1, p.7):

• Baseline: DOC vs PD primes → DOC/PD target completions
• PV: PVC vs non-PVC primes → DOC/PD target completions

PVC primes used particle-object order ("put down the vase") to control for surface string similarity with DOC targets (p.5).

Results

PVCs prime DOCs (β=0.296, p=.005). PVC and DOC primes do not differ in priming magnitude (β=−0.069, p=.503). Consistent with identical structural representations under the SC analysis.

Cross-references

• ArnoldEtAl2000: The same two constructions (dative alternation + particle placement) studied from a processing perspective — heaviness drives linearization while abstract structure drives priming.
• Phenomena.ArgumentStructure.DativeAlternation: Records both DOC and PD frames as grammatical — the precondition for the priming study.

structure HaddicanEtAl2026.PrimingContrast : Type

A priming contrast between two prime conditions.

• primeA : String
• primeB : String
• target : String
• aFavorsTarget : Bool
• significant : Bool

def HaddicanEtAl2026.instReprPrimingContrast.repr : PrimingContrast → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaddicanEtAl2026.instReprPrimingContrast : Repr PrimingContrast

Equations

• HaddicanEtAl2026.instReprPrimingContrast = { reprPrec := HaddicanEtAl2026.instReprPrimingContrast.repr }

@[implicit_reducible]

instance HaddicanEtAl2026.instBEqPrimingContrast : BEq PrimingContrast

Equations

• HaddicanEtAl2026.instBEqPrimingContrast = { beq := HaddicanEtAl2026.instBEqPrimingContrast.beq }

def HaddicanEtAl2026.instBEqPrimingContrast.beq : PrimingContrast → PrimingContrast → Bool

Equations

• One or more equations did not get rendered due to their size.
• HaddicanEtAl2026.instBEqPrimingContrast.beq x✝¹ x✝ = false

structure HaddicanEtAl2026.CellRate : Type

DOC production rate by prime condition. Table 1, p.7. Percentages are integers (e.g., 59 = 59%).

• condition : String
• docPct : ℕ
• pdPct : ℕ

@[implicit_reducible]

instance HaddicanEtAl2026.instReprCellRate : Repr CellRate

Equations

• HaddicanEtAl2026.instReprCellRate = { reprPrec := HaddicanEtAl2026.instReprCellRate.repr }

def HaddicanEtAl2026.instReprCellRate.repr : CellRate → ℕ → Std.Format

Equations

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

def HaddicanEtAl2026.instBEqCellRate.beq : CellRate → CellRate → Bool

Equations

• HaddicanEtAl2026.instBEqCellRate.beq { condition := a, docPct := a_1, pdPct := a_2 } { condition := b, docPct := b_1, pdPct := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• HaddicanEtAl2026.instBEqCellRate.beq x✝¹ x✝ = false

@[implicit_reducible]

instance HaddicanEtAl2026.instBEqCellRate : BEq CellRate

Equations

• HaddicanEtAl2026.instBEqCellRate = { beq := HaddicanEtAl2026.instBEqCellRate.beq }

Table 1 cell rates

def HaddicanEtAl2026.baseline_doc : CellRate

Equations

• HaddicanEtAl2026.baseline_doc = { condition := "DOC prime", docPct := 59, pdPct := 41 }

def HaddicanEtAl2026.baseline_pd : CellRate

Equations

• HaddicanEtAl2026.baseline_pd = { condition := "PD prime", docPct := 49, pdPct := 51 }

def HaddicanEtAl2026.pv_pvc : CellRate

Equations

• HaddicanEtAl2026.pv_pvc = { condition := "PVC prime", docPct := 58, pdPct := 42 }

def HaddicanEtAl2026.pv_nonpvc : CellRate

Equations

• HaddicanEtAl2026.pv_nonpvc = { condition := "non-PVC prime", docPct := 52, pdPct := 48 }

Regression contrasts

def HaddicanEtAl2026.baseline : PrimingContrast

Baseline replication: DOC primes boost DOC production relative to PD primes (β=0.569, SE=0.114, p<.001).

Equations

• HaddicanEtAl2026.baseline = { primeA := "DOC", primeB := "PD", target := "DOC", aFavorsTarget := true, significant := true }

def HaddicanEtAl2026.pvc_primes_doc : PrimingContrast

Key finding: PVC primes boost DOC production relative to non-PVC control primes (β=0.296, SE=0.105, p=.005).

Equations

• HaddicanEtAl2026.pvc_primes_doc = { primeA := "PVC", primeB := "non-PVC", target := "DOC", aFavorsTarget := true, significant := true }

def HaddicanEtAl2026.pvc_doc_equivalent : PrimingContrast

PVC and DOC primes do not differ in their priming of DOCs (β=−0.069, SE=0.104, p=.503; combined 2×4 model, n.9).

Equations

• HaddicanEtAl2026.pvc_doc_equivalent = { primeA := "PVC", primeB := "DOC", target := "DOC", aFavorsTarget := false, significant := false }

Verification theorems

theorem HaddicanEtAl2026.baseline_effect_direction : baseline.aFavorsTarget = true ∧ baseline.significant = true

DOC priming is strictly stronger than PD non-priming (baseline effect).

theorem HaddicanEtAl2026.pvc_effect : pvc_primes_doc.aFavorsTarget = true ∧ pvc_primes_doc.significant = true

PVC primes DO boost DOC production.

theorem HaddicanEtAl2026.pvc_doc_equivalence : pvc_doc_equivalent.significant = false

PVC and DOC primes yield equivalent magnitude — no significant difference.

Lexical items

def HaddicanEtAl2026.V_give : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.V_give = Minimalist.mkLeafPhon Minimalist.Cat.V [Minimalist.Cat.D, Minimalist.Cat.D] "give" 0

def HaddicanEtAl2026.V_lift : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.V_lift = Minimalist.mkLeafPhon Minimalist.Cat.V [Minimalist.Cat.D] "lift" 1

def HaddicanEtAl2026.DP_hsu : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.DP_hsu = Minimalist.mkLeafPhon Minimalist.Cat.D [] "Hsu" 2

def HaddicanEtAl2026.DP_book : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.DP_book = Minimalist.mkLeafPhon Minimalist.Cat.D [] "the book" 3

def HaddicanEtAl2026.Prt_up : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.Prt_up = Minimalist.mkLeafPhon Minimalist.Cat.P [] "up" 4

def HaddicanEtAl2026.Appl_h : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.Appl_h = Minimalist.mkLeafPhon Minimalist.Cat.Appl [Minimalist.Cat.V] "∅" 5

def HaddicanEtAl2026.P_to : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.P_to = Minimalist.mkLeafPhon Minimalist.Cat.P [Minimalist.Cat.D] "to" 6

def HaddicanEtAl2026.V_hammer : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.V_hammer = Minimalist.mkLeafPhon Minimalist.Cat.V [Minimalist.Cat.D] "hammer" 8

def HaddicanEtAl2026.DP_metal : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.DP_metal = Minimalist.mkLeafPhon Minimalist.Cat.D [] "the metal" 9

def HaddicanEtAl2026.AP_flat : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.AP_flat = Minimalist.mkLeafPhon Minimalist.Cat.A [] "flat" 10

def HaddicanEtAl2026.V_make : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.V_make = Minimalist.mkLeafPhon Minimalist.Cat.V [Minimalist.Cat.D] "make" 11

def HaddicanEtAl2026.DP_child : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.DP_child = Minimalist.mkLeafPhon Minimalist.Cat.D [] "the child" 12

def HaddicanEtAl2026.VP_laugh : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.VP_laugh = Minimalist.mkLeafPhon Minimalist.Cat.V [] "laugh" 13

theorem HaddicanEtAl2026.experimental_pvcs_in_inventory : (Phenomena.Constructions.ParticleVerbs.inventory.any fun (x : Phenomena.Constructions.ParticleVerbs.ParticleVerb) => x == Phenomena.Constructions.ParticleVerbs.lift_up) = true ∧ (Phenomena.Constructions.ParticleVerbs.inventory.any fun (x : Phenomena.Constructions.ParticleVerbs.ParticleVerb) => x == Phenomena.Constructions.ParticleVerbs.put_down) = true

Experimental PVC primes derive from the ParticleVerbs inventory.

def HaddicanEtAl2026.doc_appl_type : Minimalist.ApplType

The ApplP analysis uses a LOW applicative.

Equations

• HaddicanEtAl2026.doc_appl_type = Minimalist.ApplType.lowRecipient

Structural analyses

def HaddicanEtAl2026.doc_sc : Minimalist.SyntacticObject

DOC, Small Clause: [VP V [SC DP_goal DP_theme]]

Equations

• HaddicanEtAl2026.doc_sc = Minimalist.merge HaddicanEtAl2026.V_give (Minimalist.merge HaddicanEtAl2026.DP_hsu HaddicanEtAl2026.DP_book)

def HaddicanEtAl2026.doc_appl : Minimalist.SyntacticObject

DOC, Applicative (@cite{halle-marantz-1993}; @cite{bruening-2010a}): [ApplP DP_goal [Appl' Appl [VP V DP_theme]]]

Equations

• HaddicanEtAl2026.doc_appl = Minimalist.merge HaddicanEtAl2026.DP_hsu (Minimalist.merge HaddicanEtAl2026.Appl_h (Minimalist.merge HaddicanEtAl2026.V_give HaddicanEtAl2026.DP_book))

def HaddicanEtAl2026.pvc_sc : Minimalist.SyntacticObject

PVC, Small Clause (@cite{aarts-1989}; @cite{dendikken-1995}): [VP V [SC DP Prt]]

Equations

• HaddicanEtAl2026.pvc_sc = Minimalist.merge HaddicanEtAl2026.V_lift (Minimalist.merge HaddicanEtAl2026.DP_hsu HaddicanEtAl2026.Prt_up)

def HaddicanEtAl2026.pvc_complexPred : Minimalist.SyntacticObject

PVC, Complex predicate: [VP [V lift+up] DP]

Equations

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

def HaddicanEtAl2026.pd : Minimalist.SyntacticObject

PD, Prepositional dative (control): [VP [V' V DP_theme] [PP P DP_goal]]

Equations

• HaddicanEtAl2026.pd = Minimalist.merge (Minimalist.merge HaddicanEtAl2026.V_give HaddicanEtAl2026.DP_book) (Minimalist.merge HaddicanEtAl2026.P_to HaddicanEtAl2026.DP_hsu)

def HaddicanEtAl2026.transitive_control : Minimalist.SyntacticObject

Non-PVC transitive control: [VP V DP]

Equations

• HaddicanEtAl2026.transitive_control = Minimalist.merge HaddicanEtAl2026.V_lift HaddicanEtAl2026.DP_hsu

@cite{dendikken-1995} SC family

def HaddicanEtAl2026.resultative_sc : Minimalist.SyntacticObject

Resultative, Small Clause: [VP V [SC DP AP]]

Equations

• HaddicanEtAl2026.resultative_sc = Minimalist.merge HaddicanEtAl2026.V_hammer (Minimalist.merge HaddicanEtAl2026.DP_metal HaddicanEtAl2026.AP_flat)

def HaddicanEtAl2026.causative_sc : Minimalist.SyntacticObject

Causative, Small Clause: [VP V [SC DP VP]]

Equations

• HaddicanEtAl2026.causative_sc = Minimalist.merge HaddicanEtAl2026.V_make (Minimalist.merge HaddicanEtAl2026.DP_child HaddicanEtAl2026.VP_laugh)

Explicit shapes

theorem HaddicanEtAl2026.doc_sc_shape : doc_sc.shape = HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝)

DOC small clause: [VP V [SC DP DP]] — three leaves in a right-branching shape.

theorem HaddicanEtAl2026.doc_appl_shape : doc_appl.shape = HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝))

DOC-Applicative: [ApplP DP_goal [Appl' Appl [VP V DP_theme]]] — 4 leaves.

theorem HaddicanEtAl2026.pvc_sc_shape : pvc_sc.shape = HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝)

theorem HaddicanEtAl2026.pvc_complexPred_shape : pvc_complexPred.shape = HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝

theorem HaddicanEtAl2026.pd_shape : pd.shape = HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝)

theorem HaddicanEtAl2026.transitive_control_shape : transitive_control.shape = HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝

theorem HaddicanEtAl2026.resultative_sc_shape : resultative_sc.shape = HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝)

theorem HaddicanEtAl2026.causative_sc_shape : causative_sc.shape = HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝)

Structural isomorphism

structurallyIsomorphic x y is Prop-valued (substrate change at 0.230.865; revived as x.shape = y.shape); previously Bool-valued on planar TraceTree. Decidable, so decide works.

theorem HaddicanEtAl2026.sc_doc_pvc_isomorphic : Minimalist.structurallyIsomorphic doc_sc pvc_sc

SC-DOC and SC-PVC share tree shape.

theorem HaddicanEtAl2026.appl_complexPred_not_isomorphic : ¬Minimalist.structurallyIsomorphic doc_appl pvc_complexPred

ApplP-DOC and ComplexPred-PVC have different shapes.

theorem HaddicanEtAl2026.sc_appl_doc_not_isomorphic : ¬Minimalist.structurallyIsomorphic doc_sc doc_appl

SC-DOC differs from ApplP-DOC.

theorem HaddicanEtAl2026.sc_doc_pd_not_isomorphic : ¬Minimalist.structurallyIsomorphic doc_sc pd

SC-DOC differs from PD.

theorem HaddicanEtAl2026.sc_pvc_pd_not_isomorphic : ¬Minimalist.structurallyIsomorphic pvc_sc pd

SC-PVC differs from PD.

theorem HaddicanEtAl2026.control_doc_not_isomorphic : ¬Minimalist.structurallyIsomorphic transitive_control doc_sc

The non-PVC transitive control has a different shape from SC-DOC.

theorem HaddicanEtAl2026.control_matches_complexPred : Minimalist.structurallyIsomorphic transitive_control pvc_complexPred

The non-PVC control has the SAME shape as the complex predicate PVC.

theorem HaddicanEtAl2026.sc_unique_among_haddican_analyses : Minimalist.structurallyIsomorphic doc_sc pvc_sc ∧ ¬Minimalist.structurallyIsomorphic doc_sc doc_appl ∧ ¬Minimalist.structurallyIsomorphic doc_sc pvc_complexPred ∧ ¬Minimalist.structurallyIsomorphic doc_sc pd ∧ ¬Minimalist.structurallyIsomorphic doc_appl pvc_sc ∧ ¬Minimalist.structurallyIsomorphic doc_appl pvc_complexPred ∧ ¬Minimalist.structurallyIsomorphic doc_appl pd ∧ ¬Minimalist.structurallyIsomorphic pvc_sc pvc_complexPred ∧ ¬Minimalist.structurallyIsomorphic pvc_sc pd ∧ ¬Minimalist.structurallyIsomorphic pvc_complexPred pd

SC is the unique source of DOC/PVC tree-shape isomorphism.

Den Dikken SC family isomorphism

theorem HaddicanEtAl2026.sc_family_same_shape : doc_sc.shape = pvc_sc.shape ∧ doc_sc.shape = resultative_sc.shape ∧ doc_sc.shape = causative_sc.shape

The SC family shares a single tree shape.

theorem HaddicanEtAl2026.sc_family_all_isomorphic : Minimalist.structurallyIsomorphic doc_sc pvc_sc ∧ Minimalist.structurallyIsomorphic doc_sc resultative_sc ∧ Minimalist.structurallyIsomorphic doc_sc causative_sc ∧ Minimalist.structurallyIsomorphic pvc_sc resultative_sc ∧ Minimalist.structurallyIsomorphic pvc_sc causative_sc ∧ Minimalist.structurallyIsomorphic resultative_sc causative_sc

All four SC constructions are pairwise isomorphic.

theorem HaddicanEtAl2026.sc_family_all_differ_from_pd : ¬Minimalist.structurallyIsomorphic pvc_sc pd ∧ ¬Minimalist.structurallyIsomorphic resultative_sc pd ∧ ¬Minimalist.structurallyIsomorphic causative_sc pd

None of the SC family members are isomorphic with PD.

SC family categorization

def HaddicanEtAl2026.pvc_category : Minimalist.SCPredCategory

Equations

• HaddicanEtAl2026.pvc_category = Minimalist.SCPredCategory.P

def HaddicanEtAl2026.doc_category : Minimalist.SCPredCategory

Equations

• HaddicanEtAl2026.doc_category = Minimalist.SCPredCategory.P

def HaddicanEtAl2026.resultative_category : Minimalist.SCPredCategory

Equations

• HaddicanEtAl2026.resultative_category = Minimalist.SCPredCategory.A

def HaddicanEtAl2026.causative_category : Minimalist.SCPredCategory

Equations

• HaddicanEtAl2026.causative_category = Minimalist.SCPredCategory.V

def HaddicanEtAl2026.copular_category : Minimalist.SCPredCategory

Equations

• HaddicanEtAl2026.copular_category = Minimalist.SCPredCategory.N

theorem HaddicanEtAl2026.doc_pvc_share_P : doc_category = pvc_category

DOC and PVC share SC predicate category P.

theorem HaddicanEtAl2026.sc_family_covers_all_categories : pvc_category = Minimalist.SCPredCategory.P ∧ resultative_category = Minimalist.SCPredCategory.A ∧ causative_category = Minimalist.SCPredCategory.V ∧ copular_category = Minimalist.SCPredCategory.N

The SC family spans all four lexical categories {A, N, P, V}.

Nested SC for DOC

def HaddicanEtAl2026.doc_nested : Minimalist.SyntacticObject

Nested SC DOC: give [SC book [PP to Hsu]].

Equations

• HaddicanEtAl2026.doc_nested = Minimalist.merge HaddicanEtAl2026.V_give (Minimalist.merge HaddicanEtAl2026.DP_book (Minimalist.merge HaddicanEtAl2026.P_to HaddicanEtAl2026.DP_hsu))

theorem HaddicanEtAl2026.doc_nested_shape : doc_nested.shape = HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝))

theorem HaddicanEtAl2026.doc_nested_not_flat : ¬Minimalist.structurallyIsomorphic doc_nested doc_sc

theorem HaddicanEtAl2026.doc_nested_matches_appl : Minimalist.structurallyIsomorphic doc_nested doc_appl

@cite{bruening-2021}: process-level isomorphism

doc_bruening below is a SyntacticObject witness of Bruening's V+P amalgam analysis. The lexical-fragment side of the same paper — Bruening's classification of implicit-argument behavior across ~43 ditransitive verbs (Table 56) — is formalized in Phenomena/ArgumentStructure/Studies/Bruening2021.lean. The bruening_give_field_consistent theorem below ties this structural witness to that lexical-fragment side.

def HaddicanEtAl2026.doc_bruening : Minimalist.SyntacticObject

Equations

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

def HaddicanEtAl2026.pvc_bruening : Minimalist.SyntacticObject

Equations

• HaddicanEtAl2026.pvc_bruening = HaddicanEtAl2026.pvc_complexPred

theorem HaddicanEtAl2026.doc_bruening_shape : doc_bruening.shape = HaddicanEtAl2026.leafShape✝ * (HaddicanEtAl2026.leafShape✝ * HaddicanEtAl2026.leafShape✝)

theorem HaddicanEtAl2026.bruening_shapes_differ : ¬Minimalist.structurallyIsomorphic doc_bruening pvc_bruening

theorem HaddicanEtAl2026.bruening_both_use_incorporation : (∃ tok ∈ Multiset.filterMap Minimalist.SyntacticObject.getLIToken doc_bruening.subtrees, tok.item.isComplex = true) ∧ ∃ tok ∈ Multiset.filterMap Minimalist.SyntacticObject.getLIToken pvc_bruening.subtrees, tok.item.isComplex = true

Both Bruening structures use a complex (incorporated) head leaf. The original theorem (planar substrate) projected the head via match doc_bruening with | .node (.leaf tok) _ => tok.item.isComplex, which doesn't reduce under MCB nonplanar SOs (children of .mul are unordered).

The claim itself remains true and verifiable: both DOC and PVC structures contain a complex (head-incorporated) LIToken among their subtrees. Reformulate as a Multiset-membership claim:

(∃ tok ∈ doc_bruening.subtrees.filterMap getLIToken, tok.item.isComplex) ∧
(∃ tok ∈ pvc_bruening.subtrees.filterMap getLIToken, tok.item.isComplex)

TODO Phase 2 / polish: prove the Multiset-version directly, or re-derive from a head-function-aware headLIToken : SO → Option LIToken once Phase 2 substrate lands.

theorem HaddicanEtAl2026.bruening_doc_matches_sc_doc : Minimalist.structurallyIsomorphic doc_bruening doc_sc

Bridge to Bruening 2021 lexical fragment

doc_bruening above is a SyntacticObject witness; this theorem ties it to the corresponding lexical-fragment entry in Bruening2021.lean, ensuring the verb we structurally treat as "give-in-DOC" is also the verb whose implicit-argument profile licenses Bruening's Table (56) classification. If Verbal.lean ever moves give to a different complement type or implicit-arg profile, this bridge fails — alerting both files.

theorem HaddicanEtAl2026.bruening_give_field_consistent : Fragments.English.Predicates.Verbal.give.complementType = Semantics.Lexical.ComplementType.np_np ∧ Fragments.English.Predicates.Verbal.give.altComplementType = some Semantics.Lexical.ComplementType.np_pp ∧ Fragments.English.Predicates.Verbal.give.implicitObj = some Semantics.Lexical.ImplicitInterp.indef ∧ Fragments.English.Predicates.Verbal.give.implicitGoal = some Semantics.Lexical.ImplicitInterp.def

Bridge to experimental data

theorem HaddicanEtAl2026.sc_predictions : Minimalist.structurallyIsomorphic doc_sc pvc_sc ∧ ¬Minimalist.structurallyIsomorphic doc_sc pd

The SC analysis predicts DOC/PVC isomorphism and DOC/PD non-isomorphism.

theorem HaddicanEtAl2026.appl_complexPred_no_isomorphism : ¬Minimalist.structurallyIsomorphic doc_appl pvc_complexPred

The ApplP + ComplexPred combination predicts DOC/PVC non-isomorphism.

theorem HaddicanEtAl2026.sc_predicts_equal_magnitude : pvc_doc_equivalent.significant = false ∧ doc_sc.shape = pvc_sc.shape

PVC priming magnitude equals DOC priming magnitude, as SC predicts.

theorem HaddicanEtAl2026.complexPred_fails_at_control : pvc_primes_doc.significant = true ∧ Minimalist.structurallyIsomorphic pvc_complexPred transitive_control

The complex predicate PVC analysis cannot explain the priming asymmetry.

IsSmallClause companion-predicate witnesses

The flat encodings (pvc_sc, doc_sc, resultative_sc, causative_sc) name the whole [VP V SC] constituent — the SC itself is the right child. We characterise the inner SCs against the IsSmallClause companion predicate (SmallClause.lean).

Three of the four families satisfy the predicate; DOC's flat DP–DP encoding does not. This surfaces a real subtlety: Haddican et al. (2026) explicitly say (p.2) "we set aside details of the internal structure of the small clause", and the flat DP–DP shape is the deliberate simplification. The richer DOC encoding (with BE+P decomposition / Predicate Inversion) in Phenomena/ArgumentStructure/Studies/Dendikken1995 does satisfy IsSmallClause at every nested SC layer.

theorem HaddicanEtAl2026.pvc_sc_inner_isSmallClause : Minimalist.IsSmallClause (Minimalist.merge DP_hsu Prt_up)

Phase 1.0 caveat: IsSmallClause is noncomputable because it routes through outerCat/headCat, which are Phase 1.0 placeholders via Quot.out on the FreeCommMagma carrier. Concrete-instance checks via decide fail at the kernel-reduction step. TODO Phase 2: once LCA-based head selection lands, restore by decide.

theorem HaddicanEtAl2026.resultative_sc_inner_isSmallClause : Minimalist.IsSmallClause (Minimalist.merge DP_metal AP_flat)

theorem HaddicanEtAl2026.causative_sc_inner_isSmallClause : Minimalist.IsSmallClause (Minimalist.merge DP_child VP_laugh)

theorem HaddicanEtAl2026.doc_sc_flat_inner_not_smallClause : ¬Minimalist.IsSmallClause (Minimalist.merge DP_hsu DP_book)

Diagnostic: the flat DP–DP DOC encoding does NOT satisfy IsSmallClause — neither child is in the SC predicate set {P,A,V,N}. Both children are DPs (head category D). The companion predicate surfaces the simplification — the encoding is correct for the priming argument but incomplete as a structural SC analysis; den Dikken's BE+P decomposition supplies the missing predicate.