A Simplified Geometry of Interaction

References

• [Jean-Yves Girard, Geometry of interaction. V: Logic in the hyperfinite factor][Gir11]
• [Thomas Seiller, Interaction graphs: multiplicatives][Sei12]

Project

structure LO.Propositional.LinearLogic.Multiplicative.GoI.Project (Carrier : Type u_1) : Type u_1

• wager : ℕ

  Wager, a remnant of self-closed cycles.

• plot : Equiv.Perm Carrier

  A main gadget expresses permutation of loci.

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.ext_iff {Carrier : Type u_1} {x y : Project Carrier} : x = y ↔ x.wager = y.wager ∧ x.plot = y.plot

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.ext {Carrier : Type u_1} {x y : Project Carrier} (wager : x.wager = y.wager) (plot : x.plot = y.plot) : x = y

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.add {α : Type u_1} {β : Type u_2} (𝔞 : Project α) (𝔟 : Project β) : Project (α ⊕ β)

Equations

• 𝔞.add 𝔟 = { wager := 𝔞.wager + 𝔟.wager, plot := 𝔞.plot.sumCongr 𝔟.plot }

@[implicit_reducible]

instance LO.Propositional.LinearLogic.Multiplicative.GoI.Project.instHAddSum {α : Type u_1} {β : Type u_2} : HAdd (Project α) (Project β) (Project (α ⊕ β))

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.Project.instHAddSum = { hAdd := LO.Propositional.LinearLogic.Multiplicative.GoI.Project.add }

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.add_wager {α : Type u_1} {β : Type u_2} (𝔞 : Project α) (𝔟 : Project β) : (𝔞 + 𝔟).wager = 𝔞.wager + 𝔟.wager

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.add_plot {α : Type u_1} {β : Type u_2} (𝔞 : Project α) (𝔟 : Project β) : (𝔞 + 𝔟).plot = 𝔞.plot.sumCongr 𝔟.plot

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.one {α : Type u_1} : Project α

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.Project.one = { wager := 0, plot := Equiv.refl α }

@[implicit_reducible]

instance LO.Propositional.LinearLogic.Multiplicative.GoI.Project.instOne {α : Type u_1} : One (Project α)

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.Project.instOne = { one := LO.Propositional.LinearLogic.Multiplicative.GoI.Project.one }

@[implicit_reducible]

instance LO.Propositional.LinearLogic.Multiplicative.GoI.Project.instInhabited {α : Type u_1} : Inhabited (Project α)

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.Project.instInhabited = { default := 1 }

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.one_wager {α : Type u_1} : wager 1 = 0

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.one_plot {α : Type u_1} : plot 1 = Equiv.refl α

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.mul {α : Type u_1} (𝔞 𝔟 : Project α) : Project α

Equations

• 𝔞.mul 𝔟 = { wager := 𝔞.wager + 𝔟.wager, plot := 𝔞.plot * 𝔟.plot }

@[implicit_reducible]

instance LO.Propositional.LinearLogic.Multiplicative.GoI.Project.instMul {α : Type u_1} : Mul (Project α)

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.Project.instMul = { mul := LO.Propositional.LinearLogic.Multiplicative.GoI.Project.mul }

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.mul_wager {α : Type u_1} (𝔞 𝔟 : Project α) : (𝔞 * 𝔟).wager = 𝔞.wager + 𝔟.wager

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.mul_plot {α : Type u_1} (𝔞 𝔟 : Project α) : (𝔞 * 𝔟).plot = 𝔞.plot * 𝔟.plot

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.mul_one {α : Type u_1} (𝔞 : Project α) : 𝔞 * 1 = 𝔞

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.one_mul {α : Type u_1} (𝔞 : Project α) : 1 * 𝔞 = 𝔞

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.mul_assoc {α : Type u_1} (𝔞 𝔟 𝔠 : Project α) : 𝔞 * 𝔟 * 𝔠 = 𝔞 * (𝔟 * 𝔠)

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.add_mul_add {α : Type u_1} {β : Type u_2} (𝔞₁ 𝔞₂ : Project α) (𝔟₁ 𝔟₂ : Project β) : (𝔞₁ + 𝔟₁) * (𝔞₂ + 𝔟₂) = 𝔞₁ * 𝔞₂ + 𝔟₁ * 𝔟₂

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.delocate {α : Type u_1} {β : Type u_2} (𝔞 : Project α) (φ : α ≃ β) : Project β

Equations

