Documentation

Linglib.Semantics.Degree.Gradability.Dimension

Scalar dimensions #

The axis a gradable predicate — an adjective, or a degree-achievement verb's base adjective — measures along. This is the single carrier the former Features.PerceptualDimension (perceptual channel) and ScalarTelicity.Dimension (scale structure) were both approximating; they are unified here so that RSA noise, adjective comparison-class dependence, and verb telicity are all views of one key.

Physical measurement dimensions (mass, volume-as-litres, …) are a different fibration — an extensive ℚ-measure, not a gradable scale — and stay in Features.Dimension.

Views #

Dimension is one more Core.Order.LicensingPipeline instance, so it shares the endpoint-licensing pipeline with Boundedness, MereoTag, and EpistemicTag.

source
inductive Semantics.Gradability.Dimension :
Type

The scalar dimension a gradable predicate measures along — the union of the perceptual adjective dimensions and the scalar-change verb dimensions.

Instances For
    source
    @[implicit_reducible]
    instance Semantics.Gradability.instDecidableEqDimension :
    DecidableEq Dimension
    Equations
    source
    @[implicit_reducible]
    instance Semantics.Gradability.instReprDimension :
    Repr Dimension
    Equations
    source
    def Semantics.Gradability.instReprDimension.repr :
    Dimension → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Gradability.instFintypeDimension :
      Fintype Dimension
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[implicit_reducible]
      instance Semantics.Gradability.instInhabitedDimension :
      Inhabited Dimension
      Equations
      source
      @[implicit_reducible]
      instance Semantics.Gradability.instBEqDimension :
      BEq Dimension
      Equations
      source
      def Semantics.Gradability.instBEqDimension.beq :
      Dimension → Dimension → Bool
      Equations
      Instances For
        source
        def Semantics.Gradability.Dimension.domain :
        Dimension → Features.PropertyDomain

        The perceptual/cognitive channel — drives RSA noise.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Semantics.Gradability.Dimension.boundedness :
          Dimension → Core.Order.Boundedness

          The dimension's canonical scale shape. Polarity/standard-type are not here — they live on the adjective entry (min/max-standard adjectives select a pole of a closed scale). Reducible so the degree fiber's OrderTop/NoMaxOrder instances synthesise through it.

          Equations
          Instances For

            Degree fiber, grounded through Boundedness (proved once, not per dimension) #

            source
            @[reducible, inline]
            abbrev Core.Order.Boundedness.degreeShape :
            Boundedness → Type

            Degree carrier per boundedness shape: a greatest element exists exactly when the scale HasMax. A computable order-proxy — only the OrderTop/NoMaxOrder mixin matters, not the carrier.

            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Semantics.Gradability.instLinearOrderDegreeShape (b : Core.Order.Boundedness) :
              LinearOrder b.degreeShape
              Equations
              • One or more equations did not get rendered due to their size.
              source
              theorem Core.Order.Boundedness.hasGreatest_degreeShape_iff (b : Boundedness) :
              Degree.HasGreatest b.degreeShape ↔ b.HasMax

              Grounding, proved once at the 4-case level.

              source
              @[reducible, inline]
              abbrev Semantics.Gradability.Dimension.degree (d : Dimension) :
              Type

              Each dimension's degree type — inherited from its boundedness, so the grounding transports rather than re-casing per dimension.

              Equations
              Instances For
                source
                @[implicit_reducible]
                instance Semantics.Gradability.instLinearOrderDegree (d : Dimension) :
                LinearOrder d.degree
                Equations
                source
                theorem Semantics.Gradability.Dimension.hasGreatest_degree_iff (d : Dimension) :
                Degree.HasGreatest d.degree ↔ d.boundedness.HasMax

                The scale's order structure has a greatest element exactly when the dimension's canonical scale HasMax — grounded for all dimensions in one application.

                Derived aspectual views (verb side) #

                source
                def Semantics.Gradability.Dimension.defaultTelicity (d : Dimension) :
                Features.Telicity

                Default telicity of a degree achievement on this dimension: a scale with a greatest degree gives a telic reading ([KL08]).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Semantics.Gradability.Dimension.defaultVendlerClass (d : Dimension) :
                  Features.VendlerClass

                  Default Vendler class: degree achievements are dynamic and durative, so a closed scale gives an accomplishment, an open one an activity.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Semantics.Gradability.Dimension.defaultTelicity_telic_iff_hasGreatest (d : Dimension) :
                    d.defaultTelicity = Features.Telicity.telic ↔ Degree.HasGreatest d.degree

                    The Kennedy–Levin thesis as a theorem. defaultTelicity is exactly the order-theoretic fact: a degree achievement is telic iff its scale's degree type has a greatest element — grounded in the scale's order structure, not stipulated.

                    The endpoint: one more LicensingPipeline instance #

                    source
                    @[implicit_reducible]
                    instance Semantics.Gradability.instLicensingPipelineDimension :
                    Core.Order.LicensingPipeline Dimension
                    Equations