module module moderate

`IndisputableMonolith.Physics.Superfluidity`

The Physics.Superfluidity module defines Bose-Einstein occupation numbers, BEC and lambda temperatures, and vortex quantization in terms of the J-cost function. Quantum fluids researchers would cite these for RS-native expressions of superfluid properties in helium-4. The module is a collection of definitions and positivity lemmas built directly on JcostCore.

claimDefines $n_{BE}(T)$ as the Bose-Einstein occupation number at temperature $T$, $T_{BEC}$ the condensation temperature, $T_λ$ the lambda point for $^4$He, and quantized vortex circulation strength.

background

The module imports JcostCore, which supplies the J-cost function $J(x)=(x+x^{-1})/2-1$ and the Recognition Composition Law. It introduces be_occupation as the occupation number at temperature T, together with bec_temperature, lambda_point, vortex_quantum, and rs_critical_exponent. The local setting applies the phi-ladder and eight-tick octave to quantum statistics and superfluidity.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the superfluidity primitives used for lambda-point and vortex calculations. Connects to T7 eight-tick octave and D=3 from the forcing chain, though the current dependency graph lists no downstream parents.

scope and limits

Does not derive hydrodynamic equations of superfluid flow.
Does not prove existence of the superfluid phase transition.
Does not address fermionic pairing or high-Tc cases.
Does not compute numerical spectra beyond positivity and range checks.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (19)

def be_occupation L23
theorem be_occupation_positive L27
def bec_temperature L37
theorem bec_temperature_positive L41
def lambda_point L51
theorem lambda_point_lt_bec L55
def lambda_point_He4 L73
theorem lambda_He4_in_range L76
def vortex_quantum L84
theorem vortex_quantum_positive L87
theorem vortex_quantized L92
def rs_critical_exponent L99
lemma golden_ratio_gt_one L103
theorem rs_critical_exponent_positive L110
def superfluid_fraction L117
theorem superfluid_fraction_at_zero L121
theorem superfluid_fraction_at_lambda L127
theorem superfluid_fraction_between L133
theorem he3_b_phase_global_minimum L149