pith. machine review for the scientific record. sign in
theorem proved term proof high

anomaly_dissolved

show as:
view Lean formalization →

Researchers cite this result to confirm that thermal thrust remains non-negative in the flyby anomaly model. It supports the dissolution of the anomaly under standard physics without beyond-standard-model contributions. The proof reduces immediately to the bsm_not_needed theorem via direct reference.

claim$F = P_{asym}/c$ satisfies $F >= 0$, where $P_{asym}$ is the asymmetric thermal power component.

background

The Flyby Anomaly module treats unexpected energy changes during Earth gravity assists. Recognition Science concludes that thermal effects plus gravity model updates suffice. Thermal thrust is defined as spacecraft thermal power times asymmetry factor divided by the speed of light. The bsm_not_needed theorem shows this quantity is non-negative by unfolding the definition and applying non-negativity lemmas to each factor.

proof idea

It is a one-line wrapper that directly invokes the bsm_not_needed theorem.

why it matters in Recognition Science

This theorem completes the EA-008 analysis by verifying the sign of thermal thrust. It feeds the ea008_certificate that declares the anomaly dissolved. The result aligns with the framework's pattern of dissolving anomalies via thermal and gravity models, consistent with the phi-ladder and eight-tick structures used in related muon g-2 work.

scope and limits

formal statement (Lean)

  98theorem anomaly_dissolved : thermal_thrust ≥ 0 := bsm_not_needed

proof body

Term-mode proof.

  99
 100/-- **THEOREM EA-008.10**: Pattern consistent with thermal hypothesis.
 101    The thermal thrust is non-negative, consistent with a thermal explanation. -/

used by (3)

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

depends on (12)

Lean names referenced from this declaration's body.