A Property Kind Calculus for Measurement Metrology

21.5. Capturing a Remark's mathematics: the surface element of an area (item 3-3)🔗

Each ISO 80000 item carries a Remarks field, and those remarks often hold the quantity's defining mathematics. Item 3-3 (area) is the example: its remark gives the surface element of a surface in terms of the Gaussian coordinates u, v and the determinant g of the metric tensor (ISO 80000-2). Rather than transcribe the licensed text or reduce it to a dimensional annotation, this work formalizes the relation — as real differential-geometric objects with proved properties — so the mathematics behind the kind is itself checked.

Definition21.5.1
Group: The metric tensor is realized as the Gram matrix of the two tangent vectors ∂r/∂u , ∂r/∂v (its entries are the classical E , F , G ); its determinant is g ; and the surface element is dA = √g . The standard writes the element with g ; the area-consistent Riemannian element is its square root , and the formalization makes that convention explicit by proving that a flat patch then recovers its Euclidean area. The kind whose magnitudes these areas are is the catalogued quantity -kind area, dimension L² . (4)
Group member previews
Preview
Definition 21.5.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

The first fundamental form (the metric tensor of ISO 80000-2) at a point is the 2 × 2 Gram matrix ⟪tᵢ, tⱼ⟫ of the surface's two tangent vectors. It is symmetric and positive-semidefinite, so its determinant g is non-negative.

Lean code for Definition21.5.1●1 definition
  • defdefined in PropertyKindCalculus/Iso80000/Part3/AreaElement.lean
    complete
    def PropertyKindCalculus.Iso80000.Part3.AreaElement.firstFundamentalForm.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (t : Fin 2 → E) : Matrix (Fin 2) (Fin 2) ℝ
    def PropertyKindCalculus.Iso80000.Part3.AreaElement.firstFundamentalForm.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (t : Fin 2 → E) :
  Matrix (Fin 2) (Fin 2) ℝ
    The **first fundamental form** (the *metric tensor* of ISO 80000-2) of a surface
at a point, given the two tangent vectors `t 0 = ∂r/∂u`, `t 1 = ∂r/∂v`: the `2 × 2`
Gram matrix `⟪tᵢ, tⱼ⟫`. Its entries are the classical coefficients `E = ⟪t₀,t₀⟫`,
`F = ⟪t₀,t₁⟫`, `G = ⟪t₁,t₁⟫`.
Proof for Definition 21.5.1
uses 0

Realized as firstFundamentalForm t := Matrix.gram ℝ t over Mathlib's Gram-matrix library; symmetry is isHermitian_gram and metricDet_nonneg is the determinant of a positive-semidefinite matrix.

Definition21.5.2
Group: The metric tensor is realized as the Gram matrix of the two tangent vectors ∂r/∂u , ∂r/∂v (its entries are the classical E , F , G ); its determinant is g ; and the surface element is dA = √g . The standard writes the element with g ; the area-consistent Riemannian element is its square root , and the formalization makes that convention explicit by proving that a flat patch then recovers its Euclidean area. The kind whose magnitudes these areas are is the catalogued quantity -kind area, dimension L² . (4)
Group member previews
Preview
Definition 21.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

The surface element dA = √g is the area-element density at a point, and the area of a surface patch is its integral over the parameter region (A = ∬ √g du dv). Uses the dimension map for the L² reading of the resulting kind.

Lean code for Definition21.5.2●1 definition
  • defdefined in PropertyKindCalculus/Iso80000/Part3/AreaElement.lean
    complete
    def PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (t : Fin 2 → E) : ℝ
    def PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (t : Fin 2 → E) : ℝ
    The **surface element** `dA = √g`: the area-element density at the point. The
square root is what makes a flat patch recover its Euclidean area
(`areaElement_eq_abs_det`).
Proof for Definition 21.5.2
uses 0

areaElement t := Real.sqrt (metricDet t) and surfaceArea t s := ∫ x in s, areaElement (t x). surfaceArea_const shows a uniformly-parametrized patch has area element × (area of the parameter region).

Theorem21.5.3
Group: The metric tensor is realized as the Gram matrix of the two tangent vectors ∂r/∂u , ∂r/∂v (its entries are the classical E , F , G ); its determinant is g ; and the surface element is dA = √g . The standard writes the element with g ; the area-consistent Riemannian element is its square root , and the formalization makes that convention explicit by proving that a flat patch then recovers its Euclidean area. The kind whose magnitudes these areas are is the catalogued quantity -kind area, dimension L² . (4)
Group member previews
Preview
Definition 21.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
EffortsmallTagsproved

