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

IndisputableMonolith.Gravity.Candidates.Searl

show as:
view Lean formalization →

This module assembles the SEG geometry under the Law of the Squares and checks alignment with φ-spiral pitch families from Recognition Science. It imports φ-tetrahedral angles and log-spiral paths from Flight.Geometry plus 8-tick scheduling from Flight.Schedule to perform the test. The module contains only definitions that combine these primitives; no new axioms or physical derivations appear.

claimSEG rotor geometry under square-law angles matches a φ-spiral pitch family when its step ratios equal the log-spiral multipliers derived from the φ-tetrahedral angle.

background

The module resides in the Gravity.Candidates section and imports the purely geometric layer from Flight.Geometry, which supplies the φ-tetrahedral angle, log-spiral rotor paths under φ-scaling, and lemmas on step ratios and per-turn multipliers. It further imports the minimal control surface and 8-window neutrality predicates from Flight.Schedule. The module doc-comment states that Recognition Science checks whether this geometry matches φ-spiral pitch families; all content remains math-only and derives from the RS constant φ.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies a concrete candidate check that connects the φ-tetrahedral and 8-tick primitives to the gravity domain, testing the SEG against the φ-spiral families required by the Recognition Science forcing chain (T5–T7). It supports evaluation of spiral-field propulsion models without claiming physical validity.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)