max_coherence_at_balance
plain-language theorem explainer
The theorem establishes that coherence reaches its maximum of 1 exactly at the balance point where the distinction parameter equals 1. Safety analyses in the Recognition framework cite this base case to anchor the claim that any deviation strictly lowers coherence. The proof is a direct term reduction that unfolds the coherence definition and applies the J-cost unit lemma.
Claim. Let $x$ be the distinction parameter with positivity witness $0 < x$. Then coherenceLevel$(1) = 1$, where coherenceLevel$(x)$ is the normalized function $1/(1 + J(x))$ and $J$ denotes the J-cost.
background
The SafetyInterlock module combines the Gap-45 uncomputability barrier with σ-conservation to enforce a safety interlock on high-coherence states. CoherenceLevel is defined in the Core submodule via the J-cost from the Cost module, where Jcost$(x) = (x-1)^2/(2x)$. The upstream Jcost_unit0 lemma states Jcost 1 = 0, which is the algebraic fact that zero cost occurs at unit distinction. This setting rests on the primitive distinction axioms and simplicial ledger structures imported from the Foundation.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of coherenceLevel, rewrites with the Jcost_unit0 lemma, and simplifies the resulting expression to 1.
why it matters
This result is the base case feeding power_ethics_same_axis and weaponization_structurally_impossible. It supplies the core safety claim that power requires ethics by showing maximum coherence only at balance. The declaration closes the σ = 0 optimality step in the Gap-45 interlock and connects to the J-uniqueness fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.