Possibilities are the non-impossible minterms of a basis

Proved

AssumptionsOfPhysics.isPossibility_iff_minterm

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

foundations-of-physicsmathematical-physicstopology

Let $B$ be a basis of the experimental domain $\mathcal D$ . A statement $x$ is a possibility for $\mathcal D$ if and only if $x$ is not impossible and $x$ is a minterm of $B$ , i.e. $x=\bigwedge_{b\in B}\ell_b$ where each $\ell_b$ is either $b$ or $\neg b$ .

Preamble

import Mathlib
import Definitions.Def_AoP_ExperimentalDomains

Formal statement

namespace AssumptionsOfPhysics
theorem isPossibility_iff_minterm {Ω : Type*} (D : ExperimentalDomain Ω)
    (B : Set (Set Ω)) (hB : IsBasis D.stmts B) (x : Set Ω) :
    D.IsPossibility x ↔ x.Nonempty ∧ ∃ σ : B → Bool, x = minterm B σ := by sorry
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), Proposition 1.48, p. 130

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.

Setting (common to all statements of this mission). $\Omega$ is an arbitrary type (it may be empty), and a statement is a subset $s \subseteq \Omega$ . $D$ is an arbitrary experimental domain on $\Omega$ , i.e. a family $\mathcal D$ of subsets of $\Omega$ such that

$\Omega \in \mathcal D$ and $\emptyset \in \mathcal D$ ;
$s \cap t \in \mathcal D$ whenever $s, t \in \mathcal D$ ;
$\bigcup_{n \in \mathbb N} f_n \in \mathcal D$ whenever $f_n \in \mathcal D$ for all $n \in \mathbb N$ ;
there is a countable family $B_0 \subseteq \mathcal D$ such that every member of $\mathcal D$ belongs to $\langle B_0 \rangle$ , the smallest family containing $B_0$ , $\Omega$ and $\emptyset$ and closed under binary intersections and countable unions.

The theoretical domain $\bar{\mathcal D}$ is the smallest family of subsets of $\Omega$ that contains $\mathcal D$ and $\Omega$ and is closed under complement, binary intersection and countable union. A possibility is a set $x \in \bar{\mathcal D}$ with $x \neq \emptyset$ such that for every $t \in \bar{\mathcal D}$ either $x \subseteq t$ or $x \cap t = \emptyset$ . $X$ is the type of possibilities (two possibilities are equal exactly when their underlying sets are equal). For $s \subseteq \Omega$ the verifiable set is $U(s) = \{x \in X : x \cap s \neq \emptyset\}$ . The space $X$ carries the topology $\mathcal T$ generated by $\{U(s) : s \in \mathcal D\}$ , i.e. the coarsest topology on $X$ in which every $U(s)$ with $s \in \mathcal D$ is open.

Statement. For every type $\Omega$ , every experimental domain $D$ on $\Omega$ , every family $B$ that is a basis of $\mathcal D$ ( $B\subseteq\mathcal D$ and $\mathcal D\subseteq\langle B\rangle$ ; $B$ need not be countable) and every subset $x\subseteq\Omega$ : $x$ is a possibility of $D$ if and only if $x\neq\emptyset$ and there exists a function $\sigma: B\to\{\mathrm{true},\mathrm{false}\}$ with

x = \bigcap_{b\in B}\ell_b,\qquad \ell_b=\begin{cases} b & \sigma(b)=\mathrm{true}\\ \Omega\setminus b & \sigma(b)=\mathrm{false}.\end{cases}

When $B=\emptyset$ the right-hand intersection is $\Omega$ .

Human review

Endorsed by Shuze Chen · Oct 3, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph