Assumptions of Physics II.1: statements, experimental and theoretical domains, possibilities, natural topology

Definition

AoP_ExperimentalDomains

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

foundations-of-physicsmathematical-physicstopology

This definition file fixes the vocabulary of Part II, Chapter 1 of Assumptions of Physics (Carcassi–Aidala, v3.0).

Statements as truth sets. A logical context is represented by its set $\Omega$ of possible assignments (Axiom 1.4, Definition 1.5). Because the axiom of closure (Axiom 1.9, Proposition 1.14) makes every set of possible assignments the truth set of some statement, and two statements are equivalent (Definition 1.15) exactly when they are true in the same possible assignments, a statement up to equivalence is represented by its truth set $s\subseteq\Omega$ . Negation, conjunction and disjunction become complement, intersection and union; the certainty is $\Omega$ , the impossibility is $\emptyset$ ; " $s_1$ is narrower than $s_2$ " is $s_1\subseteq s_2$ ; " $s_1$ is compatible with $s_2$ " is $s_1\cap s_2\neq\emptyset$ .

Basis (Definition 1.34). $B\subseteq\mathcal D$ is a basis of $\mathcal D$ if every element of $\mathcal D$ can be generated from $B$ by finite conjunction and countable disjunction (the empty conjunction and empty disjunction, i.e. certainty and impossibility, included).

Experimental domain (Definition 1.35). A set $\mathcal D$ of statements, closed under finite conjunction and countable disjunction, containing the certainty and the impossibility, and admitting a countable basis.

Theoretical domain (Definition 1.36). $\bar{\mathcal D}$ , the closure of $\mathcal D$ under negation, finite conjunction and countable disjunction.

Approximately verifiable (Definition 1.38). $s\in\bar{\mathcal D}$ with $s=\bigcap_{i=1}^\infty s_i$ for some sequence $s_i\in\mathcal D$ .

Possibility (Definition 1.47). $x\in\bar{\mathcal D}$ , $x\not\equiv\bot$ , such that for every $s\in\bar{\mathcal D}$ either $x\preccurlyeq s$ or $x$ is incompatible with $s$ . The possibilities form the set (and type) $X$ .

Verifiable sets and natural topology (Definition 1.55, Proposition 1.57). $U(s)=\{x\in X : x \text{ compatible with } s\}$ ; the natural topology on $X$ is the one generated by $\{U(s): s\in\mathcal D\}$ (Proposition 1.57, a separate milestone, asserts these are already all open sets).

Decidable domain (Definition 1.73). For every $s\in\mathcal D$ also $\neg s\in\mathcal D$ .

Minterm (Definition 1.25). A conjunction in which every element of $B$ appears exactly once, negated or not.

The primitive notion of verifiability (Axiom 1.27) is not modelled separately: membership in $\mathcal D$ is what the chapter's mathematical results use.

Definition code

import Mathlib

/-!
# Assumptions of Physics, Part II, Chapter 1: experimental domains

Source: G. Carcassi, C. A. Aidala, *Assumptions of Physics*, Ver. 3.0 (December 31, 2025),
Part II ("Physical Mathematics"), Chapter 1 "Verifiable statements and experimental domains",
Sections 1.1–1.4 and 1.6.

Modelling convention. A logical context is represented by its type `Ω` of possible
assignments (Axiom 1.4, Definition 1.5). By the axiom of closure (Axiom 1.9 /
Proposition 1.14) every set of possible assignments is the truth set of some statement, and
two statements are equivalent (Definition 1.15) exactly when they are true in the same
possible assignments. A statement up to equivalence is therefore represented by its truth set
`s : Set Ω`; negation, conjunction and disjunction are complement, intersection and union;
the certainty is `Set.univ` and the impossibility is `∅`; `s₁ ≼ s₂` (narrower than) is
`s₁ ⊆ s₂`; `s₁` compatible with `s₂` is `(s₁ ∩ s₂).Nonempty`; incompatibility is `Disjoint`.
-/

namespace AssumptionsOfPhysics

universe u

/-- The statements generated from a set `B` of statements by finite conjunction and countable
disjunction (Definition 1.34). The empty conjunction (the certainty) and the empty disjunction
(the impossibility) are included. -/
inductive FinConjCountDisj {Ω : Type u} (B : Set (Set Ω)) : Set Ω → Prop
  | basic {s : Set Ω} : s ∈ B → FinConjCountDisj B s
  | univ : FinConjCountDisj B Set.univ
  | empty : FinConjCountDisj B ∅
  | inter {s t : Set Ω} : FinConjCountDisj B s → FinConjCountDisj B t →
      FinConjCountDisj B (s ∩ t)
  | iUnion (f : ℕ → Set Ω) : (∀ n, FinConjCountDisj B (f n)) →
      FinConjCountDisj B (⋃ n, f n)