The element squares back to the determinant: (dA)² = g. The √ in dA = √g is faithful — the element is exactly the square root of the determinant of the metric tensor.

Lean code for Theorem21.5.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part3/AreaElement.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement_sq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (t : Fin 2 → E) :
  PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement t ^ 2 =
    PropertyKindCalculus.Iso80000.Part3.AreaElement.metricDet t
    theorem PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement_sq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (t : Fin 2 → E) :
  PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement
        t ^
      2 =
    PropertyKindCalculus.Iso80000.Part3.AreaElement.metricDet
      t
    `(dA)² = g` — the surface element squares back to the determinant of the metric
tensor: the `√` in `dA = √g` is faithful.
Proof for Theorem 21.5.3
uses 0

areaElement_sq : areaElement t ^ 2 = metricDet t, from Real.sq_sqrt and the non-negativity of g.

Theorem21.5.4
Group: The metric tensor is realized as the Gram matrix of the two tangent vectors ∂r/∂u , ∂r/∂v (its entries are the classical E , F , G ); its determinant is g ; and the surface element is dA = √g . The standard writes the element with g ; the area-consistent Riemannian element is its square root , and the formalization makes that convention explicit by proving that a flat patch then recovers its Euclidean area. The kind whose magnitudes these areas are is the catalogued quantity -kind area, dimension L² . (4)
Group member previews
Preview
Definition 21.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
EffortmediumTagsproved

A flat patch recovers its Euclidean area. For a surface lying in the plane the element equals |det A|, the change-of-variables area density of the parametrization — so the √g reading computes the actual area. This is the correctness anchor that pins the convention the prose remark leaves implicit.

Lean code for Theorem21.5.4●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part3/AreaElement.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement_eq_abs_det
  (t : Fin 2 → EuclideanSpace ℝ (Fin 2)) :
  PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement t =
    |(Matrix.of fun i j => (t j).ofLp i).det|
    theorem PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement_eq_abs_det
  (t : Fin 2 → EuclideanSpace ℝ (Fin 2)) :
  PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement
      t =
    |(Matrix.of fun i j =>
          (t j).ofLp i).det|
    **The element is the change-of-variables area density.** For a flat patch the
surface element equals `|det A|` — so `dA = |det A| du dv` integrates to the *actual*
area, confirming the `√g` reading against the Euclidean area it must reproduce.
Proof for Theorem 21.5.4
uses 0

areaElement_eq_abs_det : areaElement t = |(Matrix.of fun i j => t j i).det|, via gram_eq_conjTranspose_mul (so g = (det A)²) and Real.sqrt_sq_eq_abs.

Theorem21.5.5
Group: The metric tensor is realized as the Gram matrix of the two tangent vectors ∂r/∂u , ∂r/∂v (its entries are the classical E , F , G ); its determinant is g ; and the surface element is dA = √g . The standard writes the element with g ; the area-consistent Riemannian element is its square root , and the formalization makes that convention explicit by proving that a flat patch then recovers its Euclidean area. The kind whose magnitudes these areas are is the catalogued quantity -kind area, dimension L² . (4)
Group member previews
Preview
Definition 21.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
EffortsmallTagsproved

Regularity. The element is strictly positive exactly when the two tangent vectors are linearly independent — a non-degenerate (regular) point. A vanishing element marks a degenerate parametrization.

Lean code for Theorem21.5.5●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part3/AreaElement.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement_pos_iff.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (t : Fin 2 → E) :
  0 < PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement t ↔
    LinearIndependent ℝ t
    theorem PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement_pos_iff.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (t : Fin 2 → E) :
  0 <
      PropertyKindCalculus.Iso80000.Part3.AreaElement.areaElement
        t ↔
    LinearIndependent ℝ t
    **Regularity.** The surface element is strictly positive exactly when the two
tangent vectors are linearly independent — i.e. at a non-degenerate (regular) point of
the parametrization. A vanishing element marks a degenerate parametrization.
Proof for Theorem 21.5.5
uses 0

areaElement_pos_iff : 0 < areaElement t ↔ LinearIndependent ℝ t, from Real.sqrt_pos and det_gram_ne_zero_iff_linearIndependent.