The motivating idea: Solve the coupled, highly nonlinear dynamics of a manuevering hypersonic body weakly, and extract a finite-dimensional skeleton in the form of a trajectory outer-bound via Galerkin projection.
This then evolved into a tentative thesis proposal on certified reachable sets for hypersonic entry vehicles, and the Python package that implements, demonstrates and stress-tests the model.
flowchart TD
subgraph phase1_embedding ["<b>Phase 1: Embedding</b>"]
direction LR
rigid_body_6-dof["<b>Rigid Body 6-DOF:</b>
• Position, Velocity
• Quaternions, Body Rates"]
style rigid_body_6-dof text-align:left
thermal_ablation["<b>Thermal & Ablation:</b>
• Position, Velocity
• Quaternions, Body Rates"]
style thermal_ablation text-align:left
corridor_constraints_envelopes["<b>Corridor Constraints & Envelopes:</b>
• Constraints: Heating, q_bar, Load Factor, Heat Load
• Envelopes: Real-gas, Rarefaction, 2nd/3rd-Order Piston"]
style corridor_constraints_envelopes text-align:left
structural_elasticity["<b>Structural Elasticity:</b>
• Banded Stiffness w = E(T)
• Modal Amplitudes (eta)
• 1st-Order Piston Theory"]
style structural_elasticity text-align:left
rigid_body_6-dof-- "Sutton-Graves heating" -->thermal_ablation
thermal_ablation-- "T-dependant softening" -->structural_elasticity
structural_elasticity-- "Deformation changes incidence & moments" -->rigid_body_6-dof
thermal_ablation & structural_elasticity-->corridor_constraints_envelopes
end
subgraph phase2_relaxation ["<b>Phase 2: Relaxation</b>"]
direction LR
weak_liouville_identity["<b>Weak Liouville Identity</b>"]
occupation_measures["<b>Occupation Measures:</b> Tracks trajectory family in W^{1, \infty}"]
guard_measures[<b>Guard Measures:</b> Linear equality constraints across phase boundaries]
weak_liouville_identity-->occupation_measures & guard_measures
end
subgraph phase3_decomposition ["<b>Phase 3: Decomposition</b>"]
direction LR
skeleton["<b>Skeleton (Intersection of 3 Slow Manifolds):</b>
• Quasi-Equilibrium Glide
• Aerodynamic Trim
• Quasi-Static Deflection"]
style skeleton text-align:left
bubbles["<b>Bubbles (Rescaled transients at multiple scales):</b>
• Atmospheric skips
• Mode switches
• Guard crossings"]
style bubbles text-align:left
residual["<b>Residual (Explicit bound on):</b>
• High-mode tail energy
• Non-orthogonal scale collisions"]
style residual text-align:left
end
subgraph phase4_certification ["<b>Phase 4: Certification</b>"]
direction LR
dual_polynomial_construction["<b>Dual Polynomial Construction:</b> Skeleton Distance + Bubble Inner Profiles + Residual Margin"]
exact_rational_verification["<b>Exact Rational Verification:</b> Machine-checked inequality in exact arithmetic against worst-case envelopes"]
dual_polynomial_construction-- "Positivstellensatz Multipliers over Corridor" -->exact_rational_verification
end
phase1_embedding-- "Polynomial Lift via Savageau-Voit Recast" -->phase2_relaxation
phase2_relaxation-- "Singular Limit: eps_atm, eps_att, eps_ela -> 0" -->phase3_decomposition
phase3_decomposition-- "Supplies exact shape for dual comparison function" -->phase4_certification
phase4_certification-->A@{ shape: lean-r, label: "Certified Footprint & Certified Flutter Margin" }
The reachable set of a hypersonic entry vehicle — every state it can be driven to under admissible control — is what safety-critical and threat analysis actually need bounded. Computing it exactly means solving a Hamilton–Jacobi–Isaacs equation on a grid: exponential in state dimension, capped in practice around four or five states. A rigid-body entry vehicle has thirteen before any augmentation, and twenty-five once ablation, heat load and structural deformation are carried.
Worse, a grid gives a numerical approximation, not a certificate. And a polynomial barrier whose coefficients came out of an interior-point solver has analytical form but inherits the solver's accuracy. There are two things to beat here, not one.
Embed the hybrid vehicle dynamics into a Banach space of occupation measures, where the problem becomes linear despite the nonlinearity of the flight mechanics. In the thin-atmosphere limit the resulting measure family is not compact: mass concentrates onto a low-dimensional set of trajectories. Turn that failure of compactness into a profile decomposition — a finite-dimensional skeleton, one boundary-layer profile per event, and a residual with a quantitative bound — and use its structure to derive a comparison certificate rather than search for one numerically.
The bound is then analytical in the strong sense: derived by hand, discharged in exact rational arithmetic over the entry corridor. Sum-of-squares programming appears only as an independent numerical cross-check, never as the source of the guarantee.
flowchart LR
P1["<b>Paper 1</b><br/>measure embedding<br/>profile decomposition<br/>derived certificate"]
P2["<b>Paper 2</b><br/>set-membership<br/>telemetry contraction"]
P3["<b>Paper 3</b><br/>diffusion vs. concentration<br/>supermartingale bounds"]
P1 -- "ℛ_cert" --> P2
P2 -- "ℛ_post" --> P3
P3 -- "ℛ_safe" --> OUT["probability of<br/>corridor exit"]
The output of each paper is the object the next one operates on, and the containment
ℛ_safe ⊆ ℛ_post ⊆ ℛ_cert
is a monotone set-containment argument rather than an analogy: all three are supports of occupation measures related by set-valued operations on the same Liouville-governed measure. Paper 2 re-weights it by a likelihood; Paper 3 replaces Liouville by Kolmogorov-forward and diffuses it.
| # | Title | What it adds |
|---|---|---|
| 1 | Certified Analytical Bounds for Multi-Phase Hypersonic Reachable Sets | the embedding, the decomposition, the certificate |
| 2 | Sequential Telemetry and the Contraction of Certified Reachable Sets | successive measurements tighten the bound |
| 3 | Supermartingale Bounds for Multi-Phase Hypersonic Reachable Sets under Stochastic Forcing | unbounded noise; the guarantee changes kind |
Paper 3's guarantee is weaker in kind, not merely in constant: under unbounded noise no compact set contains the state almost surely, so deterministic containment becomes a probability of exit. That distinction is stated in its abstract rather than buried.
Six degrees of freedom, plus what deforms. Attitude and body rates are states; angle of attack and sideslip are outputs of the attitude solution, not commanded quantities. Controls are flap deflections, RCS moments and throttle. Trim is never assumed solvable, so attitudes the vehicle cannot hold are excluded automatically rather than by fiat.
Multi-phase. Vacuum and atmospheric flight, with and without thrust, are modes of a hybrid system. Equilibrium glide, skip-glide, boost-glide and fractional-orbit profiles are admissible words over that alphabet rather than separate models — so results hold for every family in the class without enumerating them.
The corridor is load-bearing mathematically, not just physically. Heating rate, dynamic pressure, load factor and integrated heat load are what make the state set compact, and compactness is a hypothesis of every result in the series. The hypersonic physics does mathematical work.
Every effect the model carries enters the certificate in one of exactly two ways. Effects that cannot be resolved at this fidelity are enclosed: shown to lie in a computable envelope over the corridor, so the differential inclusion they generate bounds every selection, hence the truth. Effects that can be resolved are carried as states with their own rate laws.
| Effect | Treatment |
|---|---|
| Real-gas and Mach-dependent aerodynamics | enclosed — envelope on the coefficient maps |
| Rarefaction / Knudsen bridging | enclosed — constitutive regime boundary |
| Wind | enclosed — certified bound from reanalysis climatology |
| Frame coupling of aero force into inertial energy | enclosed — sharp constant from the load-factor constraint |
| Higher-order piston-theory forcing | enclosed — keeps the load-bearing pencil linear |
| Ablation recession | resolved — state, bounded by the heat-load budget |
| Integrated heat load | resolved — state with a polynomial rate equation |
| Aerothermoelastic deformation | resolved — modal state, temperature-dependent banded stiffness, first-order piston forcing |
Aerothermoelasticity was the last effect whose bound was assumed rather than certified. Resolving it means the program is no longer "occupation measures, plus a special argument for skips, plus a separate story for elasticity" — it is one method with one standing hypothesis, a uniform spectral gap, whose certification is itself the point. The flutter margin is not a separate theorem; it is the certificate that the modal bound is forward-invariant under the true dynamics rather than posited.
Everything above is made polynomial exactly, by adjoining auxiliary states rather than by
fitting: density as y = √(ρ/ρ₀) with ẏ ∝ y, and the temperature-dependent elastic
modulus by the same exponential lift, ẇ ∝ w·Ṫ. No fit residual is smuggled in as a
disturbance. That closure is the keystone every downstream result routes through.
It owns propagation fidelity: given the input models and their uncertainty, that uncertainty is carried into reachable-set uncertainty soundly and without leakage. It does not own flow-physics fidelity — the coefficient envelopes, the temperature field, the softening law, transition and shock/boundary-layer interaction are empirical inputs with their own error bars, and no amount of analysis manufactures fidelity that is not in them.
The honest headline is therefore: the tightest certified reachable set consistent with the fidelity of the aerothermodynamic inputs, with that fidelity faithfully propagated and never silently exceeded.
Early, and deliberately explicit about it.
Paper 1's model chapter and Appendices A–E are drafted. Sections 3 through 7 are section structure. The only theorem environments that exist anywhere are the sub-escape assumption and the forward-invariance lemma — the three headline contributions are unwritten, and nothing in the manuscripts should yet be read as a claim.
The shared bibliography, manuscripts/shared.bib, is assembled by
hand: entries are added as sources are read and their details checked against the published
record, rather than generated and hoped over.
cd manuscripts
./build.sh # all three papers
./build.sh paper1 # one paper
./build.sh watch paper1 # continuous rebuild
./build.sh clean # remove build artifactsmake does the same where it is installed; build.sh is the portable entry point.
An applied implementation of the model the papers reason about — used to demonstrate that the physics closes, to generate the numbers the manuscripts are permitted to quote, and as a sandbox for testing whether a modeling decision survives being computed.
It is not the contribution, and no result in the papers depends on a float it produces. The one exception runs the other way: the certificate's exact-arithmetic verification is a script that checks the derived bound and exits nonzero on failure, and that script is the artifact carrying the guarantee.
| Module | Contents |
|---|---|
spectral/ |
Chebyshev–Gauss–Lobatto operators by direct recurrence with the negative-sum trick; Clenshaw–Curtis quadrature; barycentric interpolation |
ultraspherical/ |
Olver–Townsend banded operators and assembly — the bandedness the sparsity argument rests on |
structures/ |
Variable-rigidity Euler–Bernoulli operator with the full product-rule expansion; free-free BCs by null-space projection; modal reduction; integrators |
plates/ |
Mindlin plates, laminate stiffness |
coupling/ |
Quadrature-normalized kernel force transfer |
thermal/ |
Landau immobilization frame; semi-discrete charring/Stefan solver on the fixed grid |
fiat/ |
Fully implicit ablation and thermal response of a multilayer TPS stack; independent implementation of the Chen–Milos formulation |
aerothermal/ |
Fay–Riddell stagnation heating with the Lewis exponent stated; modified-Newtonian velocity gradient |
aerodynamics/ |
Five methods, each valid somewhere and none everywhere — modified-Newtonian and Prandtl–Meyer impact, panels, free-molecular closure |
geometry/ |
Outer mould line from a mesh; measured shape scalars rather than stipulated ones. prep conditions an authored STL into a master — consistent winding, degenerate facets dropped, units and orientation normalised — and writes a manifest recording every repair and factor applied |
atmosphere/ |
US Standard 1976, MSIS thermosphere, ERA5 reanalysis winds |
dynamics/ |
Quaternion attitude kinematics with norm-error diagnostics; incidence on a deformed surface |
flight/ |
The coupled simulator: thirteen rigid-body states augmented by mass, recession and retained structural modes, as one system of ODEs |
orbital/ |
Two-body astrodynamics over an arbitrary central body; Lambert targeting; atmospheric coast |
guidance/ |
Proportional navigation and its augmented form; strapdown inertial propagation; stable time-to-go |
optimal_control/ |
Legendre–Gauss–Lobatto direct transcription and Pontryagin refinement over an arbitrary problem |
estimation/ |
Adaptive state estimation: χ² anomaly gating and IAE |
certification/ |
Machinery answering "is this inequality provably true", as distinct from "did a float suggest so" |
batch/ |
NumPy/CuPy backend abstraction; batched common-outer-grid integrator — a Monte Carlo batch as a rank-3 tensor operation |
viz/ |
Textured WGS84 ellipsoid, terrain and Blue Marble Next Generation imagery tiles, vehicle glyphs, and scene — a chase-camera rig with polyline, mesh and glyph projection over the globe |
verification/ |
Executable verification tasks with failure criteria stated in advance |
pip install -e ".[dev]"
pip install -e ".[atmosphere]" # optional: MSIS thermosphere
pip install -e ".[reanalysis]" # optional: ERA5 winds
pip install -e ".[cuda]" # optional: GPU batch backendpytest tests -q # 604 tests
python -m aether.verification # verification tasks -> results/Each verification task states its failure criterion before it runs and writes a
timestamped Markdown report with the environment recorded. Criteria for the numerics tasks
are inherited from earlier manuscripts on the fixed-grid spectral method and its plate and
aerothermal applications; the R1- prefixed tasks serve this reachability series.
This repository is public and holds a one-way dependency boundary: the public kernel must
not import controlled code, which lives in a separate repository rather than in an ignored
subdirectory here. An ignored directory is one git add -f away from being published; a
separate repository is not. The boundary is checked by
tools/check_boundary.py.
Vehicle parameters throughout are generic and individually cited — a plausible lifting body with published mass properties and reference dimensions, traceable to no system.
MIT. See LICENSE.