/-- The statements generated from a set `B` of statements by negation, finite conjunction and
countable disjunction (Definition 1.36). The certainty (empty conjunction) is included. -/
inductive NegFinConjCountDisj {Ω : Type u} (B : Set (Set Ω)) : Set Ω → Prop
  | basic {s : Set Ω} : s ∈ B → NegFinConjCountDisj B s
  | univ : NegFinConjCountDisj B Set.univ
  | compl {s : Set Ω} : NegFinConjCountDisj B s → NegFinConjCountDisj B sᶜ
  | inter {s t : Set Ω} : NegFinConjCountDisj B s → NegFinConjCountDisj B t →
      NegFinConjCountDisj B (s ∩ t)
  | iUnion (f : ℕ → Set Ω) : (∀ n, NegFinConjCountDisj B (f n)) →
      NegFinConjCountDisj B (⋃ n, f n)

/-- Definition 1.34: `B ⊆ D` is a basis of the set of statements `D` if every element of `D`
can be generated from `B` using finite conjunction and countable disjunction. -/
def IsBasis {Ω : Type u} (D B : Set (Set Ω)) : Prop :=
  B ⊆ D ∧ ∀ s ∈ D, FinConjCountDisj B s

/-- Definition 1.35: an experimental domain is a set of statements, closed under finite
conjunction and countable disjunction, that contains the certainty and the impossibility and
is generated from a countable basis. The elements of `stmts` are the verifiable statements of
the domain. -/
structure ExperimentalDomain (Ω : Type u) where
  /-- The statements of the domain (as truth sets over the possible assignments `Ω`). -/
  stmts : Set (Set Ω)
  /-- The certainty belongs to the domain. -/
  univ_mem : Set.univ ∈ stmts
  /-- The impossibility belongs to the domain. -/
  empty_mem : ∅ ∈ stmts
  /-- Closure under finite (binary) conjunction. -/
  inter_mem : ∀ s t : Set Ω, s ∈ stmts → t ∈ stmts → s ∩ t ∈ stmts
  /-- Closure under countable disjunction. -/
  iUnion_mem : ∀ f : ℕ → Set Ω, (∀ n, f n ∈ stmts) → (⋃ n, f n) ∈ stmts
  /-- The domain admits a countable basis. -/
  exists_countable_basis : ∃ B : Set (Set Ω), B.Countable ∧ IsBasis stmts B

namespace ExperimentalDomain

variable {Ω : Type u} (D : ExperimentalDomain Ω)

/-- Definition 1.36: the theoretical domain `D̄`, the set of all statements generated from
`D` using negation, finite conjunction and countable disjunction. -/
def theoretical : Set (Set Ω) := {s | NegFinConjCountDisj D.stmts s}

/-- Definition 1.38: a theoretical statement is approximately verifiable if it is the
countable conjunction of a sequence of verifiable statements of the domain. -/
def IsApproxVerifiable (s : Set Ω) : Prop :=
  s ∈ D.theoretical ∧ ∃ f : ℕ → Set Ω, (∀ i, f i ∈ D.stmts) ∧ s = ⋂ i, f i

/-- Definition 1.47: a possibility for `D` is a theoretical statement `x` that is not
impossible and such that, for every theoretical statement `s`, either `x` is narrower than
`s` or `x` is incompatible with `s`. -/
def IsPossibility (x : Set Ω) : Prop :=
  x ∈ D.theoretical ∧ x.Nonempty ∧ ∀ s ∈ D.theoretical, x ⊆ s ∨ Disjoint x s

/-- Definition 1.47: the (full) possibilities `X` of `D`, as a set of statements. -/
def possibilities : Set (Set Ω) := {x | D.IsPossibility x}

/-- The possibilities of `D`, as a type: the points of the natural topology. -/
structure Possibility where
  /-- The statement underlying the possibility. -/
  val : Set Ω
  /-- It is a possibility of `D`. -/
  isPossibility : D.IsPossibility val

/-- Definition 1.55: the verifiable set `U(s) = {x ∈ X | x compatible with s}` of
possibilities associated with a statement `s`. -/
def verifiableSet (s : Set Ω) : Set D.Possibility :=
  {x | (x.val ∩ s).Nonempty}

/-- Proposition 1.57 / Definition 1.55: the natural topology on the possibilities, generated by
the verifiable sets `U(s)` of the statements `s ∈ D`. (That these sets are already *all* the
open sets is Proposition 1.57, stated separately.) -/
instance naturalTopology : TopologicalSpace D.Possibility :=
  TopologicalSpace.generateFrom (D.verifiableSet '' D.stmts)

