Documentation

Linglib.Core.Scales.Predicate

Core/Scales/Predicate.lean — degree predicates + monotonicity #

@cite{fox-2007} @cite{kennedy-2015} @cite{geurts-nouwen-2007} @cite{nouwen-2010} @cite{partee-1987}

Predicate transformers and degree-relative comparison primitives, parameterized by a measure function μ : W → α:

This file is part of the Phase A decomposition of the legacy Core/Scales/Scale.lean dumping ground (master plan v4).

Per master plan v4, relationalGQ and its lemmas may move to Theories/Semantics/Gradability/Kennedy.lean in Phase B (it's a Kennedy-2015-framework operator, not a domain-general primitive).

source
def Core.Scale.IsUpwardMonotone {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) :
Prop

A family of propositions indexed by scale values is upward monotone (entailments go from smaller to larger values). Kennedy: "tall" — if x is tall, x is tall-or-more. Rouillard: E-TIA with telic VP — if event fits in n days, it fits in m ≥ n days.

Equations
Instances For
    source
    def Core.Scale.IsDownwardMonotone {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) :
    Prop

    A family is downward monotone: entailments go from larger to smaller. Rouillard: E-TIA with atelic VP — if sick during n-day time, sick during m ≤ n day time.

    Equations
    Instances For
      source
      def Core.Scale.IsConstant {α : Type u_1} {W : Type u_2} (P : α → W → Prop) :
      Prop

      A family is constant: every value yields the same proposition. This is information collapse — no value is more informative than another. Occurs when a family is both upward and downward monotone.

      Equations
      Instances For
        source
        theorem Core.Scale.bimonotone_constant {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) (hUp : IsUpwardMonotone P) (hDown : IsDownwardMonotone P) :
        IsConstant P

        If P is both upward and downward monotone, it is constant.

        source
        def Core.Scale.AdmitsOptimum {α : Type u_1} {W : Type u_2} (P : α → W → Prop) :
        Prop

        Informativity licensing: a scale admits a well-defined optimum iff it is NOT constant. When the family is constant (information collapse), no grammatical element operating on that scale is felicitous.

        This is the abstract pattern shared by:

        • Kennedy's Interpretive Economy: degree modifiers require non-trivial scale contribution
        • Rouillard's MIP: TIA numerals require maximally informative values
        Equations
        Instances For
          source
          theorem Core.Scale.bimonotone_no_optimum {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) (hUp : IsUpwardMonotone P) (hDown : IsDownwardMonotone P) :
          ¬AdmitsOptimum P

          Bimonotone families do not admit an optimum: if a family is both upward and downward monotone, it collapses to a constant and no element is maximally informative. This is the abstract core of why open-scale degree modification and atelic-VP E-TIAs are both blocked.

          The cross-world entailment-based IsMaxInf (Fox 2007 / vFFI 2014 / Beck-Rullmann 1999 / Rouillard 2026) is linguistic substrate, not pure order theory — it lives in Theories/Semantics/Entailment/Extremum.lean. The per-world specialization is just IsLeast {y | P y w} x from mathlib (Mathlib.Order.Bounds.Defs); the per-world↔cross-world bridge under monotonicity is mathlib's MonotoneOn.map_isLeast family (Mathlib.Order.Bounds.Image).

          source
          theorem Core.Scale.closed_isLicensed :
          Boundedness.closed.isLicensed = true

          Closed scales predict licensing (Kennedy: "completely full" ✓; Rouillard: telic VP E-TIA ✓).

          source
          theorem Core.Scale.open_notLicensed :
          Boundedness.open_.isLicensed = false

          Open scales predict blocking (Kennedy: "??completely tall"; Rouillard: atelic VP E-TIA ✗).

          Degree properties for comparison relations #

          Five degree properties covering all comparison relations, parameterized by a measure function μ : W → α. These are the building blocks for the named numeral meanings (Semantics.Numerals.atLeastMeaning etc.) and degree question semantics.

          The key divergence: on ℕ, > collapses to ≥ with successor, so both have HasMaxInf. On dense scales, > yields an open set with no max⊨. This is the UDM prediction (@cite{fox-2007} §2).

          source
          def Core.Scale.eqDeg {α : Type u_1} {W : Type u_2} (μ : W → α) :
          α → W → Prop

          Degree property for "exactly d": the measure at w equals d.

          Equations
          Instances For
            source
            def Core.Scale.atLeastDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
            α → W → Prop

            Degree property for "at least d": the measure at w meets or exceeds d.

            Equations
            Instances For
              source
              def Core.Scale.moreThanDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
              α → W → Prop

              Degree property for "more than d": the measure strictly exceeds d.

              Equations
              Instances For
                source
                def Core.Scale.atMostDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                α → W → Prop

                Degree property for "at most d": the measure at w is at most d.

                Equations
                Instances For
                  source
                  def Core.Scale.lessThanDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                  α → W → Prop

                  Degree property for "less than d": the measure is strictly less than d.

                  Equations
                  Instances For
                    source
                    theorem Core.Scale.atLeastDeg_downMono {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                    IsDownwardMonotone (atLeastDeg μ)

                    "At least" is downward monotone: weaker thresholds are easier to satisfy.

                    source
                    theorem Core.Scale.moreThanDeg_downMono {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                    IsDownwardMonotone (moreThanDeg μ)

                    "More than" is downward monotone: weaker thresholds are easier to satisfy.

                    source
                    theorem Core.Scale.moreThan_eq_atLeast_succ {W : Type u_2} (μ : W → ℕ) (m : ℕ) (w : W) :
                    moreThanDeg μ m w ↔ atLeastDeg μ (m + 1) w

                    On ℕ, > collapses to ≥ with successor: "more than m" ↔ "at least m+1". This is the discrete equivalence that density breaks.

                    IsMaxInf-flavored consequences of these degree predicates (atLeast_hasMaxInf, moreThan_noMaxInf, isMaxInf_atLeast_iff_eq, moreThan_nat_hasMaxInf) live in Theories/Semantics/Entailment/Extremum.lean since they depend on the linguistic-substrate IsMaxInf predicate.

                    Existential lowering: exact → "at least" #

                    @cite{partee-1987}'s BE + iota + existential closure, applied to a degree property: from an exact reading exact d w ("the measure equals d"), existentially close to ∃ d' ≥ d, exact d' w. On any reflexive linear order this collapses to atLeastDeg μ d w — witness d' := μ w.

                    This is the formal content of @cite{kennedy-2015}'s "de-Fregean" derivation of the lower-bound numeral reading from the exact reading. The collapse generalizes Numeral type-shifting to arbitrary scales.

                    source
                    def Core.Scale.typeLower {α : Type u_1} [LinearOrder α] {W : Type u_2} (exact : α → W → Prop) (d : α) (w : W) :
                    Prop

                    Existentially lower an exact-style degree property to its lower-bound counterpart: there exists some d' ≥ d such that the exact property holds at d'.

                    Equations
                    Instances For
                      source
                      theorem Core.Scale.typeLower_eqDeg_iff {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) :
                      typeLower (eqDeg μ) d w ↔ atLeastDeg μ d w

                      Type-shift collapse: typeLower (eqDeg μ) = atLeastDeg μ.

                      source
                      @[implicit_reducible]
                      instance Core.Scale.atLeastDeg.decidable {α : Type u_1} [LinearOrder α] {W : Type u_2} [DecidableLE α] (μ : W → α) (d : α) (w : W) :
                      Decidable (atLeastDeg μ d w)
                      Equations
                      source
                      @[implicit_reducible]
                      instance Core.Scale.atMostDeg.decidable {α : Type u_1} [LinearOrder α] {W : Type u_2} [DecidableLE α] (μ : W → α) (d : α) (w : W) :
                      Decidable (atMostDeg μ d w)
                      Equations
                      source
                      @[implicit_reducible]
                      instance Core.Scale.moreThanDeg.decidable {α : Type u_1} [LinearOrder α] {W : Type u_2} [DecidableLT α] (μ : W → α) (d : α) (w : W) :
                      Decidable (moreThanDeg μ d w)
                      Equations
                      source
                      @[implicit_reducible]
                      instance Core.Scale.lessThanDeg.decidable {α : Type u_1} [LinearOrder α] {W : Type u_2} [DecidableLT α] (μ : W → α) (d : α) (w : W) :
                      Decidable (lessThanDeg μ d w)
                      Equations
                      source
                      @[implicit_reducible]
                      instance Core.Scale.eqDeg.decidable {α : Type u_1} {W : Type u_2} [DecidableEq α] (μ : W → α) (d : α) (w : W) :
                      Decidable (eqDeg μ d w)
                      Equations
                      source
                      @[implicit_reducible]
                      instance Core.Scale.typeLower_eqDeg.decidable {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) :
                      Decidable (typeLower (eqDeg μ) d w)
                      Equations

                      A unified GQ denotation parameterized by the comparison relation #

                      @cite{kennedy-2015} proposes a single denotation for modified and unmodified numerals: λP. max{d | #P ≥ d} REL m, where the only parameter distinguishing surface forms is the relation REL ∈ {=, ≥, >, ≤, <}.

                      Specialised to a property of the form atLeastDeg μ, the maximum degree satisfying atLeastDeg μ d w is μ w itself, so Kennedy's denotation collapses to rel (μ w) m — captured here as relationalGQ rel μ m w.

                      The five existing degree properties (eqDeg, atLeastDeg, moreThanDeg, atMostDeg, lessThanDeg) are definitionally relationalGQ instantiated at the corresponding relation. The Class A vs Class B distinction (@cite{geurts-nouwen-2007}, @cite{nouwen-2010}) collapses to a structural property of rel: Class B ↔ IsRefl α rel; Class A ↔ IsIrrefl α rel.

                      Phase B note: this Kennedy-framework operator is scheduled to move to Theories/Semantics/Gradability/Kennedy.lean per master plan v4.

                      source
                      def Core.Scale.relationalGQ {α : Type u_1} {W : Type u_2} (rel : α → α → Prop) (μ : W → α) (d : α) (w : W) :
                      Prop

                      Kennedy's unified GQ denotation: (rel) (μ w) d. The five named degree properties are definitionally equal to instantiations of this.

                      Equations
                      Instances For
                        source
                        theorem Core.Scale.relationalGQ_eq_eqDeg {α : Type u_1} {W : Type u_2} (μ : W → α) :
                        relationalGQ (fun (x1 x2 : α) => x1 = x2) μ = eqDeg μ

                        Specialisation to (· = ·) recovers eqDeg.

                        source
                        theorem Core.Scale.relationalGQ_ge_eq_atLeastDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                        relationalGQ (fun (x1 x2 : α) => x1 ≥ x2) μ = atLeastDeg μ

                        Specialisation to (· ≥ ·) recovers atLeastDeg.

                        source
                        theorem Core.Scale.relationalGQ_gt_eq_moreThanDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                        relationalGQ (fun (x1 x2 : α) => x1 > x2) μ = moreThanDeg μ

                        Specialisation to (· > ·) recovers moreThanDeg.

                        source
                        theorem Core.Scale.relationalGQ_le_eq_atMostDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                        relationalGQ (fun (x1 x2 : α) => x1 ≤ x2) μ = atMostDeg μ

                        Specialisation to (· ≤ ·) recovers atMostDeg.

                        source
                        theorem Core.Scale.relationalGQ_lt_eq_lessThanDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                        relationalGQ (fun (x1 x2 : α) => x1 < x2) μ = lessThanDeg μ

                        Specialisation to (· < ·) recovers lessThanDeg.

                        source
                        theorem Core.Scale.relationalGQ_refl_at_boundary {α : Type u_1} {W : Type u_2} {rel : α → α → Prop} [Std.Refl rel] (μ : W → α) {d : α} {w : W} (h : μ w = d) :
                        relationalGQ rel μ d w

                        Class B inclusion at the boundary (general). If rel is reflexive, Kennedy's GQ holds at any world w whose measure equals the boundary d. Specialised to numerals: "at least 3" / "at most 3" hold at w = 3.

                        source
                        theorem Core.Scale.relationalGQ_irrefl_at_boundary {α : Type u_1} {W : Type u_2} {rel : α → α → Prop} [Std.Irrefl rel] (μ : W → α) {d : α} {w : W} (h : μ w = d) :
                        ¬relationalGQ rel μ d w

                        Class A exclusion at the boundary (general). If rel is irreflexive, Kennedy's GQ fails at any world w whose measure equals the boundary d. Specialised to numerals: "more than 3" / "fewer than 3" fail at w = 3.

                        Why exact bare numerals are not part of a Horn scale #

                        @cite{kennedy-2015} argues that bare numerals (under their exact reading) are not monotone in their numerical argument — neither upward nor downward — so they fail the Horn-scale criterion. The classic Horn scale ⟨1, 2, 3, …⟩ presupposes upward monotonicity; the dual scale ⟨…, 3, 2, 1⟩ presupposes downward monotonicity. Kennedy's unified GQ accommodates both modifier directions without needing a Horn scale at all.

                        The lemmas below state the failure-of-monotonicity and weakness-vs-exact results purely in terms of eqDeg / atLeastDeg / moreThanDeg — independent of any specific scale. The Nat-specific results in Theories/Semantics/Numerals/Basic.lean are immediate corollaries.

                        source
                        theorem Core.Scale.moreThanDeg_disjoint_eqDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) :
                        ¬(eqDeg μ d w ∧ moreThanDeg μ d w)

                        "More than d" and "exactly d" are disjoint (general).

                        source
                        theorem Core.Scale.lessThanDeg_disjoint_eqDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) :
                        ¬(eqDeg μ d w ∧ lessThanDeg μ d w)

                        "Less than d" and "exactly d" are disjoint (general).

                        source
                        theorem Core.Scale.eqDeg_imp_atLeastDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) :
                        eqDeg μ d w → atLeastDeg μ d w

                        Bare exact meaning entails "at least" (general half of Class B inclusion).

                        source
                        theorem Core.Scale.eqDeg_imp_atMostDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) :
                        eqDeg μ d w → atMostDeg μ d w

                        Bare exact meaning entails "at most" (general; symmetric to above).

                        source
                        theorem Core.Scale.atLeastDeg_strictly_weaker_than_eqDeg {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) {d d' : α} (hlt : d < d') {w : W} (hμ : μ w = d') :
                        atLeastDeg μ d w ∧ ¬eqDeg μ d w

                        "At least d" is strictly weaker than "exactly d" (general). Given a witness world w with μ w = d' where d < d', "at least d" holds but "exactly d" fails.

                        source
                        theorem Core.Scale.eqDeg_not_upward_monotone {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) {d d' : α} (hne : d ≠ d') (hle : d ≤ d') {w : W} (hμ : μ w = d) :
                        ¬∀ (x y : α), x ≤ y → eqDeg μ x w → eqDeg μ y w

                        Exact eqDeg is not upward-monotone (general). Given two distinct boundary values d ≤ d' and a witness world with μ w = d, the universal "if exact at d then exact at d'" fails — μ w cannot equal both.

                        source
                        theorem Core.Scale.eqDeg_not_downward_monotone {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) {d d' : α} (hne : d ≠ d') (hle : d' ≤ d) {w : W} (hμ : μ w = d) :
                        ¬∀ (x y : α), y ≤ x → eqDeg μ x w → eqDeg μ y w

                        Exact eqDeg is not downward-monotone (general). Symmetric to above.

                        source
                        theorem Core.Scale.distinct_no_universal_witness {α : Type u_2} (k₁ k₂ : α) (hne : k₁ ≠ k₂) :
                        ¬∃ (x : α), ∀ (k : α), k = k₁ ∨ k = k₂ → x = k

                        Universal closure (the alternative to existential closure) is unsatisfiable when the closure range contains two distinct values: no single x can equal two different ks. This rules out the universal-closure reading of Partee's iota generally.

                        source
                        theorem Core.Scale.atMostDeg_upMono {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) :
                        IsUpwardMonotone (atMostDeg μ)

                        "At most" is upward monotone: larger thresholds are easier to satisfy.

                        IsMaxInf-flavored consequences of atMostDeg (atMost_hasMaxInf, isMaxInf_atMost_iff_eq) live in Theories/Semantics/Entailment/Extremum.lean.