Evidence map

Every claim of the lessons with its type, its scope, and the cell, reference, dataset card, or Lean theorem that supports it.

A lesson marks each statement that a reader could take for a scientific result as a claim and gives it a type: observational, experimentally supported, numerically verified, or formal theorem. The type says what kind of evidence stands behind the statement. This page lists every claim of the site, lesson by lesson, with its scope and the evidence it names. The claim links to its place in the lesson. The evidence is one of these:

• a cell of the lesson that the build runs again;
• a curated reference of the register, an outbound link;
• a dataset card of the repository;
• a theorem that Lean checks;
• a recorded run of an agent that the build replays.

A claim without evidence, or with evidence that does not exist, stops the build, so every row below has a target. The page is generated from the lessons when the site is built. Where a statement quotes a value that the lesson computes, the value is shown as “…”; the lesson has it.

Kinematics as a program

Claims of Kinematics as a program, with their evidence.

Claim	Type	Scope	Evidence
For a constant acceleration the position error of explicit Euler is exactly $-\tfrac{1}{2}\,a\,t_n\,\Delta t$.	Numerically verified	constant acceleration	Cell fig-ball-thrown-up
On logarithmic axes both errors follow the reference line of slope one, so the error of explicit Euler is proportional to the time step in both examples.	Numerically verified	two motions	Cell fig-error-against-time-step

Newton’s laws as a first-order system

Claims of Newton’s laws as a first-order system, with their evidence.

Claim	Type	Scope	Evidence
Explicit Euler on linear drag converges to the terminal velocity only for $\Delta t < 2\tau$, and alternates around it for $\Delta t > \tau$.	Numerically verified	linear drag, explicit Euler	Cell large-step-velocity

Projectile motion with quadratic drag

Claims of Projectile motion with quadratic drag, with their evidence.

Claim	Type	Scope	Evidence
With quadratic drag the longest throw is flatter than $45^\circ$ for this ball.	Numerically verified	tennis ball at its launch speed	Cell fig-range-against-angle

The harmonic oscillator

Claims of The harmonic oscillator, with their evidence.

Claim	Type	Scope	Evidence
Every ratio of successive energies equals the derived factor to round-off.	Numerically verified	explicit Euler on the harmonic oscillator, any step	Cell euler-energy-ratios

Numerical integrators

Claims of Numerical integrators, with their evidence.

Claim	Type	Scope	Evidence
Explicit Euler has multiplied the energy by … in three periods.	Numerically verified	the oscillator at this step	Cell state-after-three-periods
The observed orders settle at the orders of the explanation: one, one, two, and four.	Numerically verified	the oscillator, two periods	Cell error-orders; Cell fig-integrators-convergence
The symplectic methods are still within their bands, which are no wider after a thousand periods than after one.	Numerically verified	the oscillator at this step	Cell long-run-energy-bands
For one millimetre over two periods, Runge-Kutta needs … calls, velocity Verlet …, symplectic Euler …, and explicit Euler ….	Numerically verified	the oscillator, tolerance of one millimetre	Cell calls-for-one-millimetre

Energy conservation

Claims of Energy conservation, with their evidence.

Claim	Type	Scope	Evidence
The simulation reproduces the exact period to the four digits shown at every amplitude	Numerically verified	classical Runge-Kutta method, all five amplitudes of the table	Cell period-table
The four behaviours are the ones the previous lesson derived on the oscillator	Numerically verified	pendulum at the amplitude and the step of the example	Cell fig-pendulum-energy
The drift of the two first-order methods halves with the step, the drift of velocity Verlet falls by the factor of the second order, and the drift of the classical Runge-Kutta method falls by about … when the step halves	Numerically verified	pendulum at the amplitude of the example, over the four steps of the table	Cell drift-orders
The formula gives the energy gain of one step to the leading order	Numerically verified	explicit Euler on the pendulum, three states of the motion of the examples	Cell step-energy-gain
The lag grows in proportion to the number of swings for every method	Numerically verified	the three stable methods, the amplitude and the step of the example	Cell period-lag
From there the simulation describes a rotating pendulum, a different motion from the one that was asked for	Numerically verified	explicit Euler, the step and the release of this example	Cell fig-pendulum-over-the-top

Momentum and collisions

Claims of Momentum and collisions, with their evidence.