/-- Definition 1.73: an experimental domain is decidable if for every `s ∈ D` also `¬s ∈ D`. -/
def IsDecidable : Prop := ∀ s ∈ D.stmts, sᶜ ∈ D.stmts

end ExperimentalDomain

/-- Definition 1.25: the minterm of a set of statements `B` selected by `σ`: the conjunction
over all `b ∈ B` of `b` (if `σ b = true`) or `¬b` (if `σ b = false`). -/
def minterm {Ω : Type u} (B : Set (Set Ω)) (σ : B → Bool) : Set Ω :=
  ⋂ b : B, if σ b then (b : Set Ω) else (b : Set Ω)ᶜ

end AssumptionsOfPhysics

Source

G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0 (Dec 31, 2025), https://assumptionsofphysics.org/book — Part II, Chapter 1 (pp. 101–146), Definitions 1.25, 1.34, 1.35, 1.36, 1.38, 1.47, 1.55, 1.73; Axioms 1.4, 1.9; Proposition 1.14 (pp. 101–142)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves.

The definition file introduces the following objects (inside the namespace AssumptionsOfPhysics; it imports all of Mathlib and contains no theorems).

Finite-conjunction / countable-disjunction closure. For a family $B$ of subsets of a type $\Omega$ , $\langle B\rangle$ is the smallest family of subsets of $\Omega$ containing every member of $B$ , $\Omega$ itself and $\emptyset$ , and closed under binary intersection $s \cap t$ and countable unions $\bigcup_{n\in\mathbb N} f_n$ .
Negation / finite-conjunction / countable-disjunction closure. For a family $B$ , $\langle B\rangle^{\neg}$ is the smallest family containing every member of $B$ and $\Omega$ , closed under complement, binary intersection and countable unions (this is the σ-algebra generated by $B$ ; note that $\emptyset$ enters as the complement of $\Omega$ ).
Basis. For families $\mathcal D, B$ of subsets of $\Omega$ , " $B$ is a basis of $\mathcal D$ " means $B \subseteq \mathcal D$ and every member of $\mathcal D$ lies in $\langle B\rangle$ . No countability is required here.
Experimental domain on $\Omega$ (a structure). Data: a family $\mathcal D$ of subsets of $\Omega$ ("statements"). Conditions: $\Omega \in \mathcal D$ ; $\emptyset \in \mathcal D$ ; $\mathcal D$ is closed under binary intersection; $\mathcal D$ is closed under countable unions indexed by $\mathbb N$ ; and there exists a countable family $B$ that is a basis of $\mathcal D$ in the sense of item 3. There is no other condition; in particular $\Omega$ may be empty and $\mathcal D$ may be just $\{\emptyset, \Omega\}$ .

For an experimental domain $D$ with family $\mathcal D$ :

Theoretical domain $\bar{\mathcal D} = \langle \mathcal D\rangle^{\neg}$ .
Approximately verifiable. A set $s\subseteq\Omega$ is approximately verifiable if $s \in \bar{\mathcal D}$ and there is a sequence $(f_i)_{i\in\mathbb N}$ of members of $\mathcal D$ with $s = \bigcap_{i\in\mathbb N} f_i$ .
Possibility. A set $x\subseteq\Omega$ is a possibility if $x\in\bar{\mathcal D}$ , $x$ is nonempty, and for every $t\in\bar{\mathcal D}$ either $x\subseteq t$ or $x$ and $t$ are disjoint. possibilities is the set of all such $x$ .
The type of possibilities $X$ : pairs consisting of a set $x\subseteq\Omega$ and a proof that $x$ is a possibility. (Equality of two elements reduces to equality of the underlying sets.)
Verifiable set. For any $s\subseteq\Omega$ (not required to be in $\mathcal D$ ), $U(s) = \{x \in X : x\cap s \neq\emptyset\}$ .
Natural topology (declared as the default topology on $X$ ): the topology generated by the family $\{U(s): s\in\mathcal D\}$ , i.e. the coarsest topology on $X$ in which all these sets are open. Its open sets are, a priori, arbitrary unions of finite intersections of such sets.
Decidable domain. $D$ is decidable if $\Omega\setminus s \in \mathcal D$ for every $s\in\mathcal D$ .
Minterm. For a family $B$ of subsets of $\Omega$ and a function $\sigma : B\to\{\mathrm{true},\mathrm{false}\}$ , $\operatorname{minterm}(B,\sigma) = \bigcap_{b\in B} \ell_b$ , where $\ell_b = b$ if $\sigma(b)=\mathrm{true}$ and $\ell_b = \Omega\setminus b$ otherwise. If $B$ is empty this intersection is $\Omega$ .

View graph