Variational.lean

View source on GitHub

MinimizesOn / MaximizesOn

Optimality predicates. An element minimizes a cost function over a feasible set if it is feasible and no feasible element has lower cost. MaximizesOn is the dual for scores.

ConsolidateOptimality

The consolidation optimization problem. The kernel update maps (policy, ranked) to a new policy. The key hypothesis is self_feasible: the current policy is always an admissible candidate. This is discrete rate-distortion — any optimal output costs no more than the incumbent.

ConsolidateOptimality.optimal_implies_lossy

An optimal consolidation kernel is lossy: output information never exceeds input information. The output minimizes info over the feasible set, and the incumbent policy is feasible, so info(p') ≤ info(p).

theorem ConsolidateOptimality.optimal_implies_lossy
    {M : Type → Type} [Monad M] [Support M]
    {policy ranked : Type}
    (P : ConsolidateOptimality M policy ranked) :
    ∀ p r p', Support.support (P.update p r) p' →
      P.info.measure p' ≤ P.info.measure p

FilterOptimality

The filter optimization problem. Two hypotheses do the real work: outputs_optimal (the kernel picks the smallest feasible output) and strict_witness (for every input, a feasible output strictly smaller exists). Minimality plus witness gives the strict reduction contract.

FilterOptimality.optimal_implies_strictly_smaller

An optimal filter kernel is strictly reducing. Chain: minimality gives sizeOf(b) ≤ sizeOf(c) for any feasible c. The strict witness gives a feasible c with sizeOf(c) < sizeOf(a). Therefore sizeOf(b) < sizeOf(a).

AttendFeasibility

Attend's contract comes from feasibility constraints, not optimization. The proof never uses maximality — both boundedness and diversity are the feasibility constraint projected back out. The file is honest about this: a genuine variational derivation of diversity would require cardinality arguments not present in the possibilistic formalization.

Connections

• Contracts.lean — the contract structures (FilterContract, ConsolidateContract, AttendContract) that these constructors build
• Handshake.lean — imported; the contracts plug into existing handshake and coupling machinery