ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck 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.

The planar rolling disk: the holonomic constraint $x - a θ = c o n s t$ and the acceleration $f / (m + I / a^{2})$

Example

Let $a, m, I > 0$ and $f \in R$ , and consider the two-coordinate model

$G (x, θ) : = x - a θ, M : = (\begin{array}{cc} m & 0 \\ 0 & I \end{array}), Φ : = (f, 0),$

on $O : = R \times R^{2}$ , where $x$ is a centre coordinate and $θ$ an oriented spin. The constraint $G = 0$ is the ideal planar no-slip law of a disk of radius $a$ rolling in a straight line; $M$ is the adopted kinetic matrix (mass $m$ , spin inertia $I$ ), and $Φ$ the adopted applied force (force $f$ along $x$ , zero spin torque). Then:

$G$ is a regular holonomic constraint: $G_{q} = (1, - a)$ has rank one and its kernel is the line $R (a, 1)$ of virtual displacements. The associated differential constraint $x^{'} - a θ^{'} = 0$ is exact: on an interval it holds exactly when $x - a θ$ is constant, so in this planar straight-line case the rolling law is holonomic, and after translating $x$ the constant may be taken to be $0$ ;
if $q = (x, θ) : J \to R^{2}$ is a $C^{2}$ ideal-constraint motion of $(G, M, Φ)$ (A regular holonomic constraint, its virtual displacements and the ideal-reaction law), then the d'Alembert condition gives $(m x^{''} - f) a + I θ^{''} = 0$ , and differentiating the constraint twice gives $x^{''} = a θ^{''}$ ; hence

$(m + \frac{I}{a^{2}}) x^{''} = f, x^{''} = \frac{f a^{2}}{I + m a^{2}}, θ^{''} = \frac{a f}{I + m a^{2}};$

the multiplier of the motion is $λ = - \frac{f I}{I + m a^{2}}$ (uniquely determined), the reaction is $R = G_{q}^{T} λ = (λ, - a λ)$ with $∣ λ ∣ = ∣ f ∣ \frac{I}{I + m a^{2}} \leq ∣ f ∣$ , with strict inequality exactly when $f \neq 0$ , and the proposition The ideal holonomic system in a possibly time-dependent chart: explicit acceleration, constraint preservation, local existence and reaction power reproduces these numbers from $C = G_{q} M^{- 1} G_{q}^{T} = \frac{1}{m} + \frac{a^{2}}{I}$ and $Λ = - C^{- 1} G_{q} M^{- 1} Φ$ ;
for a uniform thin disk, $I = \frac{1}{2} m a^{2}$ and $x^{''} = \frac{2 f}{3 m}$ ; for a hoop (all mass at the rim), $I = m a^{2}$ and $x^{''} = \frac{f}{2 m}$ ;
the quadratic motion $x (t) = x_{0} + v_{0} t + \frac{f a^{2} t^{2}}{2 (I + m a^{2})}$ , $θ (t) = θ_{0} + ω_{0} t + \frac{a f t^{2}}{2 (I + m a^{2})}$ with $x_{0} = a θ_{0}$ and $v_{0} = a ω_{0}$ is an ideal-constraint motion with constant multiplier $λ$ , so the computed acceleration is realised by an explicit solution.

Facts & Assumptions

Given: The constants $a, m, I > 0$ and $f \in R$ , the constraint $G (x, θ) = x - a θ$ , the matrix $M = d i a g (m, I)$ , the force $Φ = (f, 0)$ , and an open interval $J$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) carrying a $C^{2}$ curve $q = (x, θ)$ .

[F1]

