Particle capabilities

This file defines Distributed α Ctx: a carrier α with a recorded three-valued distribution over licensing contexts Ctx, the Proform-style capability behind Particle's two facets (instances for Clause.Context and Clause.Embedding).

There is deliberately no universal clause carrier: a theory whose clause representation C classifies into these cells obtains Distributed Particle C by pullback along its classifier, keeping the stored facets finite and decidable.

class Distributed (α : Type u_1) (Ctx : Type u_2) : Type (max u_1 u_2)

A carrier α with a recorded three-valued distribution over licensing contexts Ctx. none = the source records nothing (distinct from some .excluded).

• status? : α → Ctx → Option ParticleStatus

  Recorded status of a in context c, if any.

def Distributed.LicensedIn {α : Type u_1} {Ctx : Type u_2} [Distributed α Ctx] (a : α) (c : Ctx) : Prop

Positively recorded as available (obligatorily or optionally).

Equations

• Distributed.LicensedIn a c = match Distributed.status? a c with | some ParticleStatus.obligatory => True | some ParticleStatus.optional => True | x => False

@[implicit_reducible]

instance Distributed.instDecidableLicensedIn {α : Type u_1} {Ctx : Type u_2} [Distributed α Ctx] (a : α) (c : Ctx) : Decidable (LicensedIn a c)

Equations

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

@[implicit_reducible]

instance instDistributedParticleContext : Distributed Particle Clause.Context

Equations

• instDistributedParticleContext = { status? := Particle.status? }

@[implicit_reducible]

instance instDistributedParticleEmbedding : Distributed Particle Clause.Embedding

Equations

• instDistributedParticleEmbedding = { status? := Particle.embedStatus? }

theorem Particle.distributed_clause_eq (p : Particle) (c : Clause.Context) : Distributed.status? p c = p.status? c

The capability agrees with the carrier's own clause-axis view.

theorem Particle.distributed_embed_eq (p : Particle) (c : Clause.Embedding) : Distributed.status? p c = p.embedStatus? c

The capability agrees with the carrier's own embedding-axis view.