symmetry_breaking_mechanism
plain-language theorem explainer
The theorem asserts that the J-cost vanishes exactly at the ground-state rung zero of the phi-ladder, is strictly positive on all nonzero rungs, and obeys the d'Alembert submultiplicative bound on products. Researchers tracing the Recognition Science derivation of structure from the T0-T8 forcing chain would cite this result to establish the instability of the trivial state. The proof is a compact term-mode packaging of the unit-cost lemma, the positive-cost theorem for nonzero rungs, and the submultiplicativity lemma.
Claim. Let $J$ be the J-cost function and $φ$ the golden ratio. Then $J(φ^0)=0$, $J(φ^n)>0$ for every nonzero integer $n$, and $J(φ^a φ^b) ≤ 2J(φ^a)+2J(φ^b)+2J(φ^a)J(φ^b)$ for all integers $a,b$.
background
The StillnessGenerative module proves from first principles that the unique zero-defect state x=1 is not a passive equilibrium but the generative source of all structure. The J-cost function is defined by $J(x)=(x-1)^2/(2x)$, which measures recognition cost and vanishes at x=1. The phi-ladder refers to the sequence of states $φ^n$ for integer n, where $φ$ is the self-similar fixed point forced by T6.
proof idea
The proof is a term-mode exact expression that directly constructs the three conjuncts of the conjunction. It applies simplification with the Jcost_unit0 lemma to obtain the zero cost at rung zero. It invokes phi_ladder_positive_cost on the hypothesis n ≠ 0 to obtain positivity for nonzero rungs. It applies Jcost_submult to the positive powers phi^a and phi^b to obtain the submultiplicative inequality.
why it matters
This declaration establishes the symmetry breaking mechanism that shows the ground state is forced to generate non-trivial content. It directly fills the description in the module doc-comment that the ground state (rung 0, J=0) is forced off the trivial rung by T4 + T7, with broken-symmetry states connected by the d'Alembert cascade. The result anchors the claim that x=1 is the maximally creative source, as derived from the T0-T8 chain without external assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.