Assumptions of Physics II.3: full characterization, natural orders, sparse/dense/complete orders

Definition

AoP_PropertiesQuantities

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

foundations-of-physicsmathematical-physicstopology

Definitions for Part II, Chapter 3 of Assumptions of Physics (Carcassi–Aidala, v3.0).

Full characterization by a property (Definitions 3.1, 3.3). A property is a continuous map $q:U\to Q$ from a verifiable set of possibilities to a topological space; the domain is fully characterized by it when $q:X\to Q$ is a homeomorphism. Only full characterization is used by the chapter's theorems, so it is defined directly as the existence of a homeomorphism $X\simeq Q$ .

Quantities (Definitions 3.4–3.6). A quantity is a property whose value space is linearly ordered and carries the order topology; in Lean this is a type with LinearOrder, TopologicalSpace and OrderTopology instances.

Natural order (Definition 3.7). A linear order on $X$ whose order topology is the natural topology.

Before-statements (Definition 3.12). $\text{“}x<x_1\text{”}=\bigvee_{x<x_1}x$ .

Sparse, dense, dense subset, complete (Definitions 3.39–3.40, 3.47, 3.49, 3.50). As in the book: every chain between two elements is finite; between any two elements $a<b$ there is an infinite chain; a subset meeting every $[q_1,q_2]$ with $q_1<q_2$ ; every non-empty bounded subset has a supremum (bounded above suffices and is used).

Definition code

import Mathlib
import Definitions.Def_AoP_ExperimentalDomains

/-!
# Assumptions of Physics, Part II, Chapter 3: properties and quantities

Source: G. Carcassi, C. A. Aidala, *Assumptions of Physics*, Ver. 3.0 (December 31, 2025),
Part II, Chapter 3 "Properties and quantities", Sections 3.1, 3.2, 3.4, 3.5.

Builds on the Chapter 1 definitions (`Def_AoP_ExperimentalDomains`): the possibilities
`D.Possibility` of an experimental domain carry the natural topology.
-/

namespace AssumptionsOfPhysics

universe u v

/-- Definition 3.40 (with Definition 3.39): a (pre)ordered set is sparse if every chain between
two elements is finite, i.e. every closed interval `[a, b]` is finite. -/
def IsSparseOrder (Q : Type v) [Preorder Q] : Prop :=
  ∀ a b : Q, (Set.Icc a b).Finite

/-- Definition 3.47: an ordered set is dense if between any two elements `a < b` there is an
infinite chain, i.e. the interval `[a, b]` is infinite. -/
def IsDenseOrder (Q : Type v) [Preorder Q] : Prop :=
  ∀ a b : Q, a < b → (Set.Icc a b).Infinite

/-- Definition 3.49: `A ⊆ Q` is dense in `Q` if for all `q₁ < q₂` there is `q ∈ A` with
`q₁ ≤ q ≤ q₂`. -/
def IsDenseSubset {Q : Type v} [Preorder Q] (A : Set Q) : Prop :=
  ∀ q₁ q₂ : Q, q₁ < q₂ → ∃ q ∈ A, q₁ ≤ q ∧ q ≤ q₂

/-- Definition 3.50: a linearly ordered set is complete if every non-empty subset that is
bounded (above) has a supremum (a least upper bound). -/
def IsCompleteOrder (Q : Type v) [Preorder Q] : Prop :=
  ∀ A : Set Q, A.Nonempty → BddAbove A → ∃ s, IsLUB A s

namespace ExperimentalDomain

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

/-- Definition 3.3: an experimental domain is fully characterized by a property with values in
the topological space `Q` if there is a homeomorphism `q : X → Q` from the possibilities
(with the natural topology) to `Q`. -/
def IsFullyCharacterizedBy (Q : Type v) [TopologicalSpace Q] : Prop :=
  Nonempty (D.Possibility ≃ₜ Q)

/-- Definition 3.7: a linear order on the possibilities is a natural order if the order
topology it generates coincides with the natural topology. -/
def IsNaturalOrder (r : LinearOrder D.Possibility) : Prop :=
  letI := r
  Preorder.topology D.Possibility = D.naturalTopology

/-- Definition 3.12: for a linear order on the possibilities, the statement "`x < x₁`", i.e.
the disjunction of all possibilities strictly before `x₁`. -/
def beforeStmt (r : LinearOrder D.Possibility) (x₁ : D.Possibility) : Set Ω :=
  letI := r
  ⋃ x ∈ {x : D.Possibility | x < x₁}, x.val

end ExperimentalDomain

end AssumptionsOfPhysics

Source

G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0 (Dec 31, 2025), https://assumptionsofphysics.org/book — Part II, Chapter 3 (pp. 169–195), Definitions 3.1–3.8, 3.12, 3.39, 3.40, 3.47, 3.49, 3.50

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.

This definition file imports Mathlib and the Chapter 1 definition file. It declares, in namespace AssumptionsOfPhysics:

Sparse order. For a type $Q$ with a preorder: every closed interval $[a,b]$ ( $a,b\in Q$ ) is a finite set. (For $a\not\le b$ the interval is empty.)
Dense order (book sense). For all $a<b$ in $Q$ , the interval $[a,b]$ is infinite. (Vacuous if $Q$ has no pair $a<b$ , e.g. $|Q|\le 1$ .)
Dense subset. $A\subseteq Q$ such that for all $q_1<q_2$ there is $q\in A$ with $q_1\le q\le q_2$ (non-strict inequalities; $q$ may equal an endpoint).
Complete order. Every nonempty $A\subseteq Q$ that has an upper bound has a least upper bound in $Q$ .

In namespace AssumptionsOfPhysics.ExperimentalDomain, for an experimental domain $D$ with possibilities $X$ (natural topology $\mathcal T$ ):

Fully characterized by $Q$ . For a topological space $Q$ : there exists a homeomorphism from $(X,\mathcal T)$ to $Q$ .
Natural order. For a linear order $\preceq$ on $X$ : the order topology of $\preceq$ (Mathlib's Preorder.topology, generated by the open rays) is equal to $\mathcal T$ .
Before-statement. For a linear order $\preceq$ on $X$ and $x_1\in X$ : the subset $\bigcup_{x\prec x_1} x\subseteq\Omega$ (union of the underlying sets of possibilities strictly below $x_1$ ; empty if $x_1$ is minimal).

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