Nested Restriction

A NestedRestriction S D is a monotone family of predicates on D indexed by an ordered scale S, where going up the scale gives a superset. The top of the scale contains everything.

This structure unifies two independently-developed formalizations:

1. Domain restriction (@cite{ritchie-schiller-2024}): spatial regions induce nested candidate domain restrictors for quantifiers. S = SpatialScale, D = Entity.

2. Comparison class inference (@cite{tessler-goodman-2022}): comparison classes (subordinate vs. superordinate) induce nested reference populations for adjective thresholds. S = ComparisonClass, D = Person.

The downstream applications differ — quantifier domain filtering vs. threshold derivation from population distribution — but the nesting structure is identical: a monotone map from an ordered scale to predicates on a domain.

structure Core.NestedRestriction (S : Type u_1) (D : Type u_2) [Preorder S] [OrderTop S] : Type (max u_1 u_2)

A monotone family of predicates indexed by an ordered scale.

Each scale level s : S induces a predicate region s : D → Bool. The family is monotone: if s₁ ≤ s₂, then region s₁ is contained in region s₂. The top element ⊤ contains everything.

Field names match DDRP exactly so that abbrev DDRP := NestedRestriction is a drop-in replacement with zero downstream breakage.

• region : S → D → Bool

  Each scale level induces a predicate on the domain.

• monotone {s₁ s₂ : S} : s₁ ≤ s₂ → ∀ (d : D), self.region s₁ d = true → self.region s₂ d = true

  Nesting: smaller scale ⊆ larger scale.

• top_total (d : D) : self.region ⊤ d = true

  The top scale contains everything.

theorem Core.NestedRestriction.subset_of_le {S : Type u_1} {D : Type u_2} [Preorder S] [OrderTop S] (nr : NestedRestriction S D) {s₁ s₂ : S} (h : s₁ ≤ s₂) (d : D) : nr.region s₁ d = true → nr.region s₂ d = true

Unwraps monotone: if s₁ ≤ s₂ then the s₁-region is a subset of the s₂-region. Trivial but documents the pattern for downstream use.

theorem Core.NestedRestriction.forall_nesting {S : Type u_1} {D : Type u_2} [Preorder S] [OrderTop S] (nr : NestedRestriction S D) {s₁ s₂ : S} (h : s₁ ≤ s₂) {P : D → Prop} (hP : ∀ (d : D), nr.region s₂ d = true → P d) (d : D) : nr.region s₁ d = true → P d

If a property holds for all elements of a larger region, it holds for all elements of any smaller region.

This is the abstract pattern behind DDRP.every_nesting: ⟦every⟧ under a larger scale entails ⟦every⟧ under any smaller scale (restrictor ↓MON).

theorem Core.NestedRestriction.exists_nesting {S : Type u_1} {D : Type u_2} [Preorder S] [OrderTop S] (nr : NestedRestriction S D) {s₁ s₂ : S} (h : s₁ ≤ s₂) {P : D → Prop} (hP : ∃ (d : D), nr.region s₁ d = true ∧ P d) : ∃ (d : D), nr.region s₂ d = true ∧ P d

If some element of a smaller region satisfies a property, some element of any larger region does too.

This is the abstract pattern behind DDRP.some_nesting: ⟦some⟧ under a smaller scale entails ⟦some⟧ under any larger scale (restrictor ↑MON).

inductive Core.TwoLevel : Type

A two-level scale for comparison class restrictions: restricted ≤ full.

Used by comparisonClassRestriction to build a generic nested restriction from any relevance predicate.

• restricted : TwoLevel
• full : TwoLevel

instance Core.instDecidableEqTwoLevel : DecidableEq TwoLevel

Equations

• Core.instDecidableEqTwoLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.instBEqTwoLevel.beq : TwoLevel → TwoLevel → Bool

Equations

• Core.instBEqTwoLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.instBEqTwoLevel : BEq TwoLevel

Equations

• Core.instBEqTwoLevel = { beq := Core.instBEqTwoLevel.beq }

def Core.instReprTwoLevel.repr : TwoLevel → ℕ → Std.Format

Equations

• Core.instReprTwoLevel.repr Core.TwoLevel.restricted prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.TwoLevel.restricted")).group prec✝
• Core.instReprTwoLevel.repr Core.TwoLevel.full prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.TwoLevel.full")).group prec✝

instance Core.instReprTwoLevel : Repr TwoLevel

Equations

• Core.instReprTwoLevel = { reprPrec := Core.instReprTwoLevel.repr }

instance Core.instFintypeTwoLevel : Fintype TwoLevel

Equations

• Core.instFintypeTwoLevel = { elems := {Core.TwoLevel.restricted, Core.TwoLevel.full}, complete := Core.instFintypeTwoLevel._proof_1 }

instance Core.instLinearOrderTwoLevel : LinearOrder TwoLevel

Equations

• Core.instLinearOrderTwoLevel = LinearOrder.lift' Core.TwoLevel.toFin✝ Core.TwoLevel.toFin_injective✝

instance Core.instOrderTopTwoLevel : OrderTop TwoLevel

Equations

• Core.instOrderTopTwoLevel = { top := Core.TwoLevel.full, le_top := Core.instOrderTopTwoLevel._proof_1 }

def Core.comparisonClassRestriction {D : Type u_1} (isRelevant : D → Bool) : NestedRestriction TwoLevel D

Generic constructor: given any relevance predicate isRelevant : D → Bool, build a 2-level NestedRestriction where the bottom level filters by isRelevant and the top level is universal.

This captures the comparison class pattern: the subordinate class restricts to a subpopulation (e.g., basketball players), while the superordinate class includes everyone.

Equations

• One or more equations did not get rendered due to their size.