diff --git a/Orb_AutFN.jl b/Orb_AutFN.jl index ddccb3d..9144b48 100644 --- a/Orb_AutFN.jl +++ b/Orb_AutFN.jl @@ -264,6 +264,25 @@ function main() info(PropertyT.logger, "maximum(P) = $(maximum(P))") info(PropertyT.logger, "minimum(P) = $(minimum(P))") + if λ > 0 + sgap = PropertyT.check_distance_to_positive_cone(Δ, λ, P, tol=tol, rational=false, len=2*radius) + if isa(sgap, Interval) + sgap = sgap.lo + end + if sgap > 0 + info(logger, "λ ≥ $(Float64(trunc(sgap,12)))") + Kazhdan_κ = PropertyT.Kazhdan_from_sgap(sgap, length(S)) + Kazhdan_κ = Float64(trunc(Kazhdan_κ, 12)) + info(logger, "κ($name, S) ≥ $Kazhdan_κ: Group HAS property (T)!") + return true + else + sgap = Float64(trunc(sgap, 12)) + info(logger, "λ($name, S) ≥ $sgap: Group may NOT HAVE property (T)!") + return false + end + end + info(logger, "κ($name, S) ≥ $λ < 0: Tells us nothing about property (T)") + return false end main()