ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Configuration domains of two labeled particles: collision exclusion and a rigid rod as a regular holonomic constraint

Physical scope

A worked verification for two labeled particles of the model: openness of the collision-excluded configuration domain, and the rigid-rod holonomic constraint as a regular level set of the squared-distance function with five configuration degrees of freedom and the two-particle mass operator. The example is a computation inside the definition of the configuration stage; it adopts no force law, asserts no motion and contains no empirical claim.

Example

Let $N = 2$ labeled particles carry masses $m_{1}, m_{2} > 0$ (Particle labels, worldlines, the frame-time parameter condition and fixed inertial masses), fix one inertial frame, and write a position pair as $x = (x_{1}, x_{2}) \in R^{6} = (R^{3})^{2}$ with the inner product

$⟨ x, y ⟩_{6} = ⟨ x_{1}, y_{1} ⟩_{2} + ⟨ x_{2}, y_{2} ⟩_{2}$

of Constrained configurations, the mass matrix and the mass metric, where $⟨ \cdot, \cdot ⟩_{2}$ is the Euclidean inner product of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ .

Singular-force branch. For a force model undefined at coincident positions, exclude the collision set $Δ = {x \in R^{6} : x_{1} = x_{2}}$ and take $Q_{0} : = R^{6} ∖ Δ$ .

Rigid rod. Let $ℓ > 0$ (in metres) and take the constraint function

$G (x) : = ∥ x_{1} - x_{2} ∥_{2}^{2} - ℓ^{2}, G : R^{6} ⟶ R,$

with the ambient set $O = R^{6}$ and $k = 1$ in the notation of Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator. The zero set $Q : = G^{- 1} (0)$ is the configuration space of two particles whose mutual distance is the fixed length $ℓ$ ; the case is a holonomic constraint branch of the definition.

Facts & Assumptions

Given: The two labeled particles with masses $m_{1}, m_{2} > 0$ , the position space $R^{6}$ with the inner product $⟨ \cdot, \cdot ⟩_{6}$ , the collision set $Δ$ and the function $G$ above with $ℓ > 0$ .

[L1]

Configuration domains: the unconstrained domain of the model is a stated open set $Q \subseteq R^{3 N}$ , the collision exclusion removes the set $Δ$ when the force law is undefined there, and the holonomic branch takes $Q = G^{- 1} (0)$ for a smooth $G$ with nonempty zero set and $D G$ of rank $k$ on it; the degrees of freedom are $\dim Q = 3 N - k$ , where $N$ is the number of labels and $k$ the number of independent constraint components (Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator).

[L2]

Regular level set theorem: for a smooth map $F : M^{m} \to N^{n}$ with regular value $q$ and nonempty $F^{- 1} (q)$ , the level set is an embedded submanifold of codimension $n$ , that is, of dimension $m - n$ (A regular level set is an embedded submanifold).

[L3]

The particle configuration $(Q, X)$ with inclusion $X : Q ↪ R^{6}$ , the mass matrix $M (x_{1}, x_{2}) = (m_{1} x_{1}, m_{2} x_{2})$ and the mass metric $G_{q} (u, v) = ⟨ d X_{q} (u), M d X_{q} (v) ⟩_{6}$ (Constrained configurations, the mass matrix and the mass metric).

[L4]

The Euclidean inner product $⟨ \cdot, \cdot ⟩_{2}$ is bilinear, symmetric and positive definite, and $∥ z ∥_{2}^{2} = ⟨ z, z ⟩_{2}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Verification

technique · direct; exhibit the openness of the collision-excluded domain by an explicit radius, compute the differential of $G$ and apply the regular level set theorem

1.1L1L4algebra

