Pith. sign in
module module high

IndisputableMonolith.Gravity.CoherenceGain

show as:
view Lean formalization →

The CoherenceGain module defines effective source strength for an ensemble of N particles whose vector contributions depend on phase alignment. Gravity modelers working on acoustic levitation effects cite these results. The module supplies a chain of definitions and lemmas that separate incoherent addition from coherent sqrt(N) amplification.

claimFor an ensemble of $N$ particles each with source magnitude $a$, the incoherent effective source is $a$ while the coherent effective source is $a\sqrt{N}$, yielding coherence gain $\sqrt{N}$.

background

The module sits inside the gravity domain and introduces the Ensemble object together with four source functions: incoherent_effective_source, coherent_effective_source, coherence_gain, and coherence_gain_eq_sqrt_N. These rest on the Recognition Composition Law for vector addition under phase control. A Superconductor subtype and CoherenceGainCert certificate close the module.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions feed directly into the AcousticPhaseLevitation module as its sole import. They supply the coherence mechanism required for the gravity section of the T0-T8 forcing chain and the Recognition Composition Law.

scope and limits

used by (1)

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

declarations in this module (13)