Greedy Residual Allocation

Abstract

Greedy allocation maximizes one-step gain and positive witnesses force progress.

Theorem 1.1 (A greedy choice maximizes one-step weighted gain).

$$[\mathrm{DecidableEq}\left(Definition\right)]\mathrm{IsGreedyChoice}\left(residuals,weight,separates,pool,chosen,definition\right)\Rightarrow \forall alternative\in pool,\mathrm{WeightedGain}\left(residuals,weight,separates,\mathrm{insert}\left(alternative,chosen\right)\right)\le \mathrm{WeightedGain}\left(residuals,weight,separates,\mathrm{insert}\left(definition,chosen\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ResidualCoverage/GreedyResidualAllocation.greedy_one_step_optimal (✓ std3). ∎

Source. Repository-derived.

Commentary.

IsGreedyChoice supplies pool membership and marginal-gain maximality over the finite weighted residual sums.

The insertion identity converts marginal maximality into the stated one-step WeightedGain bound.

Theorem 1.2 (A positive uncovered witness forces positive greedy progress).

$$[\mathrm{DecidableEq}\left(Definition\right)]\mathrm{IsGreedyChoice}\left(residuals,weight,separates,pool,chosen,definition\right)\wedge (\exists alternative\in pool,\exists residual\in residuals,\mathrm{CoveredBy}\left(separates,chosen,residual\right)=false\wedge \mathrm{separates}\left(alternative,residual\right)=true\wedge zero<\mathrm{weight}\left(residual\right))\Rightarrow zero<\mathrm{MarginalGain}\left(residuals,weight,separates,chosen,definition\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ResidualCoverage/GreedyResidualAllocation.greedy_positive_progress (✓ std3). ∎

Source. Repository-derived.

Commentary.

An available alternative, uncovered residual, true separation, and positive weight form a concrete progress witness.

Greedy maximality transfers its positive marginal gain to the selected definition.

References

• Truth anchor: D5/S3/ConceptDynamics/ResidualCoverage/GreedyResidualAllocation.greedy_one_step_optimal
• Truth anchor: D5/S3/ConceptDynamics/ResidualCoverage/GreedyResidualAllocation.greedy_positive_progress
• Dependency: D5/S3/ConceptDynamics/ResidualCoverage/WeightedResidualCoverage