CoherentGravitomagnetism
plain-language theorem explainer
The CoherentGravitomagnetism definition encodes the hypothesis that an internal gravitomagnetic field arises from an external magnetic field through a coherence-dependent coupling in superconductors. Researchers testing Ning Li's 1991 gravitomagnetism claims within Recognition Science would reference this when modeling coherence-gated source terms. The definition computes the internal field via the Li coupling and asserts physical realization as a placeholder proposition.
Claim. The RS-modified gravitomagnetic field hypothesis states that the internal field satisfies $B_g = B_{g0} + (μ_g m / (q μ)) B_0$, where the coupling factor is the Li term derived from the gravitomagnetic permeability $μ_g$, mass $m$, charge $q$, and magnetic permeability $μ$.
background
In the Recognition Science framework, gravitomagnetism is treated as a coherence-gated effect restored in superconducting condensates. The module formalizes Ning Li and D.G. Torr's 1991 claim that the gravitomagnetic field $B_g(z)$ couples to the magnetic field $B_0$ via a factor involving the gravitomagnetic permeability $μ_g$, mass $m$, charge $q$, and magnetic permeability $μ$. This is interpreted as a restoration of underlying coupling normally cancelled by phase decoherence (random walk).
proof idea
This is a definition that constructs the internal field as $B_{g0}$ plus the product of the Li coupling (computed from $μ_g$, $μ$, $m$, $q$) and $B_0$, then asserts the proposition True as a placeholder for full field equation integration. It serves as a one-line wrapper around the coupling computation without invoking additional lemmas beyond the imported constants and projectors.
why it matters
This definition captures the core hypothesis of coherent gravitomagnetism in the RS framework, linking to the broader forcing chain through coherence factors. It fills the role of a coherence-gated source term in gravity candidates, as described in the module documentation. No downstream uses are recorded yet, leaving open questions about integration with the full eight-tick octave and D=3 spatial dimensions in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.