jcost_isolated_from_zero
plain-language theorem explainer
The declaration shows that J-cost is strictly positive for any positive real different from one. Researchers assembling uniqueness proofs in the Recognition Science pre-Big-Bang setting cite this isolation result when building the existence-uniqueness certificate. The argument is a direct one-line application of the core positivity lemma Jcost_pos_of_ne_one.
Claim. For every real $x > 0$ with $x ≠ 1$, the J-cost satisfies $J(x) > 0$.
background
The module ExistenceUniquenessFromCost supplies the uniqueness half of the pre-Big-Bang complement to earlier existence results. It derives that the set of positive reals with J-cost zero is exactly the singleton {1}, confirming existence is not plural. J-cost is the functional form whose zero set is isolated at unity, as required for the semi-metric interpretation on the log-ratio scale.
proof idea
The theorem is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module, forwarding the hypotheses 0 < x and x ≠ 1 directly to obtain the strict inequality.
why it matters
This supplies the isolated component inside the existenceUniquenessCert definition, which bundles zero_iff_one, unique_member, log_symmetric and isolated to certify the singleton zero set. It fills the isolation claim listed in the module documentation and aligns with J-uniqueness in the forcing chain. The result closes one step toward showing no distinct cost minima exist on the positive reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.