Documentation

Linglib.Features.ScalarDimension

Scalar dimensions #

The axis a gradable predicate — an adjective, or a degree-achievement verb's base adjective — measures along. One key with several views: perceptual channel (domain, drives RSA noise), canonical scale shape (boundedness), and the physical-quantity bridge (dimension?).

Physical measurement dimensions (mass, volume-as-litres, …) are a different fibration — an extensive ℚ-measure, not a gradable scale — and live in Degree.Dimension. The bridge is partial: evaluative and psychological scales (happiness, intelligence) have no physical dimension, which is why they reject ratio measure phrases ("six feet tall" vs "*six feet happy"). speed is simplex here as a lexical scale (fast) but a quotient physically ([bale-schwarz-2026]'s No Division Hypothesis: the grammar does not compose the ratio).

The degree-theoretic apparatus over these dimensions (degree carriers, telicity defaults, endpoint licensing) is in Semantics/Degree/Gradability/Dimension.lean.

source
inductive Features.ScalarDimension :
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
    @[instance_reducible]
    instance Features.instDecidableEqScalarDimension :
    DecidableEq ScalarDimension
    Equations
    source
    @[instance_reducible]
    instance Features.instReprScalarDimension :
    Repr ScalarDimension
    Equations
    source
    def Features.instReprScalarDimension.repr :
    ScalarDimension → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Features.instFintypeScalarDimension :
      Fintype ScalarDimension
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance Features.instInhabitedScalarDimension :
      Inhabited ScalarDimension
      Equations
      source
      @[instance_reducible]
      instance Features.instBEqScalarDimension :
      BEq ScalarDimension
      Equations
      source
      def Features.instBEqScalarDimension.beq :
      ScalarDimension → ScalarDimension → Bool
      Equations
      Instances For
        source
        def Features.ScalarDimension.domain :
        ScalarDimension → PropertyDomain

        The perceptual/cognitive channel — drives RSA noise.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Features.ScalarDimension.boundedness :
          ScalarDimension → Degree.Boundedness

          The dimension's scale shape in its increasing direction ([kennedy-mcnally-2005] (24)–(27), [kennedy-2007] (33), (60)): ??completely wet but completely dry makes wetness lower closed, fully straight but ??fully bent makes straightness upper closed, 100% full/empty makes fullness closed. The negative member of an antonym pair measures on the dual (Boundedness.ofPolarity). Reducible so the degree fiber's OrderTop/NoMaxOrder instances synthesise through it.

          Equations
          Instances For

            Bridges to the physical quantity algebra #

            source
            def Features.ScalarDimension.dimension? :
            ScalarDimension → Option Degree.QuantityDimension

            The physical dimension a scalar dimension is measured in, when one exists: spatial scales are distance, weight is mass, quantity is cardinality, and fast lexicalizes the quotient distance / time as a primitive scale. none for evaluative/psychological/state scales — the scales that reject ratio measure phrases.

            Equations
            Instances For

              Degree fiber and aspectual views ([kennedy-levin-2008]) #

              Absorbed from the retired Degree/Gradability/Dimension.lean: the degree carrier transports from Boundedness.degreeShape, and the Kennedy–Levin telicity defaults are theorems about it.

              source
              @[reducible, inline]
              abbrev Features.ScalarDimension.degree (d : ScalarDimension) :
              Type

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

              Equations
              Instances For
                source
                @[instance_reducible]
                instance Features.instLinearOrderDimensionDegree (d : ScalarDimension) :
                LinearOrder d.degree
                Equations
                source
                theorem Features.ScalarDimension.hasGreatest_degree_iff (d : ScalarDimension) :
                (∃ (m : d.degree), IsTop m) ↔ 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 Features.ScalarDimension.defaultTelicity (d : ScalarDimension) :
                Aspect.Telicity

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Features.ScalarDimension.defaultVendlerClass (d : ScalarDimension) :
                  Aspect.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 Features.ScalarDimension.defaultTelicity_telic_iff_hasGreatest (d : ScalarDimension) :
                    d.defaultTelicity = Aspect.Telicity.telic ↔ ∃ (m : d.degree), IsTop m

                    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.