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.

Dimension bookkeeping for the quantities and frame parameters of the framework page

Physical scope

A worked application of the dimension conventions of the framework to the quantities and frame parameters of this page: the dimensions of time and position coordinates, velocity, acceleration, mass, the mass operator, the Galilean parameters and the displayed transformation laws are computed from the convention rules and checked for consistency. The item asserts no measured value and no law of nature; it is bookkeeping inside the stated conventions.

Example

Apply the dimension conventions of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework to the quantities of this page and to the parameters of the frame transformations of Inertial frames, stationary observers and the adopted Galilean transformations between frames: the time coordinate $t$ , the spatial coordinates $x_{i}$ , the worldline parameter, the coordinate velocity $w$ and acceleration $a$ of Coordinate velocity and acceleration of a worldline in an inertial frame, and the spatial velocity and acceleration vectors, the masses $m_{i}$ and the mass operator, the parameters $b, a_{0}, v, R$ of a Galilean transformation, the quantities transformed in the laws $t^{'} = t + b$ , $x^{'} = R x + v t + a_{0}$ , $w^{'} = R w + v$ , $a^{'} = R a$ of Galilean transformation of worldlines: velocity and acceleration laws, frame-independence of zero coordinate acceleration, and the group of frame changes, and the frequency $ω$ and coordinates $y$ of the rotating-basis example of the page.

For the rotating-coordinate bookkeeping, let $s \in R$ be time, let $ω > 0$ be a scalar frequency with $[ω] = τ^{- 1}$ , put $ω = (0, 0, ω)$ , and let $y : R \to R^{3}$ be a $C^{2}$ coordinate curve whose components have dimension $ℓ$ . For the constraint bookkeeping define, independently, $G : (R^{3})^{2} \to R$ by $G (x_{1}, x_{2}) = \sum_{j = 1}^{3} ((x_{1})_{j} - (x_{2})_{j})^{2} - h^{2}$ , with a fixed length $h > 0$ . These local formulas specify the objects whose dimensions are checked; no result about their motions or level sets is borrowed from a sibling example. Cross products use the explicit component formula of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework.

Facts & Assumptions

Given: The dimension symbols $ℓ, τ, μ$ and the rules $[X Y] = [X] [Y]$ , $[X / Y] = [X] [Y]^{- 1}$ , $[d X / d u] = [X] [u]^{- 1}$ , together with the requirements that a sum is formed only from equal dimensions and that $[t] = τ$ , $[x_{i}] = ℓ$ , $[m] = μ$ , $[R_{i j}] = 1$ (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework).

[L1]

Dimensions of the frame parameters: $[b] = τ$ , $[(a_{0})_{i}] = ℓ$ , $[v_{i}] = ℓ τ^{- 1}$ and $[R_{i j}] = 1$ ; the transformation laws are $t^{'} = t + b$ , $x^{'} = R x + v t + a_{0}$ , $w^{'} = R w + v$ and $a^{'} = R a$ (Inertial frames, stationary observers and the adopted Galilean transformations between frames, Galilean transformation of worldlines: velocity and acceleration laws, frame-independence of zero coordinate acceleration, and the group of frame changes).

[L2]

Coordinate velocity and acceleration: $w = x_{γ}^{'}$ and $a = x_{γ}^{''}$ for the coordinate curve $x_{γ}$ of a worldline in a frame, whose parameter is the frame time (Coordinate velocity and acceleration of a worldline in an inertial frame, and the spatial velocity and acceleration vectors, Particle labels, worldlines, the frame-time parameter condition and fixed inertial masses).

[L3]

The mass operator multiplies the spatial components of a position tuple by the masses $m_{i}$ (Configuration domain of $N$ labeled particles: open admissible sets, regular holonomic constraints and the mass operator).

Verification

Proof technique: direct; evaluate the dimension rules on each displayed quantity and combine.

1.1givenalgebra

The time coordinate and worldline parameter have dimension $[t] = τ$ and the spatial coordinates $[x_{i}] = ℓ$ by the conventions; the dimension of a bilinear product of two quantities is the product of their dimensions, since each component of the product is a sum of products of components to which the rule $[X Y] = [X] [Y]$ applies.

2.1step 1.1L2algebra

The coordinate velocity has $[w] = [d x_{γ} / d t] = ℓ τ^{- 1}$ and the coordinate acceleration $[a] = [d w / d t] = ℓ τ^{- 2}$ , by the derivative rule and step 1.1.

3.1step 2.1L3algebra

The masses have $[m_{i}] = μ$ , so the mass operator has dimension $μ$ by [L3]; the momentum $p = m w$ has $[p] = μ ℓ τ^{- 1}$ and the product $m a$ has $[m a] = μ ℓ τ^{- 2}$ , both being products of the displayed dimensions.

3.2step 2.1L1algebra

The frame parameters have the dimensions of [L1]; each law of [L1] is dimensionally consistent: $[t^{'}] = [t + b] = τ$ because $[t] = [b] = τ$ ; in $x^{'} = R x + v t + a_{0}$ the three summands have dimensions $ℓ$ , $ℓ τ^{- 1} \cdot τ = ℓ$ and $ℓ$ ; $[w^{'}] = [R w + v] = ℓ τ^{- 1}$ because $[R w] = ℓ τ^{- 1}$ and $[v] = ℓ τ^{- 1}$ ; and $[a^{'}] = [R a] = ℓ τ^{- 2}$ .

4.1step 3.2algebra

For the locally specified rotating-basis coordinates $y$ and the angular speed $ω > 0$ measured in radians per second, $[ω] = τ^{- 1}$ under the radian convention, and the two cross-product expressions are consistent with the acceleration: $[ω \times y] = τ^{- 1} ℓ = ℓ τ^{- 1} = [y^{'}]$ and $[ω \times (ω \times y)] = τ^{- 2} ℓ = ℓ τ^{- 2} = [y^{''}]$ , where each component of a cross product is a sum of products of two components, so its dimension is the product of the dimensions.

5.1step 4.1algebra∎

Finally the locally defined two-particle constraint function has dimension $ℓ^{2}$ ; the level equation $G (x) = 0$ relates a quantity of dimension $ℓ^{2}$ to the number $0$ , which is admissible because $0$ is the neutral element of addition in every dimension, and multiplying $G$ by a nonzero constant of any fixed dimension produces the same zero set with the same ranks of $D G$ on it, as recorded with the definition of the configuration stage; all quantities and laws of this page are therefore dimensionally consistent under the stated conventions.

Remarks

The check is bookkeeping inside the conventions of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework: it does not test any physical equation, because the framework at this stage has adopted no force law and no equation of motion. Its role is to make the dimensional readings of the framework's quantities explicit before later pages combine them.
The dimension of the generalized coordinates of the constrained branch is fixed by the model of the constraint, not by the ambient positions: on a configuration manifold a generalized coordinate may carry any declared dimension, and the dimensions of its velocity and momentum then follow by the same rules; the conventions of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework record this together with the rule that only equal dimensions are added.

Dimension bookkeeping for the quantities and frame parameters of the framework page

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources