Probe: relativized search over a goal sequence

[BR03] [Pre14]

A Probe α is the theory-agnostic relativized-search kernel over a goal sequence List α. It bundles what the probe sees (vis — the search halts at the first visible goal) and what it can value there (act — a visible but inactive goal absorbs the probe, [Dea24]-style interaction vs. satisfaction). Probe specifications — relativized targets, satisfaction conditions, horizon profiles, articulated/dynamic probes — denote a Probe by a toProbe-map rather than re-implementing search.

This models a probe's search (locality, intervention, satisfaction); feature transmission — what a successful Agree copies/shares/values — is a separate concern (Agree.applyAgree). This is the general core: the φ-specialization is in Probe/Phi.lean, the satisfaction spec in Probe/Satisfaction.lean, Keine's horizon spec in Probe/Profile.lean.

Main declarations

• Probe, Probe.ofVis, Probe.indiscriminate — the bundle and constructors.
• Probe.search / Probe.agree — first visible goal / that goal if active.
• Probe.outcome, Probe.Outcome — valued vs. unvalued.
• Probe.Licensed, Probe.AllLicensed, allLicensed_iff — one search licenses at most one goal (the Person Licensing Condition's engine).
• Probe.cascade — ordered probe sequence, first with output wins.

toProbe specs denoting a Probe: Probe.Target.toProbe, SatisfactionCond.toProbe, Probe.Profile.toProbe, Probe.Articulated.toProbes, Deal2024.ProbeState.probe.

TODO

• Transmission axis. Probe models search, not what a successful Agree copies/shares/values. A Probe.agreeWith : Probe α → (α → V) → List α → Σ (Σ = Option V / List V for [Hir01] Multiple Agree / a shared-occurrence type for Frampton-Gutmann feature-sharing) would fold applyAgree, Multiple Agree, Agree-Link/Copy ([AN12]), and case-by-Agree into one extension.
• Upward Agree. Search is downward (c-command, search_eq_some_iff_closest); add a direction parameter for Bjorkman & Zeijlstra (2019)-style upward Agree.
• Preorder (Probe α) by pointwise vis-refinement, so outcome_valued_mono / Deal2024.probe_vis_antitone become order facts.
• HalpertHammerly2026.agreementClass: re-stipulated relativized search; should be two Probe searches with a _eq_derived theorem.

structure Minimalist.Probe (α : Type u_2) : Type u_2

A probe over goals of type α: relativized search (vis) with an activity gate (act).

• vis : α → Bool

  A visible goal halts the search ([Dea24] interaction).

• act : α → Bool

  A visible but inactive goal absorbs the probe without valuing it ([Dea24] satisfaction); defaults to always-active.

inductive Minimalist.Probe.Outcome : Type

The outcome of an obligatory probing operation ([Pre14] Ch. 5): valued iff the search found a goal. An unvalued outcome is failed Agree — under the obligatory-operations model it is tolerated (no crash) and spells out as the Elsewhere/default entry; study files read it off Probe.outcome.

• valued : Outcome

  The search found a goal.

• unvalued : Outcome

  The search found no goal.

@[implicit_reducible]

instance Minimalist.Probe.instDecidableEqOutcome : DecidableEq Outcome

Equations

• Minimalist.Probe.instDecidableEqOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Minimalist.Probe.instReprOutcome : Repr Outcome

Equations

• Minimalist.Probe.instReprOutcome = { reprPrec := Minimalist.Probe.instReprOutcome.repr }

def Minimalist.Probe.instReprOutcome.repr : Outcome → ℕ → Std.Format

Equations

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

def Minimalist.Probe.ofVis {α : Type u_1} (vis : α → Bool) : Probe α

A probe with a visibility condition and no activity restriction.

Equations

• Minimalist.Probe.ofVis vis = { vis := vis }

def Minimalist.Probe.indiscriminate {α : Type u_1} : Probe α

The indiscriminate probe: sees every goal, so bare minimality delivers the closest one ([Hal12]'s L⁰).

Equations

• Minimalist.Probe.indiscriminate = Minimalist.Probe.ofVis fun (x : α) => true

Search

def Minimalist.Probe.search {α : Type u_1} (p : Probe α) (goals : List α) : Option α

The goal a probe finds in an ordered goal sequence: the first goal visible to it, skipping invisible ones.

Equations

• p.search goals = List.find? p.vis goals

def Minimalist.Probe.agree {α : Type u_1} (p : Probe α) (goals : List α) : Option α

Search then Agree: the found goal, if it passes the activity condition. A visible inactive goal absorbs the probe.

Equations

• p.agree goals = Option.filter p.act (p.search goals)

@[simp]

theorem Minimalist.Probe.search_eq_none_iff {α : Type u_1} {p : Probe α} {goals : List α} : p.search goals = none ↔ ∀ (a : α), a ∈ goals → ¬p.vis a = true

A probe finds nothing iff no goal is visible to it.

theorem Minimalist.Probe.mem_of_search_eq_some {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.search goals = some a) : a ∈ goals

The found goal is a member of the sequence.

theorem Minimalist.Probe.visible_of_search_eq_some {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.search goals = some a) : p.vis a = true

The found goal is visible to the probe.

theorem Minimalist.Probe.search_pair_of_imp {α : Type u_1} {p : Probe α} {a b : α} (h : p.vis b = true → p.vis a = true) : p.search [a, b] = if p.vis a = true then some a else none

Over a two-goal sequence whose lower goal's visibility entails the higher's, the search lands on the higher goal if anywhere — the kernel of "gluttony/competition only in inverse configurations" ([CK21]) and of highest-only licensing ([Hal12]).

theorem Minimalist.Probe.agree_eq_some_iff {α : Type u_1} {p : Probe α} {goals : List α} {a : α} : p.agree goals = some a ↔ p.search goals = some a ∧ p.act a = true

The probe Agrees with a iff the search finds a and a is active.

theorem Minimalist.Probe.agree_eq_none_of_inactive {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.search goals = some a) (ha : p.act a = false) : p.agree goals = none

An inactive closest goal absorbs the probe: match without Agree.

@[simp]

theorem Minimalist.Probe.search_nil {α : Type u_1} {p : Probe α} : p.search [] = none

theorem Minimalist.Probe.agree_le_search {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.agree goals = some a) : p.search goals = some a

Satisfaction refines interaction: what the probe Agrees with, it found.

theorem Minimalist.Probe.agree_eq_search_of_act {α : Type u_1} {p : Probe α} {goals : List α} (h : ∀ (a : α), p.act a = true) : p.agree goals = p.search goals

When every goal is active, Agree coincides with search — the act gate is degenerate for ofVis-built probes.

theorem Minimalist.Probe.agree_eq_none_iff {α : Type u_1} {p : Probe α} {goals : List α} : p.agree goals = none ↔ ¬∃ (a : α), p.search goals = some a ∧ p.act a = true

theorem Minimalist.Probe.search_eq_some_iff_closest {α : Type u_1} {p : Probe α} {goals : List α} {a : α} : p.search goals = some a ↔ p.vis a = true ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), goals = l₁ ++ a :: l₂ ∧ ∀ (b : α), b ∈ l₁ → (!p.vis b) = true

Locality as list search: the probe finds a iff a is visible and every earlier goal is invisible (no intervener).

Outcomes ([Pre14] Ch. 5)

def Minimalist.Probe.outcome {α : Type u_1} (p : Probe α) (goals : List α) : Outcome

The outcome of an obligatory probing operation over a goal sequence: valued iff the search finds a goal.

Equations

• p.outcome goals = if (p.search goals).isSome = true then Minimalist.Probe.Outcome.valued else Minimalist.Probe.Outcome.unvalued

theorem Minimalist.Probe.outcome_eq_valued_iff_isSome {α : Type u_1} {p : Probe α} {goals : List α} : p.outcome goals = Outcome.valued ↔ (p.search goals).isSome = true

The probe is valued iff the search finds a goal.

theorem Minimalist.Probe.outcome_eq_unvalued_iff_eq_none {α : Type u_1} {p : Probe α} {goals : List α} : p.outcome goals = Outcome.unvalued ↔ p.search goals = none

The probe ends unvalued iff the search comes back empty.

@[simp]

theorem Minimalist.Probe.outcome_eq_valued_iff {α : Type u_1} {p : Probe α} {goals : List α} : p.outcome goals = Outcome.valued ↔ ∃ (a : α), a ∈ goals ∧ p.vis a = true

The probe is valued iff some goal is visible to it.

@[simp]

theorem Minimalist.Probe.outcome_eq_unvalued_iff {α : Type u_1} {p : Probe α} {goals : List α} : p.outcome goals = Outcome.unvalued ↔ ∀ (a : α), a ∈ goals → ¬p.vis a = true

The probe ends unvalued iff no goal is visible to it.

theorem Minimalist.Probe.outcome_valued_mono {α : Type u_1} {p : Probe α} {goals : List α} {q : Probe α} (h : ∀ (a : α), a ∈ goals → p.vis a = true → q.vis a = true) : p.outcome goals = Outcome.valued → q.outcome goals = Outcome.valued

Widening visibility can only keep a probe valued: if p is valued and q sees everything p sees (among goals), so is q. The substrate home of [Dea24]-style narrowing (Deal2024's probe_vis_antitone is the contrapositive on a probe family).

Licensing

def Minimalist.Probe.Licensed {α : Type u_1} (p : Probe α) (goals : List α) (a : α) : Prop

A goal is licensed by a probe iff the probe's single search reaches it ([BR03]: licensing is an Agree relation with the probe).

Equations

• p.Licensed goals a = (p.search goals = some a)

@[implicit_reducible]

instance Minimalist.Probe.instDecidableLicensedOfDecidableEq {α : Type u_1} [DecidableEq α] (p : Probe α) (goals : List α) (a : α) : Decidable (p.Licensed goals a)

Equations

• p.instDecidableLicensedOfDecidableEq goals a = Minimalist.Probe.instDecidableLicensedOfDecidableEq._aux_1 p goals a

theorem Minimalist.Probe.Licensed.unique {α : Type u_1} {p : Probe α} {goals : List α} {a b : α} (ha : p.Licensed goals a) (hb : p.Licensed goals b) : a = b

One search licenses at most one goal.

theorem Minimalist.Probe.licensed_iff_closest {α : Type u_1} {p : Probe α} {goals : List α} {a : α} : p.Licensed goals a ↔ p.vis a = true ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), goals = l₁ ++ a :: l₂ ∧ ∀ (b : α), b ∈ l₁ → (!p.vis b) = true

Licensing is being the closest visible goal: no matching goal intervenes (search_eq_some_iff_closest in the licensing API).

theorem Minimalist.Probe.Licensed.mem {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.Licensed goals a) : a ∈ goals

A licensed goal is a member of the sequence.

theorem Minimalist.Probe.Licensed.vis {α : Type u_1} {p : Probe α} {goals : List α} {a : α} (h : p.Licensed goals a) : p.vis a = true

A licensed goal is visible to the probe.

theorem Minimalist.Probe.indiscriminate_licensed_iff {α : Type u_1} {goals : List α} {a : α} : indiscriminate.Licensed goals a ↔ goals.head? = some a

Licensing by the indiscriminate probe is being the structurally closest goal — bare minimality, [Hal12]'s L⁰.

def Minimalist.Probe.AllLicensed {α : Type u_1} (p : Probe α) (needs : α → Bool) (goals : List α) : Prop

Every goal that needs licensing is licensed by the probe's search. Which goals need licensing (needs) and which the probe sees (p.vis) come apart in general: [Hal12]'s Zulu L⁰ sees every goal (augmented nominals intervene) while only augmentless nominals need it. Feature-relativized probes are the diagonal p.AllLicensed p.vis — the probe sees exactly the needy ([BR03]'s π as relativized by [Pre14]).

Equations

• p.AllLicensed needs goals = ∀ (a : α), a ∈ goals → needs a = true → p.Licensed goals a

@[implicit_reducible]

instance Minimalist.Probe.instDecidableAllLicensedOfDecidableEq {α : Type u_1} [DecidableEq α] (p : Probe α) (needs : α → Bool) (goals : List α) : Decidable (p.AllLicensed needs goals)

Equations

• p.instDecidableAllLicensedOfDecidableEq needs goals = Minimalist.Probe.instDecidableAllLicensedOfDecidableEq._aux_1 p needs goals

theorem Minimalist.Probe.allLicensed_iff {α : Type u_1} {vis : α → Bool} {goals : List α} : (ofVis vis).AllLicensed vis goals ↔ ∀ (a : α), a ∈ goals → ∀ (b : α), b ∈ goals → vis a = true → vis b = true → a = b

On the diagonal (probe relativized to exactly the needy), all needy goals are licensed iff the visible goals are subsingleton: one search, one Agree relation, at most one licensee — the fact behind [Pre14]'s AF person restriction. (The off-diagonal variant of the same one-licensee engine drives [BR03]'s PCC — Studies/BejarRezac2003.lean.)

theorem Minimalist.Probe.allLicensed_iff_subsingleton {α : Type u_1} {vis : α → Bool} {goals : List α} : (ofVis vis).AllLicensed vis goals ↔ {a : α | a ∈ goals ∧ vis a = true}.Subsingleton

allLicensed_iff in Set.Subsingleton form, for mathlib-API discoverability.

theorem Minimalist.Probe.indiscriminate_allLicensed_iff {α : Type u_1} {needs : α → Bool} {goals : List α} : indiscriminate.AllLicensed needs goals ↔ ∀ (a : α), a ∈ goals → needs a = true → goals.head? = some a

Licensing by the indiscriminate probe pins every needy goal to the head of the sequence — the highest-element condition ([Hal12]: an augmentless nominal must be the highest nominal in its vP).

Cascades

def Minimalist.Probe.cascade {α : Type u_1} (ps : List (Probe α)) (goals : List α) : Option α

The goal an ordered sequence of probes delivers: the first probe's finding, else the next's, and so on — Probe.search at the goal level composed with List.findSome? at the probe level. This is also the single-slot morphological competition: the first probe with output wins the slot ([Pre14] §4.4: π⁰'s clitic beats #⁰'s exponent beats nothing).

Equations

• Minimalist.Probe.cascade ps goals = List.findSome? (fun (x : Minimalist.Probe α) => x.search goals) ps

@[simp]

theorem Minimalist.Probe.cascade_eq_none_iff {α : Type u_1} {goals : List α} {ps : List (Probe α)} : cascade ps goals = none ↔ ∀ (q : Probe α), q ∈ ps → ∀ (a : α), a ∈ goals → ¬q.vis a = true

A cascade delivers nothing iff no goal is visible to any probe.

theorem Minimalist.Probe.cascade_cons {α : Type u_1} {goals : List α} {ps : List (Probe α)} {q : Probe α} : cascade (q :: ps) goals = (q.search goals <|> cascade ps goals)

Unfold one probe of the cascade.

@[simp]

theorem Minimalist.Probe.cascade_nil {α : Type u_1} {goals : List α} : cascade [] goals = none

@[simp]

theorem Minimalist.Probe.cascade_singleton {α : Type u_1} {goals : List α} {q : Probe α} : cascade [q] goals = q.search goals

theorem Minimalist.Probe.cascade_append {α : Type u_1} {goals : List α} {ps qs : List (Probe α)} : cascade (ps ++ qs) goals = (cascade ps goals <|> cascade qs goals)

cascade is a monoid map (List (Probe α), ++) → (Option α, <|>): the single-slot competition runs the left probes, then the right.

theorem Minimalist.Probe.exists_licensed_of_cascade_eq_some {α : Type u_1} {goals : List α} {ps : List (Probe α)} {a : α} (h : cascade ps goals = some a) : ∃ (q : Probe α), q ∈ ps ∧ q.Licensed goals a

The cascade's goal is licensed by one of its probes.

theorem Minimalist.Probe.mem_of_cascade_eq_some {α : Type u_1} {goals : List α} {ps : List (Probe α)} {a : α} (h : cascade ps goals = some a) : a ∈ goals

The cascade's goal is a member of the sequence.