Trace
plain-language theorem explainer
Trace supplies the minimal record schema for experimental flight data consisting of time-indexed ambient pressure, a commanded drive schedule, and measured thrust vectors. Propulsion experimenters cite this structure when feeding traces into falsifier predicates that test non-aerodynamic claims. The declaration is a bare structure definition carrying no proof obligations or computational content.
Claim. A structure Trace with fields ambientPressure : ℕ → ℝ (pressure at each tick), schedule : DriveSchedule (pulse sequence), and thrust : ℕ → Vec3 (thrust vector at each tick).
background
The Flight.Falsifiers module encodes executable predicates that must hold on recorded data if the underlying physical hypotheses are correct. Trace serves as the common input type for these predicates. It relies on the fundamental tick time quantum from Constants.tick together with the DriveSchedule and Vec3 types supplied by the Schedule and Thrust modules. Module documentation states that the falsifiers begin as simple interfaces and are intended to become stricter as the model tightens.
proof idea
The declaration is a structure definition. It directly introduces the three named fields with no lemmas applied and no reduction steps.
why it matters
Trace is the data type consumed by BandingFalsifier, PhaseLockFalsifier, SignFlipFalsifier, and VacuumTestFalsifier, and by the Podkletnov VacuumPersistence check. It supplies the experimental interface layer that lets downstream statements operate on concrete traces, directly supporting the vacuum-persistence requirement that distinguishes the model from aerodynamic alternatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.