pith. sign in
module module high

IndisputableMonolith.Flight.Falsifiers

show as:
view Lean formalization →

Flight.Falsifiers supplies minimal experimental trace schemas for the Flight propulsion scaffold. It defines display-level falsifiers including VacuumTestFalsifier, BandingFalsifier, SignFlipFalsifier, and PhaseLockFalsifier that draw on the 8-tick schedule and thrust observables. Physicists testing RS predictions in propulsion would reference these when constructing experiments. The module is kept small for extensibility and serves as an interface layer.

claimThe module defines experimental falsifiers Trace, VacuumTestFalsifier, BandingFalsifier, SignFlipFalsifier, PhaseLockFalsifier as display-level trace schemas for the thrust observable and 8-tick schedule in spiral-field propulsion.

background

The Flight domain formalizes a minimal control surface for φ-Vortex Drive propulsion. Upstream Schedule defines the 8-tick control discipline reusing neutrality predicates from SpiralField, while Thrust provides a vector type and placeholder thrust observable without full continuum derivation. This module focuses on minimal experimental trace schemas at display level, intentionally small and extensible. It supports the isolation of physical hypotheses as explicit assumptions in the broader Recognition Science framework.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module is imported by the main Flight facade to re-export submodules, by Flight.Report for lightweight indicators of proved versus assumed content, and by Gravity.Candidates.Podkletnov to formalize the Podkletnov gravity shielding claim within RS. It supplies the falsification tools needed to test the 8-tick octave and thrust predictions against experiment.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)