aligned_collective_cost_zero
The result shows that J-cost vanishes exactly at unit ratio. Researchers deriving the Global Co-Identity Constraint from the forcing chain cite it as the base case establishing zero collective cost at alignment. The argument is a direct one-line reduction to the unit lemma for the squared-ratio definition of J.
claimWhen the ratio equals one, the J-cost satisfies $J(1)=0$.
background
J-cost is defined by the squared-ratio expression $J(x)=(x-1)^2/(2x)$. The module derives the Global Co-Identity Constraint from the RS forcing chain with no empirical axioms: T5 (J-uniqueness) implies ratio rigidity at J=0, which combines with compact phase from T6+T7 to yield uniform phase at stationarity. The upstream unit lemma states that J-cost at argument 1 is zero by direct simplification of the definition.
proof idea
One-line wrapper that applies the unit lemma Jcost_unit0, which itself follows by simplification from the definition $J(x)=(x-1)^2/(2x)$.
why it matters in Recognition Science
This supplies the zero-cost base case required by gcic_from_forcing_chain and phase_alignment_minimizes_Jtilde. It closes the alignment step in the T5-to-GCIC chain, confirming that collective J-cost reaches its global minimum precisely when phases are uniform. No open scaffolding remains at this node.
scope and limits
- Does not compute J-cost values for ratios other than one.
- Does not address collective costs under non-uniform phase distributions.
- Does not derive the full GCIC statement.
formal statement (Lean)
116theorem aligned_collective_cost_zero : Jcost 1 = 0 := Jcost_unit0
proof body
Term-mode proof.
117
118/-- Individual perturbed costs are positive. -/