$Δ$ is closed, hence $Q_{0} = R^{6} ∖ Δ$ is open: for $x \notin Δ$ the number $δ : = ∥ x_{1} - x_{2} ∥_{2}$ is positive, and every $y \in R^{6}$ with $∥ y - x ∥_{2} < δ / 4$ satisfies $∥ y_{1} - y_{2} ∥_{2} \geq ∥ x_{1} - x_{2} ∥_{2} - ∥ y_{1} - x_{1} ∥_{2} - ∥ y_{2} - x_{2} ∥_{2} > δ - δ / 4 - δ / 4 = δ / 2 > 0$ , so $y \notin Δ$ ; the ball of radius $δ / 4$ about $x$ therefore lies in $Q_{0}$ , and $Q_{0}$ is open as required by [L1].

1.2L4algebra

The differential of $G$ : for $x \in R^{6}$ and $u = (u_{1}, u_{2}) \in R^{6}$ one has $G (x + s u) - G (x) = 2 s ⟨ x_{1} - x_{2}, u_{1} - u_{2} ⟩_{2} + s^{2} ∥ u_{1} - u_{2} ∥_{2}^{2}$ by bilinearity of the inner product [L4], so $D G (x) (u) = 2 ⟨ x_{1} - x_{2}, u_{1} - u_{2} ⟩_{2}$ ; this linear functional is nonzero exactly when $x_{1} \neq x_{2}$ , since it vanishes for all $u$ only if $x_{1} = x_{2}$ , while if $x_{1} \neq x_{2}$ then $u = (x_{1} - x_{2}, 0)$ gives $D G (x) (u) = 2 ∥ x_{1} - x_{2} ∥_{2}^{2} > 0$ ; hence $D G (x)$ has rank $1$ exactly on the complement of $Δ$ .

2.1step 1.2L4algebra

On the zero set the rank condition holds: if $G (x) = 0$ then $∥ x_{1} - x_{2} ∥_{2}^{2} = ℓ^{2} > 0$ , so $x_{1} \neq x_{2}$ and $D G (x)$ is surjective by step 1.2; and $G^{- 1} (0) \neq \emptyset$ , for instance $x_{1} = 0$ and $x_{2} = ℓ e_{1}$ give $G (x) = ℓ^{2} - ℓ^{2} = 0$ ; thus $0$ is a regular value of $G$ with nonempty level set.

3.1step 2.1L1L2L3algebra∎

By the regular level set theorem [L2], applied to the smooth map $G : R^{6} \to R$ with the regular value $0$ , the set $Q = G^{- 1} (0)$ is an embedded submanifold of $R^{6}$ of dimension $6 - 1 = 5$ ; by [L1] the rigid-rod branch therefore has $5 = 3 \cdot 2 - 1$ configuration degrees of freedom, in agreement with the identification of the same constraint in the cited treatment. With the masses $m_{1}, m_{2}$ , the pair consisting of $Q$ and the inclusion is a particle configuration whose mass matrix is $M = diag (m_{1} I_{3}, m_{2} I_{3})$ and whose mass metric is that of [L3]; the constraint function $G$ has dimension $ℓ^{2}$ , and rescaling it by any nonzero constant leaves both its zero set and the rank condition on that set unchanged, as recorded in [L1].

Remarks

The example exhibits both branches of Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator for the same two-particle model: without the rod the model uses the open domain $Q_{0}$ with the collision configurations excluded; with the rod it uses the five-dimensional embedded submanifold $Q$ . The two are alternatives of one model, not descriptions of one system at one time, and each would be paired with its own force law when the dynamics is adopted.
A constraint expressed as $∥ x_{1} - x_{2} ∥_{2} - ℓ = 0$ has the same zero set $Q$ and, on it, the same regular-value property, since $∥ x_{1} - x_{2} ∥_{2} = ℓ > 0$ there and the squared-distance function is smooth near $Q$ with nonzero gradient; the choice $G = ∥ x_{1} - x_{2} ∥_{2}^{2} - ℓ^{2}$ keeps the computation polynomial and is the one displayed. No physical claim depends on which of the two representative functions is used.

Configuration domains of two labeled particles: collision exclusion and a rigid rod as a regular holonomic constraint

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources