The level lattice + the minimal-`(m,n)` solver core #

The synthesizer (ParamSynth) composes Param witnesses at a fixed level. The full engine picks the minimal (m,n) a goal needs and synthesizes there. This module supplies the solver's mathematical core:

the MapClass lattice order ≤ (not linear — map2a/map2b are incomparable, both below map3), with Decidable, the partial-order laws, and the meet (⊓) = greatest lower bound (the "least common level");
the level-arithmetic decision tables arrowReq/forallReq: for a desired output level, the exact input levels each Map_k_arrow/Map_k_forall requires (read off ParamArrow.lean/ParamForall.lean). A level-directed resolution or a MetaM solver consults these to dispatch the right combinator — the Lean analogue of Trocq's Elpi param-class constraint solver.

What remains for the full solver is the resolution wiring (variable-level HasParam with these tables driving instance selection), built on this substrate.

The lattice order on `MapClass` #

source

def Transfer.Param.MapClass.le :

MapClass → MapClass → Bool

The structure order: map0 ⊑ map1 ⊑ {map2a, map2b} ⊑ map3 ⊑ map4, with map2a, map2b incomparable. le m' m means m' carries no more structure than m.

Equations

Instances For

source

def Transfer.Param.«term_⊑_» :

Lean.TrailingParserDescr

m' ⊑ m: m' carries no more structure than m (the lattice order).

Equations

Transfer.Param.«term_⊑_» = Lean.ParserDescr.trailingNode `Transfer.Param.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

Instances For

source

theorem Transfer.Param.MapClass.le_refl (m : MapClass) :

(fun (a b : MapClass) => a.le b = true) m m

Reflexivity.

source

theorem Transfer.Param.MapClass.le_trans {a b c : MapClass} (h1 : a.le b = true) (h2 : b.le c = true) :

(fun (a b : MapClass) => a.le b = true) a c

Transitivity.

source

theorem Transfer.Param.MapClass.le_antisymm {a b : MapClass} (h1 : a.le b = true) (h2 : b.le a = true) :

a = b

Antisymmetry.

source

def Transfer.Param.MapClass.meet :

MapClass → MapClass → MapClass

The meet (greatest lower bound): the least common structure level.

Equations

Instances For

source

theorem Transfer.Param.MapClass.meet_le_left (a b : MapClass) :

(fun (a b : MapClass) => a.le b = true) (a.meet b) a

The meet is a lower bound (left).

source

theorem Transfer.Param.MapClass.meet_le_right (a b : MapClass) :

(fun (a b : MapClass) => a.le b = true) (a.meet b) b

The meet is a lower bound (right).

The level-arithmetic decision tables (the solver's dispatch core) #

For a desired output forward level of the arrow/forall combinator, these give the exact (m,n) the two arguments must have — read directly off ParamArrow.lean / ParamForall.lean. A level-directed resolver consults these to choose which Map_k_{arrow,forall} to apply.

source

def Transfer.Param.arrowReq :

MapClass → Option (MapClass × MapClass × MapClass × MapClass)

Required argument levels for Map_k_arrow at a given output forward level. Returns (PA.fwd, PA.bwd, PB.fwd, PB.bwd). From ParamArrow.lean: Map1_arrow ← Param01/Param10, Map2a_arrow ← Param02b/Param2a0, Map2b_arrow ← Param02a/Param2b0, Map3_arrow ← Param03/Param30.

Equations

Instances For

source

def Transfer.Param.forallReq :

MapClass → Option MapClass

Required domain level for Map_k_forall at a given output forward level (the codomain family is at (k, map0)). From ParamForall.lean: Map1_forall needs the domain at Param02a (backward map2a); Map2a_forall needs the domain at Param04 (backward map4 = univalence) — the localized UA boundary.

Equations

Instances For

source

def Transfer.Param.forallUnivalenceFree (k : MapClass) :

Bool

The univalence-free forall fragment: output levels whose domain requirement stays below map4. Exactly {map0, map1} — matching the localization in ParamForall.

Equations