φ-probes: the φ-feature specialization of Probe

[Pre14] [BR03]

The φ-instantiation of the general Probe core (Probe/Basic.lean): probes over Agreement.Cells, relativized by the sought feature (Probe.Target, Phi/Geometry.lean). This is [Pre14]'s participant-relativized person probe and the Person Licensing Condition built on it.

Main declarations

• Agreement.Cell.visibleTo — a cell bears the feature a target seeks.
• Probe.Target.toProbe — a target's denotation as a Probe over φ-cells.
• PLC — the Person Licensing Condition over φ-bearing goal tokens.

def Agreement.Cell.visibleTo (c : Cell) (t : Minimalist.Probe.Target) : Bool

Visibility of a φ-cell to a relativized probe: the cell bears the feature the probe seeks (probeVisible, Phi/Geometry.lean).

Equations

• c.visibleTo t = Minimalist.probeVisible t c.toPerson c.isPlural

def Minimalist.Probe.Target.toProbe (t : Target) : Probe Agreement.Cell

The Probe a Probe.Target denotes: relativized to the sought feature, over φ-cells (π⁰ = Probe.Target.participant.toProbe).

Equations

• t.toProbe = Minimalist.Probe.ofVis fun (x : Agreement.Cell) => x.visibleTo t

def Minimalist.PLC {α : Type u_1} (cellOf : α → Agreement.Cell) (goals : List α) : Prop

The Person Licensing Condition ([BR03], [Pre14]): every [participant]-bearing goal is licensed by the person probe's search. This single-cycle, search-only rendering omits [BR03]'s F-licensing route and multi-cycle repairs (see BejarRezac2003.PLCOk).

Equations

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

@[implicit_reducible]

instance Minimalist.instDecidablePLCOfDecidableEq {α : Type u_1} [DecidableEq α] (cellOf : α → Agreement.Cell) (goals : List α) : Decidable (PLC cellOf goals)

Equations

• Minimalist.instDecidablePLCOfDecidableEq cellOf goals = Minimalist.instDecidablePLCOfDecidableEq._aux_1 cellOf goals