Constraint data ( $C^{k}$ Euclidean maps and diffeomorphisms, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, Submersions and immersions between Euclidean open sets): $G$ is $C^{\infty}$ on $R^{2}$ with gradient $G_{q} = (1, - a)$ ; since $1 \neq 0$ , $G_{q}$ has rank $1$ and is surjective onto $R$ ; and $M$ is symmetric positive definite with inverse $d i a g (m^{- 1}, I^{- 1})$ , while $Φ$ is a constant $C^{1}$ field (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[F2]

The ideal-constraint model (A regular holonomic constraint, its virtual displacements and the ideal-reaction law): a $C^{2}$ curve $q$ with $G (q (t)) = 0$ and permitted velocity $G_{q} (q (t)) q^{'} (t) = 0$ is an ideal-constraint motion of $(G, M, Φ)$ when there is a continuous $λ : J \to R$ with $M q^{''} = Φ + G_{q}^{T} λ$ ; for every such motion the reaction $R : = M q^{''} - Φ = G_{q}^{T} λ$ satisfies the d'Alembert condition $R \cdot δ = 0$ for every $δ \in \ker G_{q}$ .

[F3]

Kernel and virtual displacements (Linear map between vector spaces over the same field, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ): $δ \in \ker G_{q}$ means $δ_{x} - a δ_{θ} = 0$ , i.e. $δ = (a δ_{θ}, δ_{θ}) = δ_{θ} (a, 1)$ ; thus the kernel is the line spanned by $(a, 1)$ and is one-dimensional.

[F4]

Differentiation of the constraint: for a $C^{2}$ curve $q = (x, θ)$ the function $t \mapsto x (t) - a θ (t)$ is $C^{2}$ with second derivative $x^{''} - a θ^{''}$ (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral); equivalently $G_{q} q^{''} + G_{q q} [q^{'}, q^{'}] = x^{''} - a θ^{''}$ by the chain rule (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F5]

If a differentiable function on an interval has identically vanishing derivative, it is constant (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[F6]

The multiplier lemma (Reactions annihilating the virtual displacements are transpose multiples, with a positive definite multiplier matrix): the matrix $C : = G_{q} M^{- 1} G_{q}^{T}$ is symmetric positive definite and invertible (The transpose $A^{T}$ of a matrix, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ), and a vector $R$ orthogonal to $\ker G_{q}$ is $R = G_{q}^{T} λ$ for a unique $λ$ , namely $λ = C^{- 1} G_{q} M^{- 1} R$ .

[F7]

The chart proposition (The ideal holonomic system in a possibly time-dependent chart: explicit acceleration, constraint preservation, local existence and reaction power): with the present time-independent data it defines $Λ = - C^{- 1} [G_{q} M^{- 1} Φ + G_{t t} + 2 G_{t q} [v] + G_{q q} [v, v]]$ and states that the ideal-constraint motion with permitted velocity satisfies $M q^{''} = Φ + G_{q}^{T} Λ$ ; here all time derivatives of $G$ vanish.

Verification

technique · direct; compute the kernel, project the ideal equation onto the virtual displacement, differentiate the constraint twice and solve the resulting linear system, then check the multiplier against the proposition and exhibit the motion

1.1F1F3algebra

By [F1], $G$ is $C^{\infty}$ with $G_{q} = (1, - a)$ of rank one; the virtual displacements are the kernel of [F3], the line $R (a, 1)$ ; the velocity constraint $x^{'} - a θ^{'} = 0$ is exactly $G_{q} q^{'} = 0$ . This is the first assertion of part 1.

1.2F5algebra

Let $J \subseteq R$ be an interval and $q \in C^{1}$ . If $x^{'} - a θ^{'} = 0$ on $J$ , then the derivative of $t \mapsto x (t) - a θ (t)$ vanishes identically, so the function is constant on $J$ by [F5]; conversely a constant difference has derivative $0$ . Hence the differential constraint is equivalent to $x - a θ \equiv c$ , and replacing $x$ by $x - c$ (a translation of the coordinate origin) turns it into $G (x, θ) = x - a θ = 0$ . This is the second assertion of part 1.

1.3F2F3algebra

Let $q$ be an ideal-constraint motion. Then $M q^{''} - Φ = G_{q}^{T} λ$ and, by [F2], $(M q^{''} - Φ) \cdot δ = 0$ for every $δ \in \ker G_{q}$ . Taking the virtual displacement $δ = (a δ_{0}, δ_{0})$ , $δ_{0} \in R$ , and writing out $M q^{''} - Φ = (m x^{''} - f, I θ^{''})$ , gives $δ_{0} [(m x^{''} - f) a + I θ^{''}] = 0$ ; choosing $δ_{0} = 1$ yields $(m x^{''} - f) a + I θ^{''} = 0$ . This is the first equation of part 2.

1.4F4algebra

Since $G (q (t)) = x (t) - a θ (t)$ is identically zero and both $x$ and $θ$ are $C^{2}$ , its second derivative vanishes; by [F4] this second derivative is $x^{''} - a θ^{''}$ , so $x^{''} = a θ^{''}$ . This is the second relation of part 2.

2.1step 1.3step 1.4algebra

Substituting $x^{''} = a θ^{''}$ of step 1.4 into the identity $(m x^{''} - f) a + I θ^{''} = 0$ of step 1.3 gives $(m a^{2} + I) θ^{''} = a f$ , hence $θ^{''} = \frac{a f}{I + m a^{2}}$ and $x^{''} = a θ^{''} = \frac{f a^{2}}{I + m a^{2}}$ ; substituting $θ^{''} = x^{''} / a$ into $(m a^{2} + I) θ^{''} = a f$ and dividing by $a$ gives $(m + \frac{I}{a^{2}}) x^{''} = f$ . This is the chain of formulas of part 2.

3.1F2F6step 2.1algebra

Multiplier: from $M q^{''} = Φ + G_{q}^{T} λ$ in components, $m x^{''} = f + λ$ and $I θ^{''} = - a λ$ ; by step 2.1, $λ = m x^{''} - f = \frac{m f a^{2}}{I + m a^{2}} - f = - \frac{f I}{I + m a^{2}}$ , and then $- a λ = \frac{a f I}{I + m a^{2}} = I θ^{''}$ reproduces the second component. The uniqueness of $λ$ is [F6], applied to $R = M q^{''} - Φ$ , which is orthogonal to the kernel by [F2]; thus $λ$ is the unique multiplier of the motion and $∣ λ ∣ = ∣ f ∣ I / (I + m a^{2}) \leq ∣ f ∣$ , with equality when $f = 0$ and strict inequality when $f \neq 0$ , since $0 < I / (I + m a^{2}) < 1$ . This is the first assertion of part 3.

3.2step 2.1algebra

Constants: at $I = \frac{1}{2} m a^{2}$ , $x^{''} = \frac{f a^{2}}{\frac{1}{2} m a^{2} + m a^{2}} = \frac{f a^{2}}{\frac{3}{2} m a^{2}} = \frac{2 f}{3 m}$ ; at $I = m a^{2}$ , $x^{''} = \frac{f a^{2}}{2 m a^{2}} = \frac{f}{2 m}$ . This is part 4.

4.1F1F6F7step 2.1step 3.1algebra

Chart cross-check: by [F1], $G_{q} M^{- 1} G_{q}^{T} = \frac{1}{m} + \frac{a^{2}}{I} = \frac{I + m a^{2}}{m I} = C$ and $G_{q} M^{- 1} Φ = \frac{f}{m}$ , so [F7] gives $Λ = - C^{- 1} \frac{f}{m} = - \frac{m I}{I + m a^{2}} \cdot \frac{f}{m} = - \frac{f I}{I + m a^{2}}$ , and $M q^{''} = Φ + G_{q}^{T} Λ$ gives the same acceleration as step 2.1 and the same multiplier as step 3.1. This is the second assertion of part 3.

4.2F2step 2.1step 3.1algebra

Realisation: let $x_{0}, θ_{0}, v_{0}, ω_{0} \in R$ with $x_{0} = a θ_{0}$ and $v_{0} = a ω_{0}$ , put $c : = \frac{a f}{I + m a^{2}}$ and $x (t) : = x_{0} + v_{0} t + \frac{1}{2} a c t^{2}, θ (t) : = θ_{0} + ω_{0} t + \frac{1}{2} c t^{2} .$ Then $x (t) - a θ (t) = x_{0} - a θ_{0} + (v_{0} - a ω_{0}) t + 0 = 0$ , so the constraint holds; $q$ is $C^{\infty}$ with $x^{''} = a c$ , $θ^{''} = c$ , so $x^{''} = a θ^{''}$ ; the velocity is permitted because $G_{t} = 0$ and $x^{'} - a θ^{'} = 0$ ; and with $λ : = - \frac{f I}{I + m a^{2}}$ one has $f + λ = m x^{''}$ and $- a λ = I θ^{''}$ , so $M q^{''} = Φ + G_{q}^{T} λ$ . Hence $q$ is an ideal-constraint motion of $(G, M, Φ)$ with constant multiplier $λ$ , realising the acceleration of part 2. This is part 5.

5.1step 1.1step 1.2step 1.3step 1.4step 2.1step 3.1step 4.1step 3.2step 4.2∎

Parts 1-5 are proved.

Remarks

The model is the ideal planar no-slip law with an adopted kinetic matrix; the multiplier $λ$ computed in part 3, i.e. the component of the reaction $G_{q}^{T} λ = (λ, - a λ)$ , is the force the model requires along the line of rolling. Whether a real contact can supply that force (sufficient static friction in the contact, no deformation or rolling resistance) is an empirical condition on the apparatus, not a consequence of this mathematical development; when it fails, the no-slip constraint itself is not a valid model and the present equations do not apply.
The reduction to a single holonomic constraint uses that the disk rolls in a straight line with fixed vertical plane; the general three-dimensional rolling problem has velocity-dependent constraints that are not integrable in the same way, and no acceleration formula of the present form is asserted for it. The precise planar case is exactly the one identified in Section 5.7 of the cited textbook.
The multiplier is the model's constraint force and is not a measured quantity; only the reaction $G_{q}^{T} λ = (λ, - a λ)$ enters the equations, in agreement with the general scope note of A regular holonomic constraint, its virtual displacements and the ideal-reaction law.

The planar rolling disk: the holonomic constraint $x - a θ = c o n s t$ and the acceleration $f / (m + I / a^{2})$

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

The planar rolling disk: the holonomic constraint x−aθ=constx−aθ=const and the acceleration f/(m+I/a2)f/(m+I/a2)

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

The planar rolling disk: the holonomic constraint $x - a θ = c o n s t$ and the acceleration $f / (m + I / a^{2})$