• 𝔞.delocate φ = { wager := 𝔞.wager, plot := (φ.symm.trans 𝔞.plot).trans φ }

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.delocate_wager {α : Type u_1} {β : Type u_2} (𝔞 : Project α) (φ : α ≃ β) : (𝔞.delocate φ).wager = 𝔞.wager

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.delocate_plot {α : Type u_1} {β : Type u_2} (𝔞 : Project α) (φ : α ≃ β) : (𝔞.delocate φ).plot = (φ.symm.trans 𝔞.plot).trans φ

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.delocate_mul {α : Type u_1} {β : Type u_2} (𝔞 𝔟 : Project α) (φ : α ≃ β) : (𝔞 * 𝔟).delocate φ = 𝔞.delocate φ * 𝔟.delocate φ

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.delocate_sumComm_add {α : Type u_1} {β : Type u_2} {𝔠 : Project (α ⊕ β)} (𝔞 : Project α) (𝔟 : Project β) : 𝔠.delocate (Equiv.sumComm α β) * (𝔟 + 𝔞) = (𝔠 * (𝔞 + 𝔟)).delocate (Equiv.sumComm α β)

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.delocate_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (𝔞 : Project α) (φ : α ≃ β) (ψ : β ≃ γ) : 𝔞.delocate (φ.trans ψ) = (𝔞.delocate φ).delocate ψ

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.delocate_one {α : Type u_1} (𝔞 : Project α) : 𝔞.delocate 1 = 𝔞

Measurement and Polarity

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.tr {α : Type u_1} [Fintype α] [DecidableEq α] (𝔞 : Project α) : ℕ

Equations

• 𝔞.tr = 𝔞.wager + 𝔞.plot.tr

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.measurement {α : Type u_1} [Fintype α] [DecidableEq α] (𝔞 𝔟 : Project α) : ℕ

Equations

• 𝔞.measurement 𝔟 = (𝔞 * 𝔟).tr

def LO.Propositional.LinearLogic.Multiplicative.GoI.«term⟪_|_⟫» : Lean.ParserDescr

Equations

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

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.IsPolar {α : Type u_1} [Fintype α] [DecidableEq α] (𝔞 𝔟 : Project α) : Prop

Equations

• 𝔞.IsPolar 𝔟 = (𝔞.measurement 𝔟 = 1)

def LO.Propositional.LinearLogic.Multiplicative.GoI.«term_⟂_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.tr_add {α : Type u_1} [Fintype α] [DecidableEq α] (𝔞 𝔟 : Project α) : (𝔞 + 𝔟).tr = 𝔞.tr + 𝔟.tr

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.tr_delocate {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (𝔞 : Project α) (φ : α ≃ β) : (𝔞.delocate φ).tr = 𝔞.tr

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.measurement_comm {α : Type u_1} [Fintype α] [DecidableEq α] (𝔞 𝔟 : Project α) : 𝔞.measurement 𝔟 = 𝔟.measurement 𝔞

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.isPolar_symm {α : Type u_1} [Fintype α] [DecidableEq α] {𝔞 𝔟 : Project α} : 𝔞.IsPolar 𝔟 ↔ 𝔟.IsPolar 𝔞

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.fax (α : Type u_4) : Project (α ⊕ α)

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.Project.fax α = { wager := 0, plot := Equiv.sumComm α α }

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.fax_wager (α : Type u_4) : (fax α).wager = 0

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.daimon (r : ℕ) : Project PEmpty.{u_4 + 1}

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.Project.daimon r = { wager := r, plot := default }

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.subtypeExtend {α : Type u_1} {P : α → Prop} [DecidablePred P] (𝔞 : Project { a : α // P a }) : Project α

Equations

• 𝔞.subtypeExtend = { wager := 𝔞.wager, plot := 𝔞.plot.subtypeCongr 1 }

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.subtypeExtend_wager {α : Type u_1} {P : α → Prop} [DecidablePred P] (𝔞 : Project { a : α // P a }) : 𝔞.subtypeExtend.wager = 𝔞.wager

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.permApp {α : Type u_1} {β : Type u_2} (F : Equiv.Perm (α ⊕ β)) (A : Equiv.Perm α) : Equiv.Perm (α ⊕ β)

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.Project.permApp F A = F * A.sumCongr 1

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.IsLeftEquivLeft {α : Type u_1} {β : Type u_2} : { x : α ⊕ β // x.isLeft = true } ≃ α

Equations

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

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.notIsLeftEquivRight {α : Type u_1} {β : Type u_2} : { x : α ⊕ β // ¬x.isLeft = true } ≃ β

Equations

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

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.subtypeExtend_delocate_IsLeftEquivLeft_symm {α : Type u_1} {β : Type u_2} (𝔞 : Project α) : (𝔞.delocate IsLeftEquivLeft.symm).subtypeExtend = 𝔞 + 1

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.subtypeExtend_delocate_notIsLeftEquivRight_symm {α : Type u_1} {β : Type u_2} (𝔟 : Project β) : (𝔟.delocate notIsLeftEquivRight.symm).subtypeExtend = 1 + 𝔟

Execution and Adjoint

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.trace {γ : Type u_3} [Fintype γ] [DecidableEq γ] (𝔣 : Project γ) (P : γ → Prop) [DecidablePred P] : Project { x : γ // ¬P x }

Equations

• 𝔣.trace P = { wager := 𝔣.wager + 𝔣.plot.closedCycles P, plot := 𝔣.plot.trace P }

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.trace_wager {γ : Type u_3} [Fintype γ] [DecidableEq γ] {P : γ → Prop} [DecidablePred P] (𝔣 : Project γ) : (𝔣.trace P).wager = 𝔣.wager + 𝔣.plot.closedCycles P

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.trace_plot {γ : Type u_3} [Fintype γ] [DecidableEq γ] {P : γ → Prop} [DecidablePred P] (𝔣 : Project γ) : (𝔣.trace P).plot = 𝔣.plot.trace P

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.trace_tr {γ : Type u_3} [Fintype γ] [DecidableEq γ] {P : γ → Prop} [DecidablePred P] (𝔣 : Project γ) : (𝔣.trace P).tr = 𝔣.wager + 𝔣.plot.closedCycles P + (𝔣.trace P).plot.tr

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.execution {γ : Type u_3} [Fintype γ] [DecidableEq γ] {P : γ → Prop} [DecidablePred P] (𝔣 : Project γ) (𝔞 : Project { x : γ // P x }) : Project { x : γ // ¬P x }

Equations

• 𝔣.execution 𝔞 = (𝔣 * 𝔞.subtypeExtend).trace P

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.execution_wager {γ : Type u_3} [Fintype γ] [DecidableEq γ] {P : γ → Prop} [DecidablePred P] (𝔣 : Project γ) (𝔞 : Project { x : γ // P x }) : (𝔣.execution 𝔞).wager = 𝔣.wager + 𝔞.wager + (𝔣 * 𝔞.subtypeExtend).plot.closedCycles P

def LO.Propositional.LinearLogic.Multiplicative.GoI.Project.executionSum {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (𝔣 : Project (α ⊕ β)) (𝔞 : Project α) : Project β

Equations

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

def LO.Propositional.LinearLogic.Multiplicative.GoI.«term_∷_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.executionSum_wager {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (𝔣 : Project (α ⊕ β)) (𝔞 : Project α) : (𝔣.executionSum 𝔞).wager = 𝔣.wager + 𝔞.wager + (𝔣 * (𝔞 + 1)).plot.closedCycles fun (x : α ⊕ β) => x.isLeft = true

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.executionSum_tr {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (𝔣 : Project (α ⊕ β)) (𝔞 : Project α) : (𝔣.executionSum 𝔞).tr = (𝔣.wager + 𝔞.wager + (𝔣 * (𝔞 + 1)).plot.closedCycles fun (x : α ⊕ β) => x.isLeft = true) + ((𝔣 * (𝔞 + 1)).trace fun (x : α ⊕ β) => x.isLeft = true).plot.tr

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.execution_mul {γ : Type u_3} [Fintype γ] [DecidableEq γ] {P : γ → Prop} [DecidablePred P] (𝔣 : Project γ) (𝔞 : Project { x : γ // P x }) (𝔟 : Project { x : γ // ¬P x }) : 𝔣.execution 𝔞 * 𝔟 = (𝔣 * 𝔟.subtypeExtend).execution 𝔞

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.executionSum_mul {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (𝔣 : Project (α ⊕ β)) (𝔞 : Project α) (𝔟 : Project β) : 𝔣.executionSum 𝔞 * 𝔟 = (𝔣 * (1 + 𝔟)).executionSum 𝔞

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.execution_adjoint {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (𝔣 : Project (α ⊕ β)) (𝔞 : Project α) (𝔟 : Project β) : 𝔣.measurement (𝔞 + 𝔟) = (𝔣.executionSum 𝔞).measurement 𝔟

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Project.execution_adjoint_polar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (𝔣 : Project (α ⊕ β)) (𝔞 : Project α) (𝔟 : Project β) : (𝔣.executionSum 𝔞).IsPolar 𝔟 ↔ 𝔣.IsPolar (𝔞 + 𝔟)

Conducts

def LO.Propositional.LinearLogic.Multiplicative.GoI.poler {α : Type u_1} [Fintype α] [DecidableEq α] (A : Set (Project α)) : Set (Project α)

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.poler A = {𝔟 : LO.Propositional.LinearLogic.Multiplicative.GoI.Project α | ∀ 𝔞 ∈ A, 𝔞.IsPolar 𝔟}

def LO.Propositional.LinearLogic.Multiplicative.GoI.«term_ᗮ» : Lean.TrailingParserDescr

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.«term_ᗮ» = Lean.ParserDescr.trailingNode `LO.Propositional.LinearLogic.Multiplicative.GoI.«term_ᗮ» 1024 1024 (Lean.ParserDescr.symbol "ᗮ")

def LO.Propositional.LinearLogic.Multiplicative.GoI.IsConduct {α : Type u_1} [Fintype α] [DecidableEq α] (A : Set (Project α)) : Prop

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.IsConduct A = (A = LO.Propositional.LinearLogic.Multiplicative.GoI.poler (LO.Propositional.LinearLogic.Multiplicative.GoI.poler A))

structure LO.Propositional.LinearLogic.Multiplicative.GoI.Conduct (α : Type u_3) [Fintype α] [DecidableEq α] : Type u_3

• set : Set (Project α)
• set_isConduct : IsConduct self.set

@[implicit_reducible]

instance LO.Propositional.LinearLogic.Multiplicative.GoI.instSetLikeConductProject {α : Type u_1} [Fintype α] [DecidableEq α] : SetLike (Conduct α) (Project α)

Equations

• LO.Propositional.LinearLogic.Multiplicative.GoI.instSetLikeConductProject = { coe := LO.Propositional.LinearLogic.Multiplicative.GoI.Conduct.set, coe_injective := ⋯ }

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.mem_poler_iff {α : Type u_1} [Fintype α] [DecidableEq α] (A : Set (Project α)) (𝔟 : Project α) : 𝔟 ∈ poler A ↔ ∀ 𝔞 ∈ A, 𝔞.IsPolar 𝔟

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.tripoler_eq_poler {α : Type u_1} [Fintype α] [DecidableEq α] (A : Set (Project α)) : poler (poler (poler A)) = poler A

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.subset_bipoler {α : Type u_1} [Fintype α] [DecidableEq α] (A : Set (Project α)) : A ⊆ poler (poler A)

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.isConduct_iff_subset_bipoler {α : Type u_1} [Fintype α] [DecidableEq α] {A : Set (Project α)} : IsConduct A ↔ poler (poler A) ⊆ A

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.poler_isConduct {α : Type u_1} [Fintype α] [DecidableEq α] (A : Set (Project α)) : IsConduct (poler A)

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Conduct.set_polar_polar {α : Type u_1} [Fintype α] [DecidableEq α] (A : Conduct α) : poler (poler A.set) = A.set

@[simp]

theorem LO.Propositional.LinearLogic.Multiplicative.GoI.Conduct.mem_set_polar_polar {α : Type u_1} [Fintype α] [DecidableEq α] {a : Project α} (A : Conduct α) : a ∈ poler (poler A.set) ↔ a ∈ A

def LO.Propositional.LinearLogic.Multiplicative.GoI.Conduct.tensor {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Conduct α) (B : Conduct β) : Conduct (α ⊕ β)

Equations

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

def LO.Propositional.LinearLogic.Multiplicative.GoI.Conduct.par {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Conduct α) (B : Conduct β) : Conduct (α ⊕ β)

Equations

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

def LO.Propositional.LinearLogic.Multiplicative.GoI.Conduct.lollipop {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Conduct α) (B : Conduct β) : Conduct (α ⊕ β)

Equations

• A.lollipop B = { set := {𝔣 : LO.Propositional.LinearLogic.Multiplicative.GoI.Project (α ⊕ β) | ∀ 𝔞 ∈ A, 𝔣.executionSum 𝔞 ∈ B}, set_isConduct := ⋯ }

Successful Projects and Conducts

structure LO.Propositional.LinearLogic.Multiplicative.GoI.Project.IsSuccessful {α : Type u_1} [Fintype α] [DecidableEq α] (𝔞 : Project α) : Prop

• square_eq_one : 𝔞 * 𝔞 = 1
• trace_zero : 𝔞.plot.support = Finset.univ

def LO.Propositional.LinearLogic.Multiplicative.GoI.Conduct.IsSuccessful {α : Type u_1} [Fintype α] [DecidableEq α] (A : Conduct α) : Prop

Equations

• A.IsSuccessful = ∃ 𝔞 ∈ A, 𝔞.IsSuccessful