module module moderate

`IndisputableMonolith.Physics.Superfluidity`

The Superfluidity module defines the Bose-Einstein occupation number at temperature T together with related quantities for condensation and vortex behavior inside the Recognition Science framework. It supplies be_occupation, bec_temperature, lambda_point for He4, vortex_quantum, and rs_critical_exponent using the J-cost imported from JcostCore. Researchers deriving quantum fluid predictions from the forcing chain would cite these objects. The module consists entirely of definitions and short positivity statements.

claimBose-Einstein occupation number $n(T)$ at temperature $T$, BEC temperature $T_{BEC}$, lambda point $\lambda$ for $^4$He, quantized vortex circulation, and critical exponent derived from the J-cost function.

background

The module imports JcostCore to access the J-cost function that underlies all Recognition Science derivations. It operates in the setting where physical quantities arise from the phi-ladder and the Recognition Composition Law applied to quantum statistics. The upstream JcostCore module supplies the cost function used to express occupation numbers and critical temperatures.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the base definitions for superfluidity that prepare the ground for later theorems on critical phenomena and phase transitions within the Recognition framework. It connects the J-cost machinery to observable quantities such as the lambda transition and quantized vortices.

scope and limits

Does not derive the full hydrodynamic equations for superfluid flow.
Does not include finite-temperature corrections beyond the listed quantities.
Does not compute numerical spectra for excitations.
Does not address interactions in non-ideal gases.

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