Angular Locality

Angular Locality is the locality principle of mereological syntax: a part γ may subjoin to β only if γ is an n-part of some object α that is a 1-part of β. Since parthood is transitive within a dimension only, a subjunction path may turn through at most one angle, from dimension n into dimension 1. Everything the classical theory stipulates about cyclic domains and their escape hatches follows: 2-parts are the locality domains, and an object leaves a 2-part just when it is a 2-part of it.

This file defines Parthood.CanSubjoin and proves the consequences that hold in every structure: the target must contain the mover, so lowering, sideward, and parallel subjunction are ruled out; an immediate 1-part cannot resubjoin to its whole (antilocality); and an object inside a 2-part reaches an object outside it exactly when it lies on the 2-part's own 2-part chain.

Main definitions

• Parthood.CanSubjoin γ β — Angular Locality for subjunction of γ to β.

Main statements

• Parthood.descendant_of_canSubjoin, Parthood.not_canSubjoin_of_le — the target contains the mover.
• Parthood.not_canSubjoin_of_imm_one — antilocality, from irreflexivity of parthood.
• Parthood.canSubjoin_iff_nPart_two — locality domains are 2-parts, with escape along the 2-part chain.

References

• [adger-2025]

def MereologicalSyntax.Parthood.CanSubjoin {α : Type u_1} (P : Parthood α) (γ β : α) : Prop

Angular Locality: γ may subjoin to β only if γ is an n-part of some 1-part of β.

Equations

• P.CanSubjoin γ β = ∃ (a : α), P.WithinDim γ a ∧ P.NPart MereologicalSyntax.Dim.one a β

The target contains the mover

theorem MereologicalSyntax.Parthood.descendant_of_canSubjoin {α : Type u_1} {P : Parthood α} {γ β : α} (h : P.CanSubjoin γ β) : P.Descendant γ β

theorem MereologicalSyntax.Parthood.not_canSubjoin_of_le {α : Type u_1} {P : Parthood α} (rank : α → ℕ) (hrank : ∀ (n : Dim) (x y : α), P.Imm n x y → rank x < rank y) {γ β : α} (h : rank β ≤ rank γ) : ¬P.CanSubjoin γ β

Lowering, sideward, and parallel subjunction: no subjunction to an object of no greater rank.

Antilocality

theorem MereologicalSyntax.Parthood.not_canSubjoin_of_imm_one {α : Type u_1} {P : Parthood α} (hacyc : ∀ (x : α), ¬P.Descendant x x) {γ β : α} (h : P.Imm Dim.one γ β) : ¬P.CanSubjoin γ β

An immediate 1-part cannot resubjoin to its whole: the only candidate α is the part itself, and parthood is irreflexive.

Locality domains are 2-parts

theorem MereologicalSyntax.Parthood.not_canSubjoin_of_not_nPart_two {α : Type u_1} {P : Parthood α} {S : Set α} {b : α} (hS : ∀ x ∈ S, x ≠ b → ∀ (n : Dim) (y : α), P.Imm n x y → y ∈ S) (hb : ∀ (n : Dim) (y : α), P.Imm n b y → n = Dim.two) {γ β : α} (hγ : γ ∈ S) (hγb : γ ≠ b) (hβ : β ∉ S) (hn : ¬P.NPart Dim.two γ b) : ¬P.CanSubjoin γ β

Nothing inside the 2-part b other than its own 2-parts subjoins outside b.

theorem MereologicalSyntax.Parthood.canSubjoin_of_nPart_two {α : Type u_1} {P : Parthood α} {γ b d β : α} (hγ : P.NPart Dim.two γ b) (hbd : P.Imm Dim.two b d) (hd : P.NPart Dim.one d β) : P.CanSubjoin γ β

A 2-part of the 2-part b of d subjoins to anything d is a 1-part of.

theorem MereologicalSyntax.Parthood.canSubjoin_iff_nPart_two {α : Type u_1} {P : Parthood α} {S : Set α} {b : α} (hS : ∀ x ∈ S, x ≠ b → ∀ (n : Dim) (y : α), P.Imm n x y → y ∈ S) (hb : ∀ (n : Dim) (y : α), P.Imm n b y → n = Dim.two) {γ β d : α} (hbd : P.Imm Dim.two b d) (hd : P.NPart Dim.one d β) (hγ : γ ∈ S) (hγb : γ ≠ b) (hβ : β ∉ S) : P.CanSubjoin γ β ↔ P.NPart Dim.two γ b

The escape hatch: from inside the 2-part b of d, an object reaches an object above d in d's extended projection exactly when it is a 2-part of b.

Subjoin

def MereologicalSyntax.Parthood.subjoin {α : Type u_1} (P : Parthood α) [DecidableEq α] (x y : α) : Option (Parthood α)

Subjoin x to y: the first subjunction gives a 1-part, the second a 2-part, and there is no third (Dimensionality); nothing subjoins to itself.

Equations

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

theorem MereologicalSyntax.Parthood.subjoin_eq_none_of_full {α : Type u_1} {P : Parthood α} [DecidableEq α] {x y : α} (h₁ : (P.onePart y).isSome = true) (h₂ : (P.twoPart y).isSome = true) : P.subjoin x y = none