canonicalThreshold

This module builds a structural bridge from the Recognition J-cost to classical room acoustics. The Sabine reverberation time is written $T_{60} = 0.161,V/(A\alpha)$, and the module takes the canonical absorption coefficient near the diffuse-field optimum to be $\alpha \approx J(\varphi)$, with $J$ the unique cost $J(x)=(x+x^{-1})/2-1$.

Here $\varphi$ is the forced self-similar scale from the T6 step of the unified forcing chain (imported via Constants). The threshold $\varphi-3/2$ sits next to sibling facts that the domain cost is nonnegative and vanishes at equilibrium; it supplies a fixed positive scale against which impulse-response certificates are later compared.

No external acoustic axioms are assumed: the only inputs are Mathlib reals, the RS constants, and the Cost module.

Pure definitional abbreviation. The body is the closed-form real expression $\varphi - 3/2$; Lean reduces equalities by rfl. No lemmas are applied and no tactics run.

Gives the acoustics layer a single RS-native cutoff built only from $\varphi$, so later certificates (RoomImpulseCert and the inhabited cert) can quote a dimensionless number rather than an ad-hoc constant. It sits in the same structural package that identifies diffuse-field absorption with $J(\varphi)$, tying classical RT60 bookkeeping to the T5/T6 forcing landmarks (J-uniqueness and $\varphi$ as fixed point). Downstream positivity of the threshold is the immediate companion fact; the broader claim is that room-impulse structure is forced once J-cost and $\varphi$ are fixed, with zero sorry and zero extra axioms in the module.