finite_operations_from_budget
plain-language theorem explainer
finite_operations_from_budget establishes that a positive per-operation cost together with a non-negative budget bounds the number of operations by the ratio of budget to cost. Researchers proving finiteness of recognition crossings or events under resource limits cite it in the Foundation layer. The proof is a one-line wrapper that rewrites the scaled inequality using the division lemma for positive multipliers.
Claim. If $0 < c$, $0 ≤ b$, and $n · c ≤ b$ for $n ∈ ℕ$, then $n ≤ b / c$.
background
Pinch Algebra develops mutual divisibility results in unique factorization domains and Fredholm obstructions for paper F5. The cost appearing in the hypotheses is the J-cost of a recognition event, defined either as derivedCost of a multiplicative recognizer's comparator or directly as Cost.Jcost of the event state. The upstream cost definition in ObserverForcing records that every recognition event carries non-negative cost.
proof idea
The proof is a one-line wrapper applying le_div_iff₀ to the hypothesis n * cost ≤ budget under the assumption cost > 0, which directly yields the target division inequality.
why it matters
The result supplies the F5.3.1/3.2 step on finite operations under budget and is invoked verbatim by finite_crossings_from_budget in TopologicalVeto to obtain the corresponding bound on crossings. It anchors the framework's treatment of resource-limited recognition processes within the forcing chain and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.