pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Flight.Falsifiers

show as:
view Lean formalization →

Minimal experimental trace schema for the Flight subtheory in Recognition Science. It defines a core Trace type together with four falsifier predicates (VacuumTestFalsifier, BandingFalsifier, SignFlipFalsifier, PhaseLockFalsifier) that isolate testable signatures of thrust observables. Researchers formalizing φ-vortex propulsion or Podkletnov-style gravity shielding cite the module to keep experimental hypotheses explicit and extensible. The module reuses 8-tick scheduling and thrust interfaces from its imports and contains no proofs.

claimA display-level schema consisting of a trace type $T$ and falsifier predicates $F_V$, $F_B$, $F_S$, $F_P$ for vacuum, banding, sign-flip and phase-lock tests on flight thrust observables.

background

The Flight subtheory scaffolds Spiral-Field Propulsion as a φ-Vortex Drive. Schedule supplies the 8-tick control discipline that reuses neutrality predicates from SpiralField. Thrust supplies a vector type and placeholder thrust observable without attempting surface integrals or control-volume derivations. The Falsifiers module sits at the experimental interface, providing a minimal, intentionally small schema that can be extended.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the falsifier interface required by the Flight facade, which re-exports submodules while isolating physical hypotheses. It is imported by Flight.Report to expose proved-versus-assumed indicators and by Gravity.Candidates.Podkletnov to formalize the rotating YBCO disk weight-reduction claim (0.3 %–2.1 %) inside the Recognition framework.

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)