Trace
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not attach units or calibration to pressure and thrust values.
- Does not include temperature, power, or other sensor channels.
- Does not model measurement uncertainty or noise.
- Does not enforce any relation between schedule and observed thrust.
formal statement (Lean)
26structure Trace where
27 /-- Ambient pressure (e.g., vacuum chamber pressure) as a function of time tick. -/
28 ambientPressure : ℕ → ℝ
29 /-- Commanded schedule (pulse/no-pulse). -/
30 schedule : Schedule.DriveSchedule
31 /-- Measured thrust vector (or inferred acceleration proxy). -/
32 thrust : ℕ → Thrust.Vec3
33
34/-- Vacuum persistence falsifier:
35
36If thrust remains nonzero while ambient pressure is lowered below a threshold,
37then the claim is *consistent* with non-aerodynamic propulsion.
38
39(This is a *one-way* falsifier: failure does not disprove the model unless
40we control for other conditions.)
41-/