GateFailureCost
plain-language theorem explainer
GateFailureCost assigns a positive real number to any natural-number pair whose gate fails the balanced square-budget phase. Researchers tracking unresolved phase budgets over finite gate collections cite the structure to isolate the single positivity axiom required by accumulation results. The definition is a direct structure declaration whose only field is the implication from failure to strict positivity.
Claim. For natural numbers $n$ and $c$, a GateFailureCost structure consists of a real number $cost$ together with a proof that failure of the balanced phase condition implies $0 < cost$.
background
The Phase Failure Cost module states the second phase-budget theorem: failed finite gates contribute positive unresolved phase cost, and finite sums of those costs accumulate. GateFails is the predicate that a gate fails precisely when it does not hit the balanced square-budget phase. Upstream results supply the eight-tick phases $kπ/4$ for $k=0..7$, the J-cost of recognition events, and the derived cost of multiplicative recognizers.
proof idea
The structure is introduced directly by declaring the two fields cost : ℝ and positive_of_failure : GateFails n c → 0 < cost. No lemmas or tactics are applied; the declaration itself encodes the required positivity property.
why it matters
The structure supplies the minimal positivity interface used by phase_failure_accumulates_packaged and phase_failure_cost_lower_bound. It thereby completes the finite accumulation step of the phase-budget theorem inside the eight-tick octave framework, where unresolved costs must remain strictly positive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.