pydantic lifter to per-lifter Δ=0 (Field constraints + validators)

[TSavo]

Part of #1914 (Python lifter family). Get the pydantic lifter to per-lifter Δ=0. pydantic encodes data contracts (what valid data looks like) — structural + relational constraints on model fields. Ubiquitous in modern Python.

Form census (contract-around OR loudly-refuse)

pydantic form	lifts to	notes
Field(gt=, ge=, lt=, le=)	relational constraints on a field	bounds
Field(min_length=, max_length=)	length constraints
Field(pattern=...)	regex constraint	string shape
conint(gt=,lt=), constr(...), confloat(...)	constrained-type constraints	desugar to field constraints
@field_validator("f")	field validation body	lift the validator predicate
@model_validator(mode="after")	cross-field invariant	holds over the constructed model

Loudly refuse

mode="before" arbitrary coercion, validators with side effects / external calls, Field(default_factory=...) with effects, dynamic model creation (create_model).

Discipline

Per-lifter Δ=0. Field bounds lift to relational facts (same hub as assertGreater / @require(x > 0)). Each constraint/validator form = a discrimination dummy (valid data proves / invalid data refused), RED-first. Real provekit mint+prove receipts.