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 bridges (physical?, quotient?).

Physical measurement dimensions (mass, volume-as-litres, …) are a different fibration — an extensive ℚ-measure, not a gradable scale — and live in Features.Dimension. The bridges are 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 ([BS26a]'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
    @[implicit_reducible]
    instance Features.instDecidableEqScalarDimension :
    DecidableEq 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
      @[implicit_reducible]
      instance Features.instReprScalarDimension :
      Repr ScalarDimension
      Equations
      source
      @[implicit_reducible]
      instance Features.instFintypeScalarDimension :
      Fintype ScalarDimension
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[implicit_reducible]
      instance Features.instInhabitedScalarDimension :
      Inhabited ScalarDimension
      Equations
      source
      def Features.instBEqScalarDimension.beq :
      ScalarDimension → ScalarDimension → Bool
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Features.instBEqScalarDimension :
        BEq ScalarDimension
        Equations
        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 → 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

            Bridges to the physical quantity algebra #

            source
            def Features.ScalarDimension.physical? :
            ScalarDimension → Option Dimension.Dimension

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

            Equations
            Instances For
              source
              def Features.ScalarDimension.quotient? :
              ScalarDimension → Option Dimension.QuotientDimension

              The quotient physical dimension, for lexical scales that are physically ratios: fast lexicalizes speed = distance / time as a primitive scale.

              Equations
              Instances For
                source
                theorem Features.ScalarDimension.physical_quotient_disjoint (d : ScalarDimension) :
                d.physical? = none ∨ d.quotient? = none

                No scalar dimension is both simplex-physical and quotient-physical.

                Degree fiber and aspectual views ([KL08]) #

                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
                  @[implicit_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) :
                  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 Features.ScalarDimension.defaultVendlerClass (d : ScalarDimension) :
                    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 = 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.

                      The endpoint: one more LicensingPipeline instance #

                      source
                      @[implicit_reducible]
                      instance Features.instLicensingPipelineScalarDimension :
                      Core.Order.LicensingPipeline ScalarDimension
                      Equations