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

IndisputableMonolith.Gravity.Candidates.Podkletnov

show as:
view Lean formalization →

The Podkletnov module encodes the claimed gravity effect magnitude range of 0.3% to 2.1% as a falsifiable interface inside the Recognition Science gravity candidates. Experimental physicists working on rotating superconductor weight-loss tests would cite it when building data predicates. The module structures its argument through four sibling definitions that import executable trace predicates from Flight.Falsifiers and the ILG weight kernel connection from GravityBridge.

claimThe Podkletnov candidate effect magnitude satisfies $0.003 < |w - w_0|/w_0 < 0.021$ under the ILG weight kernel, with auxiliary predicates for vacuum persistence, resonant speed, and material independence.

background

This module resides in Gravity.Candidates and imports Flight.Falsifiers, whose doc-comment states that it supplies executable predicates over recorded traces to encode what must be true in data if the physical hypotheses hold. It also imports Flight.GravityBridge, which connects the ILG weight kernel from Gravity.ILG to the Flight/Propulsion model and poses the question of T_dyn for a rotating lab device. The local setting therefore treats the Podkletnov claim as one concrete candidate whose magnitude range is declared alongside three supporting falsifier interfaces.

proof idea

This is a definition module, no proofs. It declares the main objects via the four sibling definitions claimed_effect_range, VacuumPersistence, ResonantSpeedFalsifier, and MaterialIndependence, each of which supplies a predicate or range that downstream falsification code can invoke directly.

why it matters in Recognition Science

The module supplies the Podkletnov candidate interface that populates the falsification pipeline begun in Flight.Falsifiers. It fills the concrete magnitude step (0.3% to 2.1%) required by the Recognition Science gravity candidate list, allowing the ILG weight kernel from GravityBridge to be tested against rotating-lab data without committing to any underlying mechanism.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)