Claim	Type	Scope	Evidence
Every method conserves the total momentum and keeps the centre of mass on its straight line within the bound, explicit Euler included.	Numerically verified	two particles, a spring, the step shown	Cell result-pair-conservation
which shows that the two-particle simulation reproduces the one-particle problem of the reduced mass	Numerically verified	spring pair, fourth-order method	Cell fig-pair-on-a-spring
The soft spheres leave with the hard-sphere velocities to the digits shown	Numerically verified	head on, this stiffness, the step shown	Cell fig-head-on-collision
The error shrinks with the step, but not smoothly: the force has a kink where the spheres touch, and where the step lands relative to it changes from one row to the next.	Numerically verified	head on, velocity Verlet, this stiffness	Cell result-steps-per-contact
from twenty steps per contact on, the drift lies within … per cent of the band	Numerically verified	from twenty steps per contact	Cell result-steps-per-contact
The spheres leave at a right angle for every stiffness, to within …$^\circ$	Numerically verified	equal masses, target at rest, five stiffnesses	Cell result-stiffness-sweep
The difference from the hard-sphere deflection falls by a factor between … and … for each factor of ten in the stiffness over the four stiffest rows, near $\sqrt{10} =$ …	Numerically verified	equal masses, offset at half the diameter, stiffness from the second row up	Cell result-stiffness-sweep

The Kepler orbit

Claims of The Kepler orbit, with their evidence.

Claim	Type	Scope	Evidence
The two symplectic methods conserve the angular momentum to round-off at a step of a hundredth of an orbit, while explicit Euler and the classical Runge-Kutta method do not.	Numerically verified	the example orbit at this step	Cell four-methods-two-orbits
Velocity Verlet shows its second order at once, and the classical Runge-Kutta method approaches its fourth from above as the step becomes small enough for the fast perihelion passage.	Numerically verified	the example orbit, two orbits	Cell observed-orders
Velocity Verlet’s energy band is as wide after a thousand orbits as after one, its angular momentum is exact to round-off, and the semi-major axis stays within … per cent of the truth for the whole run.	Numerically verified	the example orbit at this step	Cell thousand-orbits; Cell fig-orbit-thousand
The classical Runge-Kutta method holds the direction but loses energy at every step, so its ellipse shrinks by … per cent in a thousand orbits, and with it the period.	Numerically verified	the example orbit at this step	Cell thousand-orbits; Cell fig-orbit-thousand
The precession falls by a factor of four when the step halves.	Numerically verified	velocity Verlet, the example orbit	Cell precession-against-step
The two simulations agree, as they must: the same method and the same step applied to the same equations in two forms.	Numerically verified	velocity Verlet, five orbits	Cell two-body-simulation
The first planet confirmed around a star like the Sun was found this way.	Observational	the radial velocity method	Reference doppler-spectroscopy-overview
The overview of the radial velocity method quotes the same effect for Jupiter and the Sun: about 12.4 m/s (not verified), as the change of the speed of the Sun over one orbit of Jupiter.	Observational	the Sun and Jupiter, as quoted	Reference doppler-spectroscopy-overview

Automated analysis pipelines

Claims of Automated analysis pipelines, with their evidence.

Claim	Type	Scope	Evidence
Drag moves the angle of the longest throw below the drag-free value of forty-five degrees, to … degrees on the grid.	Numerically verified	this ball, speed, and air	Cell fine-sweep
The first-order propagation and the Monte Carlo spread differ by … per cent at the best angle.	Numerically verified	this throw and a speed uncertainty of under two per cent	Cell monte-carlo-check
The change of the RMS elevation with the end of the window is … times the standard error of the five repetitions.	Experimentally supported	gauge five of the first wave condition, windows from five seconds to the ends shown	Cell window-sweep; Card aalborg-submerged-bar
All three runs have a smaller RMS elevation than the measurement, by … to … per cent, and their periods agree with it within the resolution of the window.	Experimentally supported	gauge five of the first wave condition, window as stated	Cell model-comparison; Card aalborg-submerged-bar

Gravitational-wave strain lab

Claims of Gravitational-wave strain lab, with their evidence.

Claim	Type	Scope	Evidence
The frequency of the integrated inspiral and the closed form agree to … in relative terms over the first … percent of the time to coalescence, and the frequency of the starting orbit from orbital_elements is … Hz, as it was set.	Numerically verified	circular orbit, leading order, the example masses	Cell inspiral-check
The whitened strains of the two detectors correlate at the event with a coefficient of magnitude … at a delay of … milliseconds, with the sign reversed and the Livingston detector first. The same procedure on the … quiet windows of the segment never gives more than ….	Observational	whitened and band-passed strain, windows of a fifth of a second, delay searched within the light travel time	Cell detector-correlation; Card gw150914-strain
The published chirp mass of this event is quoted from the GWOSC record of the event, in the source frame, with its redshift.	Observational	as quoted, source frame	Card gw150914-strain
The fit of the Newtonian chirp to the measured strain gives a detector-frame chirp mass of … solar masses, with a statistical interval of … to … and a spread of … to … over the analysis choices. It is … percent above the published value.	Experimentally supported	Newtonian-order model, window ending before the merger, white-noise assumption	Cell primary-fit; Cell sensitivity; Card gw150914-strain

Inverse physics: parameters from observations

Claims of Inverse physics: parameters from observations, with their evidence.

Claim	Type	Scope	Evidence
Over … synthetic data sets the fit recovers every parameter of the damped oscillation with a bias below … of its value, its stated standard errors are the size of the scatter of the estimates, and its intervals of two standard errors hold the truth in at least … percent of the trials.	Numerically verified	damped oscillation, 120 samples, Gaussian noise of known size, fits started within 20 percent of the truth	Cell recovery
A free oscillation fitted with the mass and the spring constant as separate parameters is reported as not identified: the helper flags both parameters, and the profile of the spring constant stays within … of its minimum over a tenfold range, so no interval for either exists.	Numerically verified	free oscillation of a mass on a spring, noise of 0.05, 120 samples	Cell tied-parameters
A fit of the exponentially damped oscillation to data with a linear loss converges with small standard errors and a reduced chi-square of …, and the verdict of the helper lists structure in its residuals; the same fit to data of the right model lists none.	Numerically verified	one seeded data set of each kind, noise of 0.05, 120 samples	Cell wrong-model
The fit of the Newtonian chirp to the measured strain gives a detector-frame chirp mass of … solar masses with a profile interval of … on each side. A known chirp of … solar masses added to four stretches of strain without an event is recovered with a root-mean-square error of … solar masses where the stated intervals averaged …, and the choice of band moves the fitted value between … and …; the estimate is … solar masses above the published detector-frame value of ….	Experimentally supported	Newtonian-order chirp, window of 0.2 s before the event time, four off-source stretches, three bands, noise estimated from the file	Cell injection; Cell band-spread; Cell primary-fit; Card gw150914-strain

Double pendulum and chaos

Claims of Double pendulum and chaos, with their evidence.

Claim	Type	Scope	Evidence
The simulated periods of both modes agree with the closed form to the four digits shown	Numerically verified	equal masses and rods, amplitude of one thousandth of a radian, classical Runge-Kutta method	Cell modes-and-energy
The energy stays within a small fraction of its start in both regimes	Numerically verified	the two starts of the table, fifty seconds, classical Runge-Kutta method with the stated step	Cell energy-drift
The estimate for the regular start falls with the length of the run and ends near zero, and the estimate for the chaotic start is positive and steady	Numerically verified	the two starts, one hundred seconds, classical Runge-Kutta method, separation one hundred-millionth	Cell lyapunov-table
The estimator recovers the known exponent to a fraction of a per cent	Numerically verified	the linear hyperbolic point, thirty seconds	Cell known-exponent

Lagrangian mechanics

Claims of Lagrangian mechanics, with their evidence.

Claim	Type	Scope	Evidence
The equation from the Lagrangian is the Newtonian one	Numerically verified	the pendulum, four angles, any velocity because the force does not depend on it	Cell pendulum-check
The simulated period of the Lagrangian pendulum is the closed-form one	Numerically verified	amplitude of one and a half radians, classical Runge-Kutta method	Cell pendulum-period
The Lagrangian reproduces both normal-mode frequencies	Numerically verified	the stated masses and springs	Cell coupled-springs
The angular momentum $p_\phi$ and the energy are constant over the orbit to the accuracy of the method	Numerically verified	one bound orbit, classical Runge-Kutta method	Cell planet
The closed-form accelerations of the double pendulum agree with the Euler-Lagrange equations of its Lagrangian	Numerically verified	unequal masses and rods, two hundred random states and a regular start	Cell double-pendulum-check

Hamiltonian mechanics

Claims of Hamiltonian mechanics, with their evidence.

Claim	Type	Scope	Evidence
The Legendre transform of the program reproduces the energy written in the momenta	Numerically verified	the pendulum at three points and the coupled springs at one	Cell legendre
The determinants of symplectic Euler and velocity Verlet are one for both steps, to the accuracy of the derivative	Numerically verified	the pendulum at one state, two step lengths	Cell determinants
The two symplectic methods keep the area to the accuracy of the polygon of the images, and explicit Euler enlarges it	Numerically verified	one circle of starts, two small-angle periods, fifty steps per period	Cell blob
Each symplectic method conserves its modified energy of the earlier lessons to round-off, while its energy oscillates	Numerically verified	the oscillator, sixteen steps per period, twenty periods	Cell modified-oscillator
The band of the energy shrinks by about a factor of two when the step is halved, as a first-order method, and the band of the modified energy by about a factor of four, as the first correction removed and the next left	Numerically verified	the pendulum at one amplitude, twenty periods, three steps	Cell modified-pendulum

Resonance and driven oscillators

Claims of Resonance and driven oscillators, with their evidence.

Claim	Type	Scope	Evidence
The simulated motion of the driven oscillator agrees with the exact solution at every instant, the transient included	Numerically verified	one driving frequency, forty seconds, classical Runge-Kutta method at the stated step	Cell closed-form-check
The simulated resonance curve agrees with the analytic amplitude at every frequency	Numerically verified	forty-three frequencies, classical Runge-Kutta method, amplitude read after eight decay times	Cell resonance-curve
The quality factor read from the width of the simulated curve is the one that the parameters give, to the accuracy of the sampling of the curve	Numerically verified	one oscillator, the samples of the curve above	Cell peak-and-width

Random walks and diffusion

Claims of Random walks and diffusion, with their evidence.

Claim	Type	Scope	Evidence
The diffusion coefficient measured from the mean squared displacement agrees with $\ell^2/(4\tau)$ within the tolerance of four standard errors, and a prediction twice as large is rejected.	Numerically verified	equal steps in the plane, six runs of five hundred walkers, four standard errors	Cell diffusion-check; Cell diffusion-summary
The fraction of walkers within a radius agrees with $1 - \exp(-R^2/4Dt)$ at three radii within four standard errors.	Numerically verified	the last step of the walk, six runs, four standard errors	Cell radial-check

Kinetic theory of gases

Claims of Kinetic theory of gases, with their evidence.

Claim	Type	Scope	Evidence
The speeds of the relaxed gas follow the Maxwell distribution at its own temperature: the measured fraction below each of five quantile speeds agrees with the predicted fraction within four standard errors.	Numerically verified	a dilute gas of hard discs in two dimensions, six seeds, five quantiles, four standard errors	Cell quantile-check

Entropy from ensembles

Claims of Entropy from ensembles, with their evidence.

Claim	Type	Scope	Evidence
The mean number of particles on the left follows $N/2 + (n_0 - N/2)(1 - 1/N)^t$ within four standard errors at the four steps shown.	Numerically verified	twelve particles, five thousand boxes per run, six runs, four standard errors	Cell mean-check
At equilibrium the entropy of the ensemble, estimated from the observed frequencies with the first-order correction of the bias, agrees with $N\ln 2$ within four standard errors at three sizes of ensemble.	Numerically verified	twelve particles, six runs, four standard errors, bias corrected to first order	Cell equilibrium-check

The wave equation

Claims of The wave equation, with their evidence.

Claim	Type	Scope	Evidence
The computed field follows the exact solution of d’Alembert with a mirror image behind the fixed end.	Numerically verified	a Gaussian pulse, fixed ends, Courant number one half, four hundred cells	Cell pulse-run
The error of the scheme falls as the second power of the grid spacing at a fixed Courant number.	Numerically verified	a pulse and a standing mode, fixed ends, Courant number one half, grids of fifty to eight hundred cells	Cell convergence
Up to a Courant number of one the field stays at the size of its start; above it the zigzag grows by the factor that the stability calculation predicts.	Numerically verified	a zigzag of size 1e-10, free ends, sixty cells, forty steps	Cell cfl-run

Interference and resonance

Claims of Interference and resonance, with their evidence.

Claim	Type	Scope	Evidence
The field of two pulses released together equals the sum of the fields of each released alone.	Numerically verified	two Gaussian pulses, fixed ends, Courant number one half	Cell superposition-run
The peaks of the spectrum of a simulated plucked string lie at the analytic frequencies $n c / 2L$, and no peak lies at the third, which has a node at the pluck.	Numerically verified	a string plucked at a third, fixed ends, two hundred cells, twenty periods recorded	Cell modes-run
A force at the frequency of a mode makes its amplitude grow in proportion to the time, and a force at another frequency leaves it bounded; the simulation follows both exact formulas.	Numerically verified	the first mode, fixed ends, one hundred cells, ten periods	Cell resonance-run
The frequencies of the scheme follow its dispersion relation, which departs from $\omega = ck$ for waves of a few cells.	Numerically verified	one hundred cells, Courant number one half, modes from the first to the eightieth	Cell dispersion-run
A packet of short waves on the grid travels slower than the wave speed of the equation it solves, at the group velocity of the scheme.	Numerically verified	one packet, carrier of a few cells per wavelength, Courant number one half	Cell packet-run
The intensity of two coherent sources, found by adding their waves, follows $4\cos^2(\pi d\sin\theta/\lambda)$ in the far field.	Numerically verified	two sources five wavelengths apart, a screen twenty thousand wavelengths away	Cell interference-run

Sound, resonance, and the Doppler effect

Claims of Sound, resonance, and the Doppler effect, with their evidence.

Claim	Type	Scope	Evidence
The first three resonances of a simulated pipe agree with $n c/2L$ for the pipe open at both ends and with $(2n-1)c/4L$ for the pipe closed at one end.	Numerically verified	a uniform pipe, ideal ends, one hundred sixty cells, a record of four tenths of a second	Cell pipe-run
A pipe driven at a range of frequencies answers at its resonances, the frequencies of its modes.	Numerically verified	a closed pipe, forty cells, a tenth of a second of driving, steps of the stated spacing	Cell sweep-run
The frequency heard from a moving source follows $f_0 c/(c - v_s)$, and the frequency heard by a moving listener follows $f_0 (c + v_o)/c$, to a relative difference below the tolerance.	Numerically verified	a tone, motion on a line through still air at speeds up to a third of the speed of sound	Cell doppler-run

Electric fields, superposition, and the potential

Claims of Electric fields, superposition, and the potential, with their evidence.

Claim	Type	Scope	Evidence
The sum of the Coulomb fields equals minus the gradient of the summed potential: the two differ by an amount that falls as the square of the step of the difference.	Numerically verified	three point charges, one point at a distance of centimetres, steps from a millimetre down	Cell gradient-run
The field of a pair of opposite charges approaches the field of a dipole with the same moment, and the relative difference falls as the square of the separation over the distance.	Numerically verified	a pair of equal and opposite point charges, distances from five to eighty separations	Cell dipole-run
The flux of the field of point charges out through a sphere is the charge inside divided by $\varepsilon_0$; charges outside the sphere add nothing, whatever their distance.	Numerically verified	four point charges, spheres that do not pass close to a charge	Cell gauss-run

Charged particles in electric and magnetic fields

Claims of Charged particles in electric and magnetic fields, with their evidence.

Claim	Type	Scope	Evidence
A proton in a uniform magnetic field circles at the cyclotron frequency $qB/m$ on the Larmor radius $mv/(qB)$; the frequency and the radius of the Boris orbit converge to both with order two in the step, and agree with the pusher’s own closed forms to round-off.	Numerically verified	a non-relativistic proton, a uniform field, ten turns, steps from a twentieth of a period down	Cell cyclotron-run
In a magnetic field the Boris pusher keeps the kinetic energy to round-off, while explicit Euler multiplies it by $1 + (\omega_c\Delta t)^2$ at every step.	Numerically verified	a uniform magnetic field, eighty steps per turn, five turns	Cell energy-run
In crossed uniform fields the centre of the orbit drifts with $\mathbf{E}\times\mathbf{B}/B^2$, at right angles to both fields and in the same direction for a positive and a negative charge.	Numerically verified	uniform crossed fields, a drift far slower than light, fifty turns	Cell drift-run

Induction: magnetic flux and the electromotive force

Claims of Induction: magnetic flux and the electromotive force, with their evidence.

Claim	Type	Scope	Evidence
The EMF of a loop moving through a static, non-uniform magnetic field, computed from the force $\mathbf{u}\times\mathbf{B}$ on the charges of the wire, equals minus the rate of change of the flux through the loop.	Numerically verified	a rigid rectangular loop translated through a static field, a central difference of the stated step	Cell moving-loop-run
The EMF of a coil turning in a uniform field, computed from the force on the charges of the moving wire, equals minus the rate of change of its flux and follows $B A\omega\sin\omega t$.	Numerically verified	a flat rectangular coil of one turn, a uniform field across its axis, one turn	Cell coil-run
For a loop at rest in a changing magnetic field, the line integral of the induced electric field around the loop equals minus the rate of change of the flux through it, for a loop around the field, beside it, and across its edge.	Numerically verified	square loops at rest near a smooth tube of field that grows at a constant rate, induced field from the vector potential	Cell tube-run

An agent runs an experiment

Claims of An agent runs an experiment, with their evidence.

Claim	Type	Scope	Evidence
At the smallest time step the agent used, the two angles it tried with the longest ranges bracket the best angle of an independent scan of the simulation, and the best angle lands the ball further than forty-five degrees by the amount in the table.	Numerically verified	the simulated tennis ball with quadratic drag at 25 m/s, explicit Euler at the smallest allowed step, no measurement	Cell agent-conclusion

Discovering a force law with controlled probes

Claims of Discovering a force law with controlled probes, with their evidence.

Claim	Type	Scope	Evidence
The law the agent submitted predicts the force at the held-out distances within the tolerance of the protocol: the outcome is ….	Numerically verified	the simulated central force of this protocol, one recorded run, one seed	Cell d1-score; Replayed run replay
A least-squares fit to the agent’s own readings also recovers the law, with standard errors of the size the noise allows.	Numerically verified	the four readings of the recorded run	Cell d1-probe-fit

Full, partial, and no prior knowledge under one protocol

Claims of Full, partial, and no prior knowledge under one protocol, with their evidence.

Claim	Type	Scope	Evidence
Across the three conditions the model, the system prompt, the tools, the budget, the step limit, the seed, the tolerance, and the held-out settings are the same, and only the task text differs.	Numerically verified	the protocol and the run records of this lesson	Cell d2-fairness
Scored on the same held-out settings, the claim of the full condition recovers the law and the claims of partial and none do not.	Numerically verified	one recorded run per condition, one seed, the simulated spring of this protocol	Cell d2-scores; Replayed run replay-full; Replayed run replay-partial; Replayed run replay-none
The readings of every one of the three runs determine the frequency well enough to recover the law: a least-squares fit to each run’s own readings has a held-out error within the tolerance.	Numerically verified	the readings of the three recorded runs	Cell d2-probe-fits

Unlearning a familiar law: a modified force

Claims of Unlearning a familiar law: a modified force, with their evidence.

Claim	Type	Scope	Evidence
The inverse-square law does not describe the readings of this world: its chi-square is far beyond what the noise gives, and its prediction at the held-out distances is off by more than the tolerance.	Numerically verified	the simulated modified central force, the grid of the protocol’s budget	Cell d3-familiar
Least squares of the free family, on the grid and on random settings, recovers the modified law: its claim predicts the held-out distances within the tolerance.	Numerically verified	the simulated modified central force, one seed, the protocol’s budget	Cell d3-baselines
The agent’s claim is scored … by the protocol: it did not fall back on the inverse square, and its law predicts the held-out distances within the tolerance.	Numerically verified	one recorded run, one seed, the simulated modified central force	Cell d3-score; Replayed run replay

Particles in a box

Claims of Particles in a box, with their evidence.

Claim	Type	Scope	Evidence
Starting from one speed, the gas approaches the Maxwell value of the moment ratio, passing a ratio of …, before the measurement begins.	Numerically verified	this gas, twelve seeds, the stated time step	Cell relaxation-history
The moment ratio of the relaxed gas agrees with the Maxwell value two, and the pressure with the virial prediction that includes the area of the discs, by the rule of the lesson; the ideal gas law alone does not.	Numerically verified	a dilute gas of hard discs in two dimensions, twelve seeds, the stated time step, the stated allowances, a false-failure probability of one in a thousand	Cell kinetic-theory-check

Proving what the simulation showed

Claims of Proving what the simulation showed, with their evidence.

Claim	Type	Scope	Evidence
For a particle with constant acceleration, $v^2 = v_0^2 + 2a(x - x_0)$ at every time.	Formal theorem	motion on a line with the position and velocity formulas as hypotheses, real arithmetic, any start, acceleration, and time	Theorem velocity_sq_of_constant_acceleration
In the same motion the distance covered is the mean of the initial and the final velocity times the time.	Formal theorem	the same hypotheses	Theorem displacement_of_mean_velocity
One step of explicit Euler on the harmonic oscillator multiplies the energy by $1 + (k/m)\,\Delta t^2$.	Formal theorem	positive mass, Hooke’s law, the explicit Euler update, any state and any step size, real arithmetic	Theorem euler_energy_step
For a positive spring constant, a step of non-zero size, and a positive energy, one step of explicit Euler makes the energy strictly greater.	Formal theorem	the hypotheses of the one-step theorem and `hk`, `hdt`, `hE`, real arithmetic	Theorem euler_energy_grows
After $n$ steps of explicit Euler the energy is $(1 + k\,\Delta t^2/m)^n$ times the initial energy.	Formal theorem	the same model for a whole run, every step obeying the hypotheses, any number of steps, real arithmetic	Theorem euler_energy_after_steps
Along the exact motion the residual of the identity is zero to round-off.	Numerically verified	one throw, nine instants, doubles	Cell exact-residual
On the explicit Euler fall under constant acceleration, the residual of the identity is $a^2\,t\,\Delta t$.	Numerically verified	constant acceleration, explicit Euler, any step; derived above and recomputed here for one step size	Cell euler-residual
The energy of the simulated oscillator follows the factor of the theorem at every step.	Numerically verified	one oscillator, one step size, doubles	Cell energy-factor

Momentum in a collision, proved

Claims of Momentum in a collision, proved, with their evidence.

Claim	Type	Scope	Evidence
For two particles of positive mass, the collision rule conserves the total momentum along every axis, for all velocities and every direction.	Formal theorem	the instantaneous collision rule of two hard spheres, real arithmetic	Theorem collision_momentum
The change of momentum of the first sphere is the negative of the change of momentum of the second.	Formal theorem	the same rule, real arithmetic	Theorem collision_impulses

What symplectic Euler conserves

Claims of What symplectic Euler conserves, with their evidence.

Claim	Type	Scope	Evidence
One step of symplectic Euler on the harmonic oscillator leaves the modified energy unchanged.	Formal theorem	symplectic Euler on a mass of positive mass on a spring, any step size, real arithmetic	Theorem symplectic_modified_energy_step
After any number of steps of symplectic Euler, the modified energy equals its initial value.	Formal theorem	symplectic Euler on the oscillator, any step size and any number of steps, real arithmetic	Theorem symplectic_modified_energy_after_steps
For a spring constant that is positive and a step with $k\,\Delta t^2 < 4m$, the modified energy is never negative.	Formal theorem	the step sizes below the stated limit, real arithmetic	Theorem modified_energy_nonneg

The chirp law, proved

Claims of The chirp law, proved, with their evidence.

Claim	Type	Scope	Evidence
If a circular orbit loses energy at the quadrupole power, its separation shrinks at the rate $-\tfrac{64}{5}G^3 m_1 m_2 (m_1+m_2)/(c^5 a^3)$.	Formal theorem	two positive masses on a circular orbit, the quadrupole power taken as a hypothesis, real arithmetic	Theorem shrink_rate_of_energy_loss
With Kepler’s third law, the rate of change of the orbital angular frequency satisfies $(\omega')^3 = (96/5)^3 (G\mathcal{M}/c^3)^5\omega^{11}$ with the chirp mass defined by $\mathcal{M}^5 = (m_1 m_2)^3/(m_1 + m_2)$.	Formal theorem	the same model, real arithmetic	Theorem chirp_rate_cubed
A frequency and its rate of change determine the chirp mass: two positive chirp masses that satisfy the law with the same $\omega$ and $\omega'$ are equal.	Formal theorem	positive constants, a non-zero frequency, real arithmetic	Theorem chirp_mass_unique
Where $(\omega')^3 = K\omega^{11}$ holds on a neighbourhood of an instant, the quantity $3\omega/(8\omega')$ decreases at the rate one at that instant.	Formal theorem	a local identity at one instant, for a rising frequency with a differentiable rate, real arithmetic	Theorem coalescence_countdown