GateFails
plain-language theorem explainer
GateFails marks a gate as failed precisely when it misses the balanced square-budget phase. Researchers deriving bounds on accumulated phase cost from finite failed gates cite this predicate to trigger positivity assumptions before summing costs. The definition is a direct negation of the balanced-phase predicate imported from the Erdos-Straus construction.
Claim. For natural numbers $n$ and $c$, a gate fails if and only if it does not hit the balanced square-budget phase condition.
background
The Phase Failure Cost module develops the second phase-budget theorem: failed finite gates contribute positive unresolved phase cost, and finite sums of those costs accumulate. A gate fails exactly when it misses the balanced phase, the square-budget hitting condition defined in the Erdos-Straus box-phase construction. Upstream cost definitions supply the J-cost of a recognition event and the derived cost of a multiplicative recognizer comparator, both non-negative by construction.
proof idea
The declaration is a one-line definition expressing failure as the negation of the balanced phase predicate.
why it matters
GateFails supplies the failure predicate required by the KThetaFailureFloorHypothesis and the accumulation theorems phase_failure_accumulates and phase_failure_cost_lower_bound. It completes the identification step in the phase-budget argument, allowing the framework to treat failed gates as sources of positive cost that accumulate. In the Recognition Science setting it supports the transition from phase visibility to bounded failure cost under the KTheta floor, consistent with finite-gate accumulation in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.