Strict college preferences and applicant optimality

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Max
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Sigma
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_Basic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_DeferredAcceptance
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62_GS62CollegeAdmissions_MainTheorems
import Definitions.Def_AMLGS62Rest_AppliedModelingLib_Markets_Matching_ManyToOne

namespace GS62CollegeAdmissions
open AppliedModelingLib.Matching

/--
Strict applicant rankings, with no college tied with being unassigned.  Values
below zero give an arbitrary injective numerical extension of an applicant's
unlisted colleges; source-facing procedures filter them out before ranking.
-/
def ApplicantsStrictCollegeProfile {Applicants Colleges : Type*}
    (val_applicant : Applicants → Colleges → ℝ) : Prop :=
  (∀ a c c', val_applicant a c = val_applicant a c' → c = c') ∧
    ∀ a c, val_applicant a c ≠ 0

/--
Strict college rankings, with no applicant tied with an empty seat.  Values
below zero similarly extend the unlisted applicants only for a total numeric
representation; they never become mutually eligible applications.
-/
def CollegesStrictApplicantProfile {Applicants Colleges : Type*}
    (val_college : Colleges → Applicants → ℝ) : Prop :=
  (∀ c a a', val_college c a = val_college c a' → a = a') ∧
    ∀ c a, val_college c a ≠ 0

/--
The paper's finite strict college-admissions domain.  Positive values encode
names appearing on an acceptable list and negative values encode omitted
names; `0` is the outside option.
-/
def gs_strict_college_admissions_domain {Applicants Colleges : Type*}
    (val_applicant : Applicants → Colleges → ℝ)
    (val_college : Colleges → Applicants → ℝ) : Prop :=
  ApplicantsStrictCollegeProfile val_applicant ∧
    CollegesStrictApplicantProfile val_college

/--
Completed standard stability convention used by the reusable many-to-one API:
quotas and individual rationality hold, and there is no applicant-college pair
that prefers one another to the current assignment (including through an empty
seat).  This deliberately extends the page-10 displayed replacement-pair
condition, which is formalized separately in `SourceStability.lean`.
-/
def gs_stable_college_assignment {Applicants Colleges : Type*}
    (quota : Colleges → ℕ)
    (val_applicant : Applicants → Colleges → ℝ)
    (val_college : Colleges → Applicants → ℝ)
    (mu : ManyToOneAssignment Applicants Colleges) : Prop :=
  ManyToOne.IsStable val_applicant val_college quota mu

/-- Applicant optimality among all stable assignments in the same quota market. -/
def gs_applicant_optimal_college_assignment {Applicants Colleges : Type*}
    (quota : Colleges → ℕ)
    (val_applicant : Applicants → Colleges → ℝ)
    (val_college : Colleges → Applicants → ℝ)
    (mu : ManyToOneAssignment Applicants Colleges) : Prop :=
  gs_stable_college_assignment quota val_applicant val_college mu ∧
    ∀ nu, gs_stable_college_assignment quota val_applicant val_college nu →
      ∀ a, ManyToOne.valApplicant val_applicant a (nu.app_match a) ≤
        ManyToOne.valApplicant val_applicant a (mu.app_match a)

end GS62CollegeAdmissions