london_depth
plain-language theorem explainer
The declaration supplies the explicit formula for London penetration depth as a function of superfluid density, charge, mass, and speed of light. Researchers modeling the Meissner effect inside the Recognition Science treatment of BCS superconductivity cite this expression. It is introduced as a direct one-line definition that matches the classical electromagnetic length scale.
Claim. The London penetration depth is given by $λ = √(m c² / (4 π n_s e²))$, where $n_s$ is the superfluid density, $e$ the electron charge, $m$ the electron mass, and $c$ the speed of light.
background
The module derives Cooper-pair stability from J-cost submultiplicativity, proving that time-reversed pairs reach zero J-cost and that pairing lowers total cost. It also establishes the BCS gap ratio and the structural origin of the Meissner effect from U(1) gauge invariance. The London depth definition appears in this setting to supply the characteristic length that governs magnetic-field expulsion, using only real arithmetic imported from Mathlib and the EightTick periodicity structure.
proof idea
This is a direct definition that expands immediately to the square-root expression. No auxiliary lemmas are invoked beyond the built-in real operations.
why it matters
The definition feeds the downstream theorem london_depth_positive, which asserts positivity under the natural positivity hypotheses on the parameters. It supplies the explicit length scale required for the Meissner-effect discussion in the module, thereby connecting the J-cost framework and eight-tick octave to an observable electromagnetic quantity in superconductivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.