Pipeline-generated

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.

Poincare semidirect group, dual pairing and moment components

1 · Prerequisites

2 · Summary

This page fixes the proper orthochronous Poincare semidirect product, the cotangent and dual-charge sign conventions, and the translation and Lorentz moment components. It derives their algebra and conditional shell descent, identifies the massive spinless and positive classical-spin KKS orbits, and develops local Hamilton-Jacobi solutions and complete-integral coordinates. For these Hamilton-Jacobi families, a caustic is a point where the characteristic projection loses local invertibility. Physical consequences are conditional on the separately stated free-action or optional spinning-orbit model postulates. Sources using natural units or the opposite metric signature are translated explicitly. The page asserts neither quantum spin classification nor global Hamilton-Jacobi continuation through such points.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

DefinitionDefinition: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Poincare semidirect group, dual pairing and moment components

Definition

Assume ${A C}_{ω}$ for the referenced cotangent and symplectic-action conventions. Work on affine Minkowski spacetime with inertial coordinates $x^{0} = c t, x^{1}, x^{2}, x^{3}$ in metres, metric matrix $η = diag (- 1, 1, 1, 1)$ , and cotangent coordinates $(x^{a}, p_{a})$ , where each $p_{a}$ has SI momentum units. Fix the future cone as the timelike component containing the positive $x^{0}$ axis, equivalently $v^{0} > ∣ v ∣$ . Let $S O^{+} (1, 3)$ denote the determinant-one, future-cone-preserving Lorentz subgroup. Define the proper orthochronous Poincaré group and its multiplication by

$G = R^{4} ⋊ S O^{+} (1, 3), (a, Λ) (b, L) = (a + Λ b, Λ L) .$

Its action on spacetime and the cotangent lift are $x^{'} = Λ x + a$ and $p^{'} = Λ^{- T} p$ . The Lie algebra consists of pairs $(a, A)$ with $A^{T} η + η A = 0$ , bracket

$[(a, A), (b, B)] = (A b - B a, [A, B]) .$

Use the library convention $ξ_{M} = {\frac{d}{d s} ∣}_{0} \exp_{G} (- s ξ) \cdot z$ . Thus the positive affine generator on spacetime is $Y_{(a, A)} (x) = a + A x$ , the fundamental field is its negative, and the cotangent-lifted positive field is $(a + A x, - A^{T} p)$ . Pair the cotangent point with a Lie-algebra element by

$ℓ_{(a, A)} (x, p) = p_{b} (a^{b} + A^{b}_{c} x^{c}) .$

Define $P^{a} = η^{a b} p_{b}$ and $J^{a b} = x^{a} P^{b} - x^{b} P^{a}$ . The equivalent dual pairing is $ℓ_{(a, A)} = p_{b} a^{b} - \frac{1}{2} J_{b c} A^{b c}$ , where $A^{b c} = A^{b}_{d} η^{d c}$ and $J_{b c} = η_{b d} η_{c e} J^{d e}$ . Here $[P^{a}] = k g m / s$ and $[J^{a b}] = J s$ . These are charge-space definitions on the full cotangent bundle; shell reduction and the moment-map identities are stated separately. No spin or particle model is included.

Facts & Assumptions

Given: The Lorentz metric convention, an inertial affine chart, and the cotangent phase-space data specified above.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only; no full axiom of choice is used.

[F1]

The proper orthochronous Lorentz group: boosts, rotations, unique factorization and invariants: $S O^{+} (1, 3)$ is the determinant-one Lorentz subgroup preserving the selected future cone.

[L1]

Cotangent phase data, observables and action dimensions: the current H0 draft defines finite-dimensional $T^{*} Q$ with $θ = p_{i} d q^{i}$ , $ω = - d θ = d q^{i} \land d p_{i}$ , and ${A C}_{ω}$ only. Its H25 Step 1 record is ready and hash-current; that records readiness but is not independent proof approval. The carrier remains status draft with no pipeline_run binding; its definition and sign interface match here, and proof provenance is not-applicable.

[F2]

Symplectic and Hamiltonian Lie-group actions: the Lie-algebra dual is the space of linear functionals $g^{*} = L (g, R)$ ; the library uses $ξ_{M} (z) = {\frac{d}{d s} ∣}_{0} \exp (- s ξ) \cdot z$ and $d μ^{ξ} = - ι_{ξ_{M}} ω$ .

[F3]

A regular level set is an embedded submanifold: a nonempty regular level of a smooth map between finite-dimensional manifolds is an embedded submanifold of codimension the target dimension.

[F4]

The timelike set has exactly two convex components, described in orthonormal coordinates: in an orthonormal inertial chart the timelike set has exactly two connected components $T_{+}$ and $T_{-}$ ; the chosen future cone is the component containing the positive time axis, and every invertible Lorentz map carries each component onto one component.

[F5]

The Lie algebra of eta-antisymmetric endomorphisms, its generators and commutators: the derivatives at identity of $C^{1}$ curves in $O (1, 3)$ satisfy $A^{T} η + η A = 0$ , and this condition defines a six-dimensional linear subspace closed under the matrix commutator.

Proof

technique · direct

Given: $η = diag (- 1, 1, 1, 1)$ , the selected time orientation, affine action, cotangent convention, and [F1]–[F4].

1.1F3algebra

On $G L (4, R)$ define $Φ (L) = L^{T} η L$ with values in the ten-dimensional space of symmetric matrices. At $Φ (L) = η$ , its derivative is $D Φ_{L} (Δ) = Δ^{T} η L + L^{T} η Δ$ . For any symmetric $S$ , set $Δ = L η^{- 1} S / 2$ ; using $L^{T} η L = η$ and $S^{T} = S$ , each summand equals $S / 2$ . Thus $D Φ_{L}$ is onto.

2.1F1F3F4step 1.1algebra

Every point of $Φ^{- 1} (η)$ is regular by step 1.1, and the level is nonempty because it contains $I$ . Thus [F3] makes $O (1, 3) = Φ^{- 1} (η)$ an embedded six-dimensional submanifold of $G L (4, R)$ . For $L \in O (1, 3)$ , $L e_{0}$ is timelike and $L$ is a homeomorphism of the timelike set; [F4] implies that $L$ preserves the selected future component exactly when $L e_{0}$ lies in that component. Since $e_{0}$ is the positive time-axis vector, this is exactly $L^{0}_{0} > 0$ . Also $∣ L^{0}_{0} ∣ \geq 1$ , and taking determinants in $L^{T} η L = η$ gives $(\det L)^{2} = 1$ . Therefore $\det L = 1$ and $L^{0}_{0} > 0$ select an open subset of $O (1, 3)$ . By [F1] this subset is $S O^{+} (1, 3)$ . Matrix multiplication and inversion restrict smoothly from $G L (4)$ , so this subgroup is a six-dimensional Lie group.

3.1F5step 2.1algebra

Give $G = R^{4} \times S O^{+} (1, 3)$ the product manifold structure from step 2.1 and multiplication $(a, Λ) (b, L) = (a + Λ b, Λ L)$ . Both parenthesizations of a triple product equal $(a + Λ b + Λ L c, Λ L M)$ ; the identity is $(0, I)$ ; and direct substitution shows $(- Λ^{- 1} a, Λ^{- 1})$ is a left and right inverse. Multiplication and inversion are smooth because matrix multiplication and inversion on $S O^{+} (1, 3)$ are smooth and the translation operations are smooth. The affine matrix map $ρ (a, Λ) = (\begin{array}{cc} Λ & a \\ 0 & 1 \end{array})$ is injective, has smooth inverse onto its image by block projection, and is a group homomorphism because matrix multiplication gives $ρ (a + Λ b, Λ L)$ . The product manifold tangent at identity is $R^{4} \times T_{I} S O^{+} (1, 3)$ . By [F5], the latter tangent space is contained in the six-dimensional space of matrices satisfying $A^{T} η + η A = 0$ ; both have dimension six by step 2.1 and [F5], so they are equal. Hence $d ρ_{I} (a, A) = (\begin{array}{cc} A & a \\ 0 & 0 \end{array})$ . A group homomorphism carries left-invariant vector fields to related left-invariant fields: differentiating $ρ \circ L_{g} = L_{ρ (g)} \circ ρ$ gives this relation. Related fields' brackets are related, since applying each bracket to a smooth test function and expanding $X (Y f) - Y (X f)$ gives the same identity after composition with $ρ$ . For matrices $M, N$ , the left-invariant fields on $G L (5)$ are $g \mapsto g M$ and $g \mapsto g N$ ; differentiating these fields gives their commutator at the identity as $M N - N M$ . Thus the bracket of two pair matrices is $(\begin{array}{cc} [A, B] & A b - B a \\ 0 & 0 \end{array})$ , yielding $[(a, A), (b, B)] = (A b - B a, [A, B])$ .

4.1L1F2A1step 3.1algebra

The cotangent lift preserves the covector-tangent pairing: $p^{'} (d x^{'}) = (Λ^{- T} p) (Λ d x) = p (d x)$ . For the one-parameter element $\exp (- s (a, A))$ , differentiation of $x^{'} = Λ_{s} x + a_{s}$ gives the fundamental field $(- (a + A x), A^{T} p)$ on $(x, p)$ ; its negative is the positive cotangent-lifted field $(a + A x, - A^{T} p)$ . Pairing the covector with the positive base generator gives $ℓ = p_{b} (a^{b} + A^{b}_{c} x^{c})$ .

5.1L1step 4.1algebra∎

Antisymmetry of $A^{b c}$ gives $J_{b c} A^{b c} = - 2 p_{b} A^{b}_{c} x^{c}$ : expand $J_{b c} = x_{b} p_{c} - x_{c} p_{b}$ and interchange $b, c$ in the first term. Substitution yields $ℓ = p_{b} a^{b} - \frac{1}{2} J_{b c} A^{b c}$ . The definitions of $P, J$ then give $[P^{a}] = k g m / s$ and $[J^{a b}] = J s$ from $[x] = m$ , $[p] = k g m / s$ , and $[c] = m / s$ .

DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

First-class closure for a regular constraint family

Definition

Assume ${A C}_{ω}$ as in Regular primary constraints and total generator. Let $(P, ω)$ be a smooth symplectic manifold. For every smooth real function $F$ on an open set $U \subseteq P$ , define its Hamiltonian vector field $X_{F}$ by $ω_{z} (X_{F} (z), v) = d F_{z} (v)$ for every $z \in U$ and $v \in T_{z} P$ , and define ${F, G} : = d F (X_{G})$ . Nondegeneracy of $ω$ makes $X_{F}$ unique; in local coordinates its coefficients are obtained by inverting the smooth nonsingular matrix of $ω$ , so $X_{F}$ and the bracket are smooth. Let $χ_{1}, \dots, χ_{r} \in C^{\infty} (U, R)$ be a regular constraint family on the common zero surface $N = {z \in U : χ_{a} (z) = 0 for all a}$ as defined by Regular primary constraints and total generator: the differentials $d χ_{a}$ are linearly independent at every point of $N$ . The family is first-class on $N$ when

${χ_{a}, χ_{b}} (z) = 0 for every z \in N and all a, b .$

Equivalently, each pairwise bracket is weakly zero in the notation $F \approx 0$ of Regular primary constraints and total generator. On a canonical cotangent phase space this intrinsic convention agrees with Canonical Poisson brackets and local Hamiltonian flow: ${F, G} = F_{q^{i}} G_{p_{i}} - F_{p_{i}} G_{q^{i}}$ . This definition is a pointwise closure condition on the stated regular surface; it does not assert multiplier-algorithm termination or global quotient regularity.

TheoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Local Hamilton-Jacobi solution by invertible characteristics

Statement

Assume ${A C}_{ω}$ . Let $H \in C^{\infty} (U, R)$ on an open set $U \subset R \times T^{*} R^{n}$ , with coordinates $(t, q, p)$ , and let $S_{0} \in C^{\infty} (Q_{0}, R)$ on an open $Q_{0} \subset R^{n}$ . The Hamilton characteristic ODE is ${\dot{q}}^{i} = \partial H / \partial p_{i}$ and ${\dot{p}}_{i} = - \partial H / \partial q^{i}$ . For a covector $p$ and vector $v$ in the canonical coordinates, write $p \cdot v : = \sum_{i} p_{i} v^{i}$ . For each $a_{0} \in Q_{0}$ such that $(0, a_{0}, d S_{0} (a_{0})) \in U$ , there are neighbourhoods of $(0, a_{0})$ and a time interval on which this ODE with $q (0, a) = a$ , $p (0, a) = d S_{0} (a)$ has a smooth solution and $(t, a) \mapsto (t, q (t, a))$ is a diffeomorphism onto its image after restriction. On that image the function

$S (t, q (t, a)) = S_{0} (a) + \int_{0}^{t} [p (u, a) \cdot \dot{q} (u, a) - H (u, q (u, a), p (u, a))] d u$

is smooth, has initial value $S_{0}$ , and satisfies $S_{t} + H (t, q, S_{q}) = 0$ . The claim is local to the invertible projection domain; it asserts no continuation beyond a point where the characteristic projection loses invertibility. For the SI interpretation, assign $S_{0}$ action units $J s$ as well as assigning $t, q, p, H$ SI time, length, momentum, and energy units. Then both $S_{0}$ and the integral have action units, so $[S] = J s$ , $[S_{q}] = [p]$ , and $[S_{t}] = J$ .

Facts & Assumptions

Given: The smooth Hamiltonian and initial exact graph in the statement, with the initial point $(0, a_{0}, d S_{0} (a_{0}))$ in $U$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only for the cotangent-bundle suppliers; no full axiom of choice is used.

[L1]

Canonical Poisson brackets and local Hamiltonian flow: the current H0 draft states $ι_{X_{H}} ω = d H$ , ${F, G} = F_{q} G_{p} - F_{p} G_{q}$ , local unique Hamilton solutions with smooth dependence on their actual domain, and no completeness claim. Its H25 Step 1 record is ready and hash-current, but that is not independent proof approval; the carrier remains draft/unbound with ai-altered proof provenance. Its sign and local-flow interface match the proof.

[F1]

Smooth dependence of ODE solutions on parameters: a smooth finite-dimensional ODE vector field has jointly smooth local solutions in time and parameters near each initial datum, on a common sufficiently short interval after restricting the parameter neighbourhood.

[F2]

Choice-free smooth inverse function theorem in Euclidean space: a smooth map with invertible derivative at a point is a smooth diffeomorphism between suitable neighbourhoods of that point and its image.

Proof

technique · direct characteristics and endpoint action

Given: The hypotheses of the statement and the exact conditional Hamiltonian-flow interface [L1].

1.1L1F1A1givenalgebra

The map $a \mapsto (0, a, d S_{0} (a))$ is continuous. Since its value at $a_{0}$ lies in the open set $U$ , it stays in $U$ for all $a$ in a sufficiently small neighborhood of $a_{0}$ . The characteristic vector field is $(H_{p}, - H_{q})$ by [L1] and is smooth on $U$ ; hence the ODE existence and parameter theorem [F1] supplies smooth $q (t, a), p (t, a)$ near $(0, a_{0})$ for these initial graph data. At $t = 0$ , $D_{a} q = I$ .

1.2L1A1algebra

Define $\tilde{S} (t, a)$ by the integral in the statement. Differentiating with respect to $a$ and integrating the $p \cdot \partial_{a} \dot{q}$ term by parts yields $\partial_{a} \tilde{S} = d S_{0} (a) + p (t, a) D_{a} q (t, a) - p (0, a) D_{a} q (0, a) + \int_{0}^{t} [- \dot{p} - H_{q}] D_{a} q + [\dot{q} - H_{p}] D_{a} p d u .$ The initial terms cancel because $p (0, a) = d S_{0} (a)$ and $D_{a} q (0, a) = I$ ; both integrands vanish by Hamilton's equations [L1]. Thus $\partial_{a} \tilde{S} = p (t, a) D_{a} q (t, a)$ .

2.1step 1.1F2algebra

The derivative of $(t, a) \mapsto (t, q (t, a))$ at $(0, a_{0})$ is block triangular with diagonal blocks $1$ and $I$ , so is invertible. [F2] gives a smooth local inverse $a = a (t, q)$ ; restrict to its image, which is the actual projection domain.

3.1step 1.2algebragiven∎

Differentiating the endpoint integral in time gives $\partial_{t} \tilde{S} = p \cdot \dot{q} - H$ , by the fundamental theorem of calculus. Put $S (t, q) = \tilde{S} (t, a (t, q))$ . The chain rule and step 1.2 give $S_{q} = p$ ; at fixed $q$ , the inverse relation $q (t, a (t, q)) = q$ gives $D_{a} q \partial_{t} a = - \dot{q}$ . Thus $S_{t} = (p \cdot \dot{q} - H) + p D_{a} q \partial_{t} a = (p \cdot \dot{q} - H) - p \cdot \dot{q} = - H$ . Therefore $S_{t} + H (t, q, S_{q}) = 0$ . At $t = 0$ , the integral is zero and $q = a$ , so $S (0, q) = S_{0} (q)$ .

TheoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Poincare cotangent moment map and full generator algebra

Statement

Assume ${A C}_{ω}$ . For the group and cotangent conventions of Poincare semidirect group, dual pairing and moment components, the map $μ : T^{*} R^{4} \to g^{*}$ defined by $⟨ μ (x, p), (a, A) ⟩ = ℓ_{(a, A)} (x, p)$ is a smooth equivariant moment map and obeys

${ℓ_{ξ}, ℓ_{η}} = ℓ_{[ξ, η]}, {P^{a}, P^{b}} = 0, {J^{a b}, P^{c}} = η^{a c} P^{b} - η^{b c} P^{a},$

${J^{a b}, J^{c d}} = η^{a c} J^{b d} - η^{a d} J^{b c} - η^{b c} J^{a d} + η^{b d} J^{a c} .$

For shell coordinates write $p = (p_{1}, p_{2}, p_{3})$ and $∣ p ∣^{2} : = p_{1}^{2} + p_{2}^{2} + p_{3}^{2}$ . For each future massive shell with $m > 0$ in kg, $c > 0$ in m/s, $p_{0} = - E / c$ , and $E = \sqrt{m^{2} c^{4} + c^{2} ∣ p ∣^{2}}$ , or nonzero future null shell with $m = 0$ and $∣ p ∣ > 0$ , its Poincare charges descend to the global quotient by complete characteristic lines of the shell constraint. For vectors $u, v \in R^{4}$ , define $(u \land v)^{a b} : = u^{a} v^{b} - u^{b} v^{a}$ . The induced dual action is $(P, J) \mapsto (Λ P, Λ J Λ^{T} + a \land Λ P)$ . On the fixed-time slice $x^{0} = c t$ , with physical position $q^{i} = x^{i}$ , the boost component $B_{i} = J^{0 i} = c t p_{i} - q^{i} E / c$ is explicitly time dependent and satisfies $\partial_{t} B_{i} + {B_{i}, E} = 0$ . These are mathematical identities; conservation is conditional on the stated free-shell evolution.

Facts & Assumptions

Given: The affine Poincaré action, cotangent phase space, and Poisson sign convention of Poincare semidirect group, dual pairing and moment components and the exact conditional suppliers below.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only; no full axiom of choice is used.

[F1]

Poincare semidirect group, dual pairing and moment components: $Y_{(a, A)} = a + A x$ , $ℓ_{(a, A)} = p_{b} (a^{b} + A^{b}_{c} x^{c})$ , $P^{a} = η^{a b} p_{b}$ , and $J^{a b} = x^{a} P^{b} - x^{b} P^{a}$ .

[L1]

Canonical Poisson brackets and local Hamiltonian flow: the current H0 draft states ${F, G} = F_{x} G_{p} - F_{p} G_{x}$ , $ι_{X_{H}} ω = d H$ , and local flow only on the open solution domain. Its H25 Step 1 record is ready and hash-current, but the draft carrier has no pipeline_run binding and its ai-altered proof has no independent proof approval. Its coordinate convention matches the proof.

[F2]

The cotangent lift of an action is Hamiltonian with the tautological moment map: for the cotangent lift and the library $\exp (- s ξ)$ convention, $μ^{ξ} = - p (ξ_{Q})$ satisfies $d μ^{ξ} = - ι_{ξ_{T^{*} Q}} ω$ and the cotangent-lift map is coadjoint equivariant.

[L2]

Flat future mass shell has an explicit global orbit quotient: the current H8 draft states the future-shell equation $- p_{0} = P^{0} = \sqrt{m^{2} c^{2} + ∣ p ∣^{2}}$ , complete affine-line flow, global $(a, p)$ quotient, reduced form $d a^{i} \land d p_{i}$ , and nonzero-null restriction. Its statement and dependencies match the H25 manifest. Its Step 1 record is ready/hash-current, but the carrier is still draft and unbound to pipeline_run, so this is not independent proof approval.

[L3]

Free shell in inertial time has the square-root Hamiltonian: the current H8 draft states $p_{0} = - E / c$ , $E = \sqrt{m^{2} c^{4} + c^{2} ∣ p ∣^{2}}$ , $q = a + t E_{p}$ , and $\dot{q} = c^{2} p / E$ , $\dot{p} = 0$ on $x^{0} = c t$ . The supplier is a mathematical deduction within its stated chart, positive-root and nonzero-null hypotheses; it introduces no physical action adoption.

Proof

technique · direct cotangent moment map and canonical differentiation

Given: The library sign conventions, [F1], and the exact conditional shell statements [L1]–[L3].

1.1F1F2L1A1algebra

For $ξ = (a, A)$ the cotangent lift has positive infinitesimal field $(a + A x, - A^{T} p) = - ξ_{T^{*} Q}$ because the library fundamental vector is generated by $\exp (- s ξ)$ . With $ω = d x^{a} \land d p_{a}$ , $ι_{X_{ℓ_{ξ}}} ω = d ℓ_{ξ}$ by [L1], as $\partial_{p} ℓ = a + A x$ and $- \partial_{x} ℓ = - A^{T} p$ . Therefore $d ℓ_{ξ} = - ι_{ξ_{T^{*} Q}} ω$ . The cotangent lift is symplectic and equivariant by [F2], so $μ$ is the claimed equivariant moment map.

1.2F1L1algebra

Substituting $P^{a} = η^{a b} p_{b}$ and $J^{a b} = x^{a} P^{b} - x^{b} P^{a}$ into [L1]'s canonical bracket, Leibniz gives ${P^{a}, P^{b}} = 0$ and ${J^{a b}, P^{c}} = η^{a c} P^{b} - η^{b c} P^{a}$ . Applying Leibniz to the four products in ${J^{a b}, J^{c d}}$ gives the four displayed metric terms, with signs fixed by ${x^{a}, p_{b}} = δ_{b}^{a}$ .

1.3F1algebra

The full dual action follows directly from the semidirect group law, without restricting to the cotangent moment-map image. For $g = (a, Λ)$ , multiplication and inversion give ${Ad}_{g} (b, B) = (Λ b - Λ B Λ^{- 1} a, Λ B Λ^{- 1})$ , hence ${Ad}_{g^{- 1}} (b, B) = (Λ^{- 1} (b + B a), Λ^{- 1} B Λ)$ . For an arbitrary dual charge $(P, J)$ use the pairing in [F1], $⟨ (P, J), (b, B) ⟩ = P_{b} b^{b} - \frac{1}{2} J_{b c} B^{b c}$ , and define $g \cdot (P, J)$ by pairing with ${Ad}_{g^{- 1}} (b, B)$ . Lorentz invariance of $η$ transforms the first term to $P_{b}^{'} b^{b} + P_{b}^{'} B^{b}_{c} a^{c}$ , where $P^{'} = Λ P$ , and the second term to $- \frac{1}{2} (Λ J Λ^{T})_{b c} B^{b c}$ . Antisymmetry gives $P_{b}^{'} B^{b}_{c} a^{c} = - \frac{1}{2} (a \land P^{'})_{b c} B^{b c}$ . Thus for every $(b, B)$ the pairing equals that of $(Λ P, Λ J Λ^{T} + a \land Λ P)$ ; uniqueness of the dual coordinates proves the formula on all of $g^{*}$ . For cotangent-image charges it also agrees with $x^{'} = Λ x + a$ , $p^{'} = Λ^{- T} p$ , and $J^{'} = x^{'} \land P^{'}$ , as required by equivariance.

1.4F1L2L1algebra

On either future shell, the characteristic shift changes $J$ by $α P \land P = 0$ and leaves $P$ fixed, so each charge is constant on quotient fibres. In H8 coordinates $(a, p)$ the descended $P$ and $J$ are explicit smooth functions, so they descend smoothly through the quotient of [L2]. Lorentz invariance of $p^{2}$ gives ${ℓ_{ξ}, C_{m}} = 0$ for Lorentz generators; translations are constants in flat spacetime, so their brackets with $C_{m}$ also vanish.

2.1F1L1step 1.1algebra

For $η = (b, B)$ , the canonical bracket gives ${ℓ_{ξ}, ℓ_{η}} = p \cdot A (b + B x) - p \cdot B (a + A x) = p \cdot (A b - B a + [A, B] x) = ℓ_{[(a, A), (b, B)]},$ using the semidirect Lie bracket from [F1]. This proves the full dual generator identity.

3.1F1L2L3algebra∎

At $x^{0} = c t$ , $P^{0} = E / c$ , hence $B_{i} = J^{0 i} = c t p_{i} - q^{i} E / c$ . With the reduced canonical bracket from [L2]–[L3], ${B_{i}, E} = - c p_{i}$ and $\partial_{t} B_{i} = c p_{i}$ . Their sum is zero, so $B_{i}$ is conserved along the free reduced motion, with the partial-time term essential.

TheoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Positive classical spin Poincare orbit and stabilizer jump

Statement

Assume ${A C}_{ω}$ . Let $G = R^{4} ⋊ S O^{+} (1, 3)$ act coadjointly on the dual charge space of Poincare semidirect group, dual pairing and moment components. At a charge point $(P^{a}, J^{a b})$ , define $P_{b} : = η_{b a} P^{a}$ , $J_{c d} : = η_{c e} η_{d f} J^{e f}$ , and $P^{2} : = η_{a b} P^{a} P^{b}$ . Let $ε_{a b c d}$ be the totally antisymmetric Minkowski volume tensor with $ε_{0123} = + 1$ ; raising all indices with $η = diag (- 1, 1, 1, 1)$ gives $ε^{0123} = - 1$ . Define the algebraic vector $W^{a} : = \frac{1}{2} ε^{a b c d} P_{b} J_{c d}$ , and write $W^{2} : = η_{a b} W^{a} W^{b}$ and $W \cdot P : = η_{a b} W^{a} P^{b}$ . For fixed mass $m > 0$ in kg, angular-momentum parameter $s > 0$ in kg m $^{2}$ /s, and $c > 0$ in m/s, take the rest charge point with $P^{a} = (m c, 0, 0, 0)$ and $J^{12} = s$ , all other independent components of $J$ being zero. Its coadjoint orbit is an eight-dimensional smooth symplectic manifold with its KKS form. On this orbit, $P^{2} = - m^{2} c^{2}$ , $P$ is future, $W \cdot P = 0$ , and $W^{2} = m^{2} c^{2} s^{2}$ . The exact joint invariant set with these values is this one orbit. At $s = 0$ the rest stabilizer has dimension four and the spinless orbit has dimension six; no smoothness claim is made for a larger union of Casimir level sets.

Facts & Assumptions

Given: The proper orthochronous Poincaré group and charge pairing, $m > 0$ , $s > 0$ , and the rest representative in the statement.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only; no full axiom of choice is used.

[F1]

Poincare semidirect group, dual pairing and moment components: the Poincaré group is a ten-dimensional Lie group with semidirect bracket and dual translation/antisymmetric Lorentz charges $(P, J)$ ; here $P_{b} = η_{b a} P^{a}$ and $J_{c d} = η_{c e} η_{d f} J^{e f}$ are lowered with $η$ .

[L1]

Poincare cotangent moment map and full generator algebra: the current assigned A draft states the affine coadjoint action (P,J)->(Lambda P,Lambda J Lambda^T+a wedge Lambda P) and the charge map with the exp(-s xi) convention. The carrier exists as this batch-26 draft, but its H0/H8 inputs and proof review remain unresolved.

[F2]

Coadjoint orbits are symplectic manifolds: under ${A C}_{ω}$ , every coadjoint orbit has the canonical smooth homogeneous-space structure and the KKS form is smooth, closed, nondegenerate, with $ω_{β} (ξ_{O}, η_{O}) = β ([ξ, η])$ .

Proof

technique · rest-frame classification and stabilizer calculation

Given: The rest covector and exact coadjoint action conditional on [L1].

1.1F1L1algebra

In the rest frame $P = (m c, 0)$ , the spatial components of $W$ are the three independent duals of $J^{i j}$ , multiplied by the nonzero factor $m c$ . Thus $∣ W ∣ = m c s$ and $W^{0} = 0$ , so $W \cdot P = 0$ and $W^{2} = m^{2} c^{2} s^{2}$ . Under translations, $J$ changes by $a \land P$ ; inserting this into $W$ adds an epsilon contraction with two copies of $P$ , which vanishes by antisymmetry. Lorentz covariance of $ε$ under $S O^{+}$ and the charge action [L1] preserve these scalar identities over the orbit.

1.2F1L1algebra

A stabilizer element must fix $P = (m c, 0)$ , so its Lorentz part is a spatial rotation. Preserving the nonzero spin vector leaves exactly the $S O (2)$ rotations about that axis, of dimension one. In the coadjoint action, preserving $J^{0 i} = 0$ then forces the spatial translation part to vanish, while translations parallel to $P$ remain free, giving one further dimension. The stabilizer has dimension two, and since $\dim G = 10$ by [F1], the orbit dimension is eight.

2.1F1L1step 1.1algebra

Any future timelike $P$ with $P^{2} = - m^{2} c^{2}$ can be sent to rest by a proper orthochronous Lorentz transformation. In that frame, choose the translation part $a$ to remove the three $J^{0 i}$ components; the remaining spatial spin vector has norm $s$ by step 1.1, and a spatial rotation sends it to the specified $J^{12} = s$ axis. Therefore every pair with the stated invariants lies in the rest representative's orbit; the converse follows from step 1.1.

3.1F1F2L1A1∎

Applying [F2] to this orbit gives its canonical smooth homogeneous-space structure and nondegenerate closed KKS two-form. If $s = 0$ , the stabilizer instead contains all three spatial rotations and the one translation parallel to $P$ , hence has dimension four and its orbit dimension is $10 - 4 = 6$ . This establishes the stabilizer jump without asserting regularity of any ambient Casimir locus.

PostulateStatement: AI-adaptedProof: Not applicable‡ sources checked 2026-10-15Open item page →

Optional adopted classical spinning-orbit model

Physical scope

Adopt specified KKS phase orbit, primitive m,s, chosen H=cP0; no quantum spectrum/unitary Wigner/spin-supplementary or force law inferred.

Postulate

Adopted model postulate (optional): Under ${A C}_{ω}$ for the referenced KKS orbit, and for fixed primitive parameters $m > 0$ (kg) and $s > 0$ (angular momentum units), use the coadjoint orbit and KKS symplectic form of Positive classical spin Poincare orbit and stabilizer jump as the phase space of a classical spinning particle. In a selected inertial frame choose the Hamiltonian $H = c P^{0}$ (joules). This premise chooses a mathematical model; it is not inferred from the spinless action, an experiment, or the existence of the orbit alone. It does not assert a quantum spin spectrum, a Wigner unitary representation, a spin supplementary condition, a charged-spin force law, or radiation dynamics.

Facts & Assumptions

Given: The optional adoption and primitive parameters stated above.

[A1]

Positive classical spin Poincare orbit and stabilizer jump: for $m, s > 0$ the specified rest charge point has an eight-dimensional KKS coadjoint orbit; this mathematical result does not select a physical particle model or Hamiltonian.

[A2]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only; no full axiom of choice is used.

Adopted premise

This item records [A1] as a model choice with the extra Hamiltonian $H = c P^{0}$ . No proof of nature's adoption of this model is claimed. The postulate carries no observational or statistical premise.

TheoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Massive spinless shell reduction is a single KKS orbit

Statement

Assume ${A C}_{ω}$ . Fix mass $m > 0$ in kg and $c > 0$ in m/s. For a charge point $(P^{a}, J^{a b})$ , lower indices by $P_{b} : = η_{b a} P^{a}$ and $J_{c d} : = η_{c e} η_{d f} J^{e f}$ , and define $P^{2} : = η_{a b} P^{a} P^{b}$ . Let $ε_{a b c d}$ be the totally antisymmetric Minkowski volume tensor with $ε_{0123} = + 1$ ; raising all indices with $η = diag (- 1, 1, 1, 1)$ gives $ε^{0123} = - 1$ . Let $Σ_{m}^{+}$ be the future mass shell in flat Minkowski cotangent space and quotient its complete characteristic lines as in the current draft H8 supplier. The resulting global phase space has coordinates $(a^{i}, p_{i}) \in R^{6}$ and form $d a^{i} \land d p_{i}$ . Under the charge map of Poincare cotangent moment map and full generator algebra, it is globally symplectomorphic to the single coadjoint orbit through $(P = (m c, 0), J = 0)$ . Its image is exactly the future massive charge pairs with $P^{2} = - m^{2} c^{2}$ and $W = 0$ , where $W^{a} = \frac{1}{2} ε^{a b c d} P_{b} J_{c d}$ . This statement identifies one smooth orbit; it makes no regularity claim about a union of Casimir level sets.

Facts & Assumptions

Given: $m > 0$ , signature $(-, +, +, +)$ , the totally antisymmetric volume tensor with $ε_{0123} = + 1$ and $ε^{0123} = - 1$ , and the exact global shell quotient.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only; no full axiom of choice is used.

[F1]

Poincare semidirect group, dual pairing and moment components: $P^{a} = η^{a b} p_{b}$ , $J^{a b} = x^{a} P^{b} - x^{b} P^{a}$ , and the affine cotangent charge pairing is fixed by $\exp (- s ξ)$ ; on charge space use $P_{b} = η_{b a} P^{a}$ and $J_{c d} = η_{c e} η_{d f} J^{e f}$ .

[L1]

Poincare cotangent moment map and full generator algebra: the current assigned A draft defines the same coadjoint charge map and action used here. The carrier exists as a batch-26 draft; its own H0/H8 prerequisites and proof status remain unresolved.

[L2]

Flat future mass shell has an explicit global orbit quotient: the current H8 draft gives the complete future-shell quotient by characteristic lines, global $(a, p)$ coordinates, reduced form $d a^{i} \land d p_{i}$ , and fixed-time slices; its dependencies match the H25 manifest. The H25 Step 1 record is ready/hash-current, but the carrier remains a draft without pipeline_run binding or independent proof approval.

[F2]

Coadjoint orbits are symplectic manifolds: a coadjoint orbit has canonical homogeneous-space smooth structure and KKS form $ω_{β} (ξ_{O}, η_{O}) = β ([ξ, η])$ , with moment equation $d μ^{ξ} = - ι_{ξ_{O}} ω$ .

Proof

technique · explicit global charge coordinates and KKS uniqueness

Given: The positive mass shell, actual H8 and H10 draft interfaces [L1]–[L2], and the inspected KKS theorem [F2].

1.1F1L1algebra

In a rest frame $P = (m c, 0)$ , $W = 0$ is equivalent to $J^{i j} = 0$ , since its three spatial components are an invertible multiple of the three spatial angular-momentum components. The remaining $J^{0 i}$ are produced explicitly by $x^{0} = 0$ , $x^{i} = - J^{0 i} / (m c)$ , since $J = x \land P$ then has exactly those components and $J^{i j} = 0$ . Lorentz transforming this representative gives a position representative for every future timelike $P$ with $W = 0$ . Equivalently for a transverse representative $x \cdot P = 0$ , $x^{a} = J^{a b} P_{b} / P^{2}$ , as substitution of $J = x \land P$ gives $J^{a b} P_{b} = x^{a} P^{2} - (x \cdot P) P^{a}$ . This characterization is Lorentz covariant.

2.1L1L2step 1.1algebra

H8's quotient point $(a, p)$ maps to $P^{0} = E / c$ , $P^{i} = p_{i}$ , $J^{0 i} = - a^{i} P^{0}$ , and $J^{i j} = a^{i} p_{j} - a^{j} p_{i}$ . The inverse is $p_{i} = P^{i}$ , $a^{i} = - J^{0 i} / P^{0}$ , smooth since $P^{0} > 0$ . These mutually inverse smooth coordinates make the image an embedded six-dimensional graph and show the quotient map is a diffeomorphism onto the charge locus of step 1.1.

3.1F1L1step 1.1step 2.1algebra

A proper orthochronous boost sends each future massive $P$ to rest. By step 1.1 its $W = 0$ charge then has only $J^{0 i}$ components, and a translation removes those components. Thus every pair in the locus is in the orbit of $(m c, 0; 0)$ ; conversely $P^{2}$ and $W = 0$ are invariant under the coadjoint action. The stabilizer at rest consists of spatial rotations and translations parallel to $P$ , dimension $3 + 1 = 4$ , so the orbit dimension is $10 - 4 = 6$ . The six smooth orbit coordinates $p_{i} = P^{i}$ , $a^{i} = - J^{0 i} / P^{0}$ from step 2.1 have injective differential: if their differentials vanish, the graph formulas in step 2.1 make every component of $(P, J)$ have zero differential, and the coadjoint-orbit inclusion is an immersion. Since both manifolds have dimension six, the inverse function theorem makes this coordinate map a local diffeomorphism. The bijection in step 2.1 is therefore a global diffeomorphism for the canonical orbit smooth structure.

4.1F2L1L2A1step 3.1∎

Let $ρ : Σ_{m}^{+} \to B_{m}$ be the H8 quotient and $ι : Σ_{m}^{+} ↪ T^{*} R^{4}$ the inclusion. H8 states $ρ^{*} ω_{r e d} = ι^{*} ω$ . The cotangent action of $g = (a, Λ)$ preserves this future shell: $P^{'} = Λ P$ preserves its norm and future cone, and it maps the full characteristic line $(x + α P, p)$ to $(Λ x + a + α Λ P, Λ^{- T} p)$ , which is exactly a characteristic line with momentum $P^{'}$ . The inverse group element gives the converse. Therefore the quotient action is well-defined. It is smooth because the global section $σ (a^{i}, p_{i})$ given by $x^{0} = 0$ , $x^{i} = a^{i}$ is smooth and $g \cdot b = ρ (g \cdot σ (b))$ is its explicit expression; fibre preservation gives the group law independently of the chosen section. The cotangent action is symplectic by [L1], so pulling back along the surjective submersion $ρ$ gives $ρ^{*} (g^{*} ω_{r e d}) = g^{*} ι^{*} ω = ι^{*} ω = ρ^{*} ω_{r e d}$ , hence the quotient action preserves $ω_{r e d}$ . Differentiating $ρ (\exp (- s ξ) \cdot z) = \exp (- s ξ) \cdot ρ (z)$ at $s = 0$ gives $d ρ (ξ_{Σ_{m}^{+}}) = ξ_{B_{m}}$ with the library's same fundamental-field convention. The moment components from [L1] are constant on each characteristic fibre since $P$ is fixed and $(x + α P) \land P = x \land P$ . Thus for any tangent $v$ on $B_{m}$ choose a lift $\tilde{v}$ and obtain $d {\overset{ˉ}{μ}}^{ξ} (v) = d μ^{ξ} (\tilde{v}) = - ω_{r e d} (ξ_{B_{m}}, v)$ . On the orbit [F2] gives the same moment equation. Its fundamental fields span each tangent space, so these equations determine both two-forms pointwise and show the diffeomorphism in step 3.1 pulls KKS back to $ω_{r e d} = d a^{i} \land d p_{i}$ .

Physics theoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Conditional classical orbit evolution and invariant labels

Physical scope

Selected linear H generates complete group translation on the orbit; m,s labels preserved.

Statement

Assume ${A C}_{ω}$ . Adopt the optional classical spinning-orbit model of Optional adopted classical spinning-orbit model with fixed $m, s > 0$ and selected inertial Hamiltonian $H = c P^{0}$ . Conditional on the KKS orbit and canonical Hamiltonian conventions, its Hamiltonian flow is the one-parameter coadjoint action of the corresponding time-translation subgroup (with the sign fixed by the library convention). It exists for all real evolution parameters and preserves $m$ and $s$ . This is a deduction inside the adopted classical model, not evidence for that model or a derivation of quantum spin.

Facts & Assumptions

Given: The optional model postulate, its fixed orbit, and $H = c P^{0}$ in one inertial frame.

[A1]

Optional adopted classical spinning-orbit model: the model adopts the positive-spin KKS orbit with primitive $m, s > 0$ and chooses $H = c P^{0}$ .

[L1]

Positive classical spin Poincare orbit and stabilizer jump: under ${A C}_{ω}$ , for $m, s, c > 0$ the coadjoint orbit through $P = (m c, 0, 0, 0)$ and $J^{12} = s$ is an eight-dimensional KKS symplectic manifold, with $P^{2} = - m^{2} c^{2}$ , $P$ future, $W \cdot P = 0$ and $W^{2} = m^{2} c^{2} s^{2}$ . Here $W^{a} = \frac{1}{2} ε^{a b c d} P_{b} J_{c d}$ with $ε_{0123} = + 1$ and indices raised by $η = diag (- 1, 1, 1, 1)$ , exactly as in that supplier. No temporal-chart or H10 hypothesis is required. It exists as a batch-26 draft, but is not independently approved.

[F1]

Coadjoint orbits are symplectic manifolds: on a coadjoint orbit the inclusion moment map satisfies $d μ^{ξ} = - ι_{ξ_{O}} ω_{K K S}$ , so linear dual components generate the corresponding infinitesimal coadjoint fields.

[L2]

Canonical Poisson brackets and local Hamiltonian flow fixes the cotangent convention $ι_{X_{H}} ω = d H$ . On the KKS symplectic orbit we define $X_{H}$ by the same intrinsic equation; existence, uniqueness and smoothness follow by inverting the smooth nonsingular matrix of $ω$ in local charts. The cotangent supplier's H25 Step 1 record is ready/hash-current; the carrier remains draft/unbound with ai-altered proof provenance, so that readiness does not independently approve its proof.

[F2]

Poincare semidirect group, dual pairing and moment components: the pure unit $x^{0}$ translation pairs with $p_{0} = - P^{0}$ under the fixed cotangent convention.

[A2]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only; no full axiom of choice is used.

Proof

technique · identify the linear Hamiltonian vector field with a group action

Given: [A1], the KKS moment equation [F1], and the Hamiltonian sign convention [L2].

1.1A1F1F2L1L2A2algebra

Let $ξ_{0}$ be unit translation in the $x^{0}$ direction. The dual pairing of [F2] gives $μ^{ξ_{0}} = p_{0} = - P^{0}$ , so $H = c P^{0} = - c μ^{ξ_{0}}$ . Since $ι_{ξ_{O}} ω = - d μ^{ξ_{0}}$ by [F1] and $ι_{X_{H}} ω = d H$ by [L2], $X_{H} = c ξ_{O}$ . With the library fundamental-field convention, its integral curve is $z (t) = \exp_{G} (- c t ξ_{0}) \cdot z (0)$ .

2.1F1L1A2step 1.1algebra∎

The fundamental field with the library convention integrates as $z (t) = \exp_{G} (- c t ξ_{0}) \cdot z (0)$ for every real $t$ ; differentiating this globally defined action gives $c ξ_{0, O}$ , the field from step 1.1. Thus this particular Hamiltonian flow is complete. The group action preserves the orbit invariants, so $P^{2} = - m^{2} c^{2}$ and $W^{2} = m^{2} c^{2} s^{2}$ remain fixed, preserving $m, s$ .

TheoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Killing scalar conservation in cotangent shell form

Statement

Assume ${A C}_{ω}$ for the cotangent supplier. Let $(M, g)$ be a smooth Lorentzian manifold with canonical cotangent coordinates $(x^{a}, p_{a})$ and $C_{m} (x, p) = \frac{1}{2} (g^{a b} p_{a} p_{b} + m^{2} c^{2})$ for fixed $m \geq 0$ . For any smooth vector field $ξ$ , set $F_{ξ} = p_{a} ξ^{a} (x)$ . With canonical bracket ${F, G} = F_{x} G_{p} - F_{p} G_{x}$ ,

${F_{ξ}, C_{m}} = - \frac{1}{2} (L_{ξ} g^{- 1})^{a b} p_{a} p_{b} .$

If $ξ$ is Killing, this bracket vanishes for all cotangent covectors, and $F_{ξ}$ is constant along every constrained free-shell trajectory generated by $e C_{m}$ with any smooth multiplier $e$ on its actual interval. No global existence or empirical conservation is asserted.

Facts & Assumptions

Given: A smooth nondegenerate Lorentzian metric, cotangent coordinates, constants $m \geq 0$ , $c > 0$ , and a smooth vector field $ξ : M \to T M$ with $ξ (x) \in T_{x} M$ . A trajectory generated by $e C_{m}$ means a smooth curve $z : I \to T^{*} M$ on an interval $I$ , with $C_{m} (z) = 0$ and $z^{'} (λ) = e (λ) X_{C_{m}} (z (λ))$ for a smooth parameter-only multiplier $e : I \to R$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only for the cotangent supplier; no full axiom of choice is used.

[L2]

Canonical Poisson brackets and local Hamiltonian flow: the current H0 draft fixes the canonical bracket $F_{x} G_{p} - F_{p} G_{x}$ and $d F / d t = F_{t} + {F, H}$ on actual solution intervals, with no completeness claim. Its H25 Step 1 record is ready/hash-current, but the carrier remains draft/unbound with ai-altered proof provenance and no independent proof approval.

[F1]

Here the Lie derivative of the metric is $L_{ξ} g = {\frac{d}{d s} ∣}_{s = 0} Φ_{s}^{*} g$ , where $Φ_{s}$ is the local flow of $ξ$ . In coordinates its components are $K_{a b} : = (L_{ξ} g)_{a b} = ξ^{c} \partial_{c} g_{a b} + g_{c b} \partial_{a} ξ^{c} + g_{a c} \partial_{b} ξ^{c}$ . A Killing field means $K_{a b} = 0$ in every chart. This definition requires neither orientation nor time orientation nor dimension four. The inverse metric has Lie derivative $(L_{ξ} g^{- 1})^{a b} = ξ^{c} \partial_{c} g^{a b} - g^{c b} \partial_{c} ξ^{a} - g^{a c} \partial_{c} ξ^{b}$ .

Proof

technique · direct tensor differentiation

Given: The smooth metric, canonical bracket [L2], shell function and generated trajectories specified above.

1.1givenL2F1algebra

In coordinates, $\partial_{x^{c}} F_{ξ} = p_{a} \partial_{c} ξ^{a}$ , $\partial_{p_{c}} F_{ξ} = ξ^{c}$ , $\partial_{p_{c}} C_{m} = g^{c b} p_{b}$ , and $\partial_{x^{c}} C_{m} = \frac{1}{2} \partial_{c} g^{a b} p_{a} p_{b}$ . Therefore [L2] gives ${F_{ξ}, C_{m}} = p_{a} (\partial_{c} ξ^{a}) g^{c b} p_{b} - \frac{1}{2} ξ^{c} (\partial_{c} g^{a b}) p_{a} p_{b} = - \frac{1}{2} (L_{ξ} g^{- 1})^{a b} p_{a} p_{b}$ , by [F1] and symmetry of $p_{a} p_{b}$ .

2.1F1step 1.1algebra

Differentiating $g^{a c} g_{c b} = δ_{b}^{a}$ gives $\partial_{e} g^{a b} = - g^{a c} g^{b d} \partial_{e} g_{c d}$ . Substitution in the coordinate formula of [F1] gives $(L_{ξ} g^{- 1})^{a b} = - g^{a c} g^{b d} K_{c d}$ . If $ξ$ is Killing, $K_{c d} = 0$ by definition, so $L_{ξ} g^{- 1} = 0$ . Step 1.1 then gives ${F_{ξ}, C_{m}} = 0$ at every cotangent covector.

3.1givenL2A1step 2.1∎

Along any generated trajectory in the stated sense, the chain rule and [L2] give $\frac{d}{d λ} F_{ξ} = d F_{ξ} (e X_{C_{m}}) = e {F_{ξ}, C_{m}}$ because $F_{ξ}$ has no explicit parameter dependence. This vanishes by step 2.1 throughout the solution's actual interval, and hence $F_{ξ}$ is constant there. The calculation is local in charts and thus applies along the whole interval, with no completeness assumption.

Physics theoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Conditional free Poincare and background Killing charges

Physical scope

Under the exact action and background symmetry, adopted mechanical charge observables are conserved; time-dependent boosts include partial-time cancellation.

Statement

Assume ${A C}_{ω}$ for the moment-map supplier. Adopt either the massive free test-particle action or the distinct massless shell action of Free massive test-particle action and Separate massless shell action. Conditional on those model choices and the corresponding future free-shell equations, the affine Poincaré charges are conserved on flat spacetime; in a fixed-time Hamiltonian description the boost charge includes its explicit partial-time derivative. On a prescribed curved background, every mechanical scalar $p_{a} ξ^{a}$ for a Killing field is conserved along the adopted free shell. These are model deductions. They do not establish the empirical adequacy of either action, and they do not extend to arbitrary interacting potentials.

Facts & Assumptions

Given: A flat inertial Minkowski background or a prescribed smooth Lorentzian background with a Killing field, and one of the explicitly adopted free-particle models.

[A1]

Free massive test-particle action: the massive model adopts fixed primitive mass $m > 0$ and the stationary action $- m c \int \sqrt{- g (x^{'}, x^{'})} d λ$ on future timelike curves with the stated endpoint and regularity conditions. The H5 carrier remains a draft adopted postulate with no pipeline_run binding; its current Step 1 record is ready/hash-current, which is input readiness and not empirical evidence or independent proof approval.

[A2]

Separate massless shell action: the massless model is a separate constrained first-order action with nonzero future null momentum and positive multiplier; it is not obtained by putting $m = 0$ in the massive square-root action. This H5 carrier remains a draft adopted postulate with no pipeline_run binding; its current Step 1 record is ready/hash-current, not an empirical finding or independent proof approval.

[L1]

Poincare cotangent moment map and full generator algebra: the current assigned A draft states shell charge descent and the time-dependent boost identity partial_t B_i+{B_i,E}=0. It is a batch-26 draft with H0/H8 inputs still open.

[L2]

Killing scalar conservation in cotangent shell form: for a Killing vector, ${p_{a} ξ^{a}, C_{m}} = 0$ identically, so the scalar is conserved along the constrained free-shell flow; the proof is conditional on H0/H7.

[A3]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only; no full axiom of choice is used.

[L3]

First-order shell action yields massive and null geodesics: the current H7 draft assumes a prescribed smooth time-oriented Lorentzian background, a compact chart interval, smooth $x, p, e$ , $e > 0$ , and either the future timelike $m > 0$ branch or the separate nonzero future-null $m = 0$ branch; its stationary equations are $x'^{a} = e g^{a b} p_{b}$ , $p'_{a} = - \frac{e}{2} \partial_{a} g^{b c} p_{b} p_{c}$ , $C_{m} = 0$ . It relates the massive square-root functional to the shell equations; the null branch remains separately specified. This is a mathematical variational supplier for explicit functionals and selected future branches; adoption of particle dynamics is a separate physical premise.

Proof

technique · apply the shell first-integral identities to the adopted models

Given: [A1] or [A2] and the actual corresponding constrained shell trajectories.

1.1A1A2A3L1L3algebra

Under [A1] or [A2], the model is restricted to its stated massive future-timelike or nonzero future-null branch. On flat spacetime the affine generators are Killing fields; their phase-space charges are the components of [L1]. The shell brackets vanish, so each time-independent translation or Lorentz component is constant along its shell characteristic. For a fixed-time boost, the derivative is instead $\partial_{t} B_{i} + {B_{i}, E}$ , which vanishes by [L1].

2.1A1A2A3L2L3algebra∎

On a prescribed curved background, let $ξ$ be Killing. By [L2] the bracket with the mass-shell constraint vanishes; along the multiplier equations selected by either adopted action the derivative is $e {p_{a} ξ^{a}, C_{m}} = 0$ . This is a conditional model prediction for the specified background symmetry.

TheoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Complete integrals and covariant versus time Hamilton-Jacobi

Statement

Assume ${A C}_{ω}$ for the cotangent/HJ supplier chain and let $n \geq 1$ . Let $U_{H} \subset R \times T^{*} R^{n}$ be open and $H \in C^{\infty} (U_{H}, R)$ . Let $D_{S} \subset R \times R_{q}^{n} \times R_{α}^{n}$ be open and $S \in C^{3} (D_{S}, R)$ , with $S_{t} + H (t, q, S_{q}) = 0$ wherever $(t, q, α) \in D_{S}$ and $(t, q, S_{q} (t, q, α)) \in U_{H}$ . If the mixed matrix $S_{q α}$ is invertible at $(t, q, α)$ , then after restricting neighborhoods the equations $p_{i} = S_{q^{i}}$ , $β^{i} = S_{α_{i}}$ define a local $C^{2}$ diffeomorphism $F_{t} : (q, p) \mapsto (β, α)$ at each fixed $t$ . Equip the old chart $(q, p)$ with $ω_{o l d} = \sum_{i} d q^{i} \land d p_{i}$ and the target chart, whose position coordinates are $β^{i}$ and momentum coordinates are $α_{i}$ , with $ω_{n e w} = \sum_{i} d β^{i} \land d α_{i}$ . Then $F_{t}^{*} ω_{n e w} = ω_{o l d}$ , so this is a local canonical transformation in the stated convention, and $β$ is constant along the Hamilton characteristics $\dot{q} = H_{p}$ , $\dot{p} = - H_{q}$ . Such a family is a complete integral only on that nonsingular local domain. In the physical interpretation, $q^{i}, β^{i}$ have units m, $p_{i}, α_{i}$ have units kg m/s, $t$ has units s, and $S$ has units J s. $S$ is assigned action units in this interpretation.

For the relativistic specialization, take $n = 3$ , $m \geq 0$ in kilograms and $c > 0$ in metres per second, and a temporal product chart $(x^{0}, q) \in I_{0} \times Ω$ with the selected future normal of A curved temporal chart gives a local reduced Hamiltonian. Write its metric as $g = - N^{2} (d x^{0})^{2} + h_{i j} (d q^{i} + b^{i} d x^{0}) (d q^{j} + b^{j} d x^{0})$ , where $N > 0$ , $b^{i}$ and the positive-definite symmetric matrix $h_{i j}$ are smooth; $h^{i j}$ is the inverse matrix. The notation $b^{i}$ denotes the shift, distinct from the integration coordinate $β^{i}$ . Set $x^{0} = c t$ and require the Hamiltonian in this specialization to be exactly

$H (t, q, p) = c (N (c t, q) \sqrt{m^{2} c^{2} + h^{i j} (c t, q) p_{i} p_{j}} - b^{i} (c t, q) p_{i}),$

on $U_{H} = {t : c t \in I_{0}} \times T^{*} Ω$ for $m > 0$ , or its open part $p \neq 0$ for $m = 0$ . For each fixed $α$ , define the spacetime action $S (x^{0}, q, α) : = S (x^{0} / c, q, α)$ on the corresponding chart domain and write $S_{a} : = \partial_{x^{a}} S$ . Then the covariant equation $g^{a b} S_{a} S_{b} + m^{2} c^{2} = 0$ with $(d S)^{♯}$ future, excluding the zero covector when $m = 0$ , is equivalent to $S_{t} + H (t, q, S_{q}) = 0$ , with $p_{0} = S_{t} / c = - H / c$ . The canonical-coordinate result above still applies to arbitrary $H$ ; the covariant-shell equivalence uses this specified reduced Hamiltonian.

Facts & Assumptions

Given: $n \geq 1$ , the open domains and smooth Hamiltonian in the statement, a local $C^{3}$ HJ solution, and a point where $S_{q α}$ is invertible.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only for the cotangent and HJ supplier chain; no full axiom of choice is used.

[L1]

Local Hamilton-Jacobi solution by invertible characteristics: for each initial point $(0, a_{0}, d S_{0} (a_{0}))$ lying in its open Hamiltonian domain, the local characteristic construction supplies an actual smooth HJ solution while its projection remains invertible; no continuation beyond loss of projection invertibility is asserted.

[F1]

The Euclidean inverse function theorem: a $C^{1}$ map with invertible derivative has a local $C^{1}$ inverse $g$ , with $D g (y) = D f (g (y))^{- 1}$ . The scalar derivative algebra and total chain rule are supplied by 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$ and The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ .

[L2]

A curved temporal chart gives a local reduced Hamiltonian: the current H9 draft assumes a temporal product chart, $N > 0$ , positive spatial metric, and excludes $p_{i} = 0$ on the massless branch; it gives $p_{0} = β^{i} p_{i} - N \sqrt{m^{2} c^{2} + h^{i j} p_{i} p_{j}}$ and $H = - c p_{0}$ . The supplier is a mathematical deduction within its stated chart, positive-root and nonzero-null hypotheses; it introduces no physical action adoption. Here the temporal coefficients in the reduced root are evaluated at $(c t, q)$ ; the physical-time domain is ${t : c t \in I}$ .

Proof

technique · implicit-function and generating-function identities

Given: The hypotheses in the statement and exact conditional temporal-shell interface [L2].

1.1F1givenalgebra

First obtain the exact finite-regularity inverse used here from [F1]. If $f$ is $C^{2}$ , its local $C^{1}$ inverse $g$ satisfies $D g = (D f \circ g)^{- 1}$ . The entries of $D f \circ g$ are $C^{1}$ by the chain rule. Matrix inversion on invertible matrices is $C^{1}$ entrywise by the cofactor-over-determinant formula, whose denominator is nonzero; finite products and reciprocal differentiation use the derivative algebra in [F1]. Consequently $D g$ is $C^{1}$ , and $g$ is $C^{2}$ . At fixed $t$ , the map $(q, α) \mapsto (q, p = S_{q})$ has derivative $(\begin{array}{cc} I & 0 \\ S_{q q} & S_{q α} \end{array})$ , which is invertible at the stated point. By [F1], after restriction it is a diffeomorphism and solves locally for $α = α (t, q, p)$ . Keeping $t$ as an additional identity coordinate in $(t, q, α) \mapsto (t, q, S_{q})$ gives the same invertible block derivative and shows that the inverse $α (t, q, p)$ is jointly $C^{2}$ . Define $β = S_{α} (t, q, α (t, q, p))$ ; this gives a $C^{2}$ local map $(q, p) \mapsto (β, α)$ .

1.2L2A1givenalgebra

In the relativistic specialization, the chain rule gives $p_{0} = \partial_{x^{0}} S = S_{t} / c$ and $p_{i} = \partial_{q^{i}} S = S_{q^{i}}$ . The future-shell root [L2] is $p_{0} = b^{i} (c t, q) p_{i} - N (c t, q) \sqrt{m^{2} c^{2} + h^{i j} (c t, q) p_{i} p_{j}} = - H (t, q, p) / c$ for the Hamiltonian explicitly required in the statement. Thus the covariant future-shell equation implies $S_{t} + H (t, q, S_{q}) = 0$ . Conversely, this HJ equation sets $p_{0}$ to precisely that root, which solves the covariant shell equation and selects its future branch; the root satisfies $p (n) = - \sqrt{m^{2} c^{2} + h^{i j} p_{i} p_{j}} < 0$ for the selected future unit normal $n$ . The nonzero-momentum domain when $m = 0$ excludes the zero null covector.

2.1F1step 1.1algebra

The map $(q, α) \mapsto (β = S_{α}, α)$ has derivative $(\begin{array}{cc} S_{α q} & S_{α α} \\ 0 & I \end{array})$ , which is invertible because $S_{α q} = (S_{q α})^{T}$ . By [F1] it has a $C^{2}$ local inverse solving for $q$ from $(β, α)$ ; then $p = S_{q}$ gives the $C^{2}$ inverse map to the one in step 1.1. The equations therefore define the claimed local diffeomorphism.

2.2L1A1step 1.1algebra

Along a Hamilton characteristic, $\dot{q} = H_{p}$ and $\dot{p} = - H_{q}$ . Differentiate $p = S_{q} (t, q, α (t, q, p))$ along it, and differentiate the HJ equation in $q$ to obtain $\dot{p} = - H_{q} + S_{q α} \dot{α}$ . Since $S_{q α}$ is invertible, $\dot{α} = 0$ . Differentiate the HJ equation with respect to $α$ : $S_{α t} + S_{α q} H_{p} = 0$ . Thus $\dot{β} = \frac{d}{d t} S_{α} = S_{α t} + S_{α q} \dot{q} = 0$ .

3.1givenstep 1.1step 2.1algebra

At fixed $t$ , the differential in $(q, α)$ is $d_{(q, α)} S = p_{i} d q^{i} + β^{i} d α_{i}$ . Taking its exterior derivative gives $0 = d p_{i} \land d q^{i} + d β^{i} \land d α_{i}$ , hence $\sum_{i} d q^{i} \land d p_{i} = \sum_{i} d β^{i} \land d α_{i}$ . This is exactly $F_{t}^{*} ω_{n e w} = ω_{o l d}$ for the source and target forms stated above.

4.1givenalgebra∎

Under the stated SI assignments, $S$ has joule-seconds, so $p = S_{q}$ has kg m/s and $S_{t}$ has joules. Since $α$ is assigned kg m/s, $β = S_{α}$ has metres. Thus the HJ equation and the canonical generating identity respect the assigned action units.

Physics theoremStatement: AI-adaptedProof: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Conditional particle trajectories from Hamilton-Jacobi characteristics

Physical scope

Adopted free test-particle/massless model on the actual time-pulled-back chart domain and invertible characteristic projection; no global graph continuation is asserted.

Statement

Assume ${A C}_{ω}$ for the cotangent/H7/H9 supplier chain. Adopt the massive free action or separate massless shell action in Free massive test-particle action and Separate massless shell action. Let $I_{0} \subseteq R$ be the open first-coordinate interval, measured in metres, of a temporal product chart, and let $Ω \subseteq R^{3}$ be its open spatial coordinate range. Let $(N, β, h)$ be the smooth temporal-chart data on $I_{0} \times Ω$ of Temporal chart with lapse, shift and positive slice metric, with $N > 0$ and $h_{i j}$ positive definite. Take $m \geq 0$ in kg and $c > 0$ in m/s, and define the physical-time domain $I_{t} : = {t \in R : c t \in I_{0}}$ and pulled-back data $\hat{N} (t, q) : = N (c t, q)$ , ${\hat{β}}^{i} (t, q) : = β^{i} (c t, q)$ , ${\hat{h}}_{i j} (t, q) : = h_{i j} (c t, q)$ . Write ${\hat{h}}^{i j}$ for the inverse matrix. On the future shell with $x^{0} = c t$ , define $κ (t, q, p) = \sqrt{m^{2} c^{2} + {\hat{h}}^{i j} (t, q) p_{i} p_{j}}$ , $p_{0} = {\hat{β}}^{i} p_{i} - \hat{N} κ$ , and the positive-root reduced Hamiltonian $H (t, q, p) = - c p_{0} = c (\hat{N} κ - {\hat{β}}^{i} p_{i})$ from A curved temporal chart gives a local reduced Hamiltonian. Its open domain is $U = I_{t} \times T^{*} Ω$ for $m > 0$ , and $U = I_{t} \times (T^{*} Ω ∖ {p = 0})$ for $m = 0$ . Here $t$ is measured in seconds, $q$ in metres, $p$ in kg m/s, $H$ in joules, and $S$ in joule-seconds. Let $D \subseteq I_{t} \times Ω$ be open and let $S \in C^{2} (D, R)$ (all partial derivatives through order two are continuous) satisfy $S_{t} + H (t, q, S_{q}) = 0$ wherever $(t, q, S_{q}) \in U$ . If $S$ is the smooth local solution supplied by Local Hamilton-Jacobi solution by invertible characteristics from an initial exact-graph point in $U$ , and $J = [t_{1}, t_{2}] \subset I_{t}$ with $t_{1} < t_{2}$ is an interval on which its characteristic projection remains invertible, let $q : J \to Ω$ be a $C^{1}$ characteristic with $\dot{q} = H_{p} (t, q, S_{q})$ . Then $p (t) : = S_{q} (t, q (t))$ satisfies $\dot{p} = - H_{q}$ , so $(q, p)$ obey Hamilton's equations. The smooth ODE makes this characteristic smooth; by A curved temporal chart gives a local reduced Hamiltonian these reduced equations are exactly the equations of the future-shell first-order system of First-order shell action yields massive and null geodesics. Under the matching adopted model postulate, this curve is a trajectory of the massive or separate massless model. The conclusion holds only on the chart and the actual invertible projection interval; no global Hamilton--Jacobi graph continuation is asserted. It is a conditional mathematical prediction, not a reported observation.

The characteristic graph is restricted to points with $(t, q, S_{q} (t, q)) \in U$ . The action $S$ is measured in joule-seconds.

Facts & Assumptions

Given: One of the stated free-particle model postulates, the temporal chart and future-shell domain, a smooth HJ solution, and a characteristic curve on a compact interval of its invertible projection.

[A3]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): assume countable choice ${A C}_{ω}$ only for the cotangent/H7 supplier chain; no full axiom of choice is used.

[A1]

Free massive test-particle action: the massive action is adopted only for future timelike curves and fixed $m > 0$ with the stated regularity and endpoint conditions. This H5 carrier remains a draft model postulate with no pipeline_run binding; its current Step 1 record is ready/hash-current, which does not make it an empirical report or independent proof approval.

[A2]

Separate massless shell action: the massless model separately adopts nonzero future null momentum and a positive multiplier; it has no massive proper-time parameterization. This H5 carrier remains a draft model postulate with no pipeline_run binding; its current Step 1 record is ready/hash-current and is not an empirical report or independent proof approval.

[L1]

First-order shell action yields massive and null geodesics: the current H7 draft assumes a prescribed smooth time-oriented Lorentzian four-manifold, a compact chart interval, smooth $x, p, e$ , $e > 0$ , $m \geq 0$ , and the future massive or separate nonzero future-null branch. It supplies $C_{m} = 0$ , $x'^{a} = e g^{a b} p_{b}$ , $p'_{a} = - \frac{e}{2} \partial_{a} g^{b c} p_{b} p_{c}$ , and the unparameterized geodesic interpretation. This is a mathematical variational supplier for explicit functionals and selected future branches; adoption of particle dynamics is a separate physical premise.

[L2]

Local Hamilton-Jacobi solution by invertible characteristics: when the initial exact-graph point lies in its open Hamiltonian domain, it supplies a smooth local HJ solution while the characteristic projection remains invertible. Its proof uses the current draft canonical-flow supplier's stated local Hamiltonian equations; that supplier's Step 1 readiness is not independent proof approval.

[L3]

Complete integrals and covariant versus time Hamilton-Jacobi: for a nonsingular mixed Hessian, the HJ parameters and their conjugates give local canonical integration coordinates; the item states the exact chart and projection-invertibility limitation.

[L4]

A curved temporal chart gives a local reduced Hamiltonian: at the point $x^{0} = c t$ in the chart, under $N > 0$ , positive-definite $h$ , and nonzero spatial momentum on the massless branch, the positive future-shell root gives $p_{0} = β^{i} (c t, q) p_{i} - N (c t, q) κ$ , $H = - c p_{0}$ , and $C_{p_{0}} = κ / N > 0$ for $C = \frac{1}{2} (g^{a b} p_{a} p_{b} + m^{2} c^{2})$ . Its gauge-reduced action has Hamilton equations on the chart interval. This current H9 supplier is a draft; the use here is conditional on that exact statement.

Proof

technique · differentiate the HJ equation along characteristics

Given: The model premises [A1] or [A2], an HJ solution on its invertible domain, and the exact conditional H7 interface [L1].

1.1givenA3algebra

Put $p (t) = S_{q} (t, q (t))$ . From $S_{t} + H (t, q, S_{q}) = 0$ , differentiation with respect to $q$ gives $S_{q t} + H_{q} + H_{p} S_{q q} = 0$ . Since $\dot{q} = H_{p}$ , the chain rule yields $\dot{p} = S_{q t} + S_{q q} \dot{q} = - H_{q}$ . Thus $(q, p)$ satisfies both Hamilton equations.

2.1A3L1L4step 1.1algebra

Write $C_{m} (x^{0}, q, p_{0}, p_{i}) = \frac{1}{2} (g^{a b} p_{a} p_{b} + m^{2} c^{2})$ and lift the characteristic by $x^{0} = c t$ , $x^{i} = q^{i}$ , with $p_{0} (t, q, p) = {\hat{β}}^{i} (t, q) p_{i} - \hat{N} (t, q) κ (t, q, p)$ from [L4]. All derivatives of $C_{m}$ below are evaluated at this lifted point. Set $e : = c / C_{p_{0}} = c \hat{N} / κ > 0$ . Implicit differentiation of $C_{m} (c t, q, p_{0} (t, q, p), p) = 0$ gives $H_{p_{i}} = c C_{p_{i}} / C_{p_{0}} = e C_{p_{i}}$ and $- H_{q^{i}} = - c C_{q^{i}} / C_{p_{0}} = - e C_{q^{i}}$ . Thus ${\dot{x}}^{0} = c = e C_{p_{0}}$ , ${\dot{x}}^{i} = e C_{p_{i}}$ , and ${\dot{p}}_{i} = - e C_{q^{i}}$ . Differentiating $C_{m} = 0$ along the lifted curve makes the $q^{i}, p_{i}$ terms cancel and gives $C_{p_{0}} {\dot{p}}_{0} = - c C_{x^{0}}$ , hence ${\dot{p}}_{0} = - e C_{x^{0}}$ . The lift therefore satisfies the complete H7 first-order shell system. The smooth HJ characteristic and $e$ meet H7's regularity conditions on the compact chart interval.

3.1A1A2A3L1L4step 2.1

By [A1] or [A2], the massive or separate massless action is adopted on exactly its stated future branch; H7's variational equivalence then identifies the shell trajectory of step 2.1 with a trajectory of that adopted model. This conclusion remains conditional on those physical postulates.

4.1L2L3A3step 1.1∎

The inverse projection and complete-integral coordinates from [L2]–[L3] apply only where their Jacobians remain nonsingular. If that projection loses invertibility, the single-valued graph $p = S_{q}$ used in step 1.1 is no longer supplied; therefore no continuation beyond the actual invertible projection interval or chart domain follows.

5 · Examples, experiments and counterexamples

None yet.