16.4. Operations the object index changes🔗

Two operations look ordinary until the object is in the type, and then say something they could not say before.

Definition16.4.1

Group: The object of an individual quantity (the foundations chapter's mode) ranges over an arbitrary type. The gate needs nothing from it; the designation needs Designated , whose injectivity field is what distinguishes a designation from a formality. (7)

Group member previews

Preview

Definition 16.3.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

The kind-licensed scalar action. A scalar quantity of an object scaling a vector quantity of the same object, licensed by the same product law the homogeneous product takes. p = m·v and F = m·a have this shape, and the homogeneous product cannot express them: it wants one carrier for both operands, and here one side is a number and the other a numerical vector.

Lean code for Definition16.4.1●1 definition

defdefined in PropertyKindCalculus/IndividualQuantity.lean

complete

def PropertyKindCalculus.IndividualQuantity.smulK.{u} {O : Type u} {o : O}
  {R V : Type} [SMul R V] [PropertyKindCalculus.ScalarCarrier R]
  {k₁ k₂ k : PropertyKindCalculus.KindOfProperty}
  (_h : PropertyKindCalculus.ProductKind k₁ k₂ k)
  (a : PropertyKindCalculus.IndividualQuantity o k₁ R)
  (b : PropertyKindCalculus.IndividualQuantity o k₂ V) :
  PropertyKindCalculus.IndividualQuantity o k V

def PropertyKindCalculus.IndividualQuantity.smulK.{u}
  {O : Type u} {o : O} {R V : Type}
  [SMul R V]
  [PropertyKindCalculus.ScalarCarrier R]
  {k₁ k₂ k :
    PropertyKindCalculus.KindOfProperty}
  (_h :
    PropertyKindCalculus.ProductKind k₁ k₂
      k)
  (a :
    PropertyKindCalculus.IndividualQuantity
      o k₁ R)
  (b :
    PropertyKindCalculus.IndividualQuantity
      o k₂ V) :
  PropertyKindCalculus.IndividualQuantity
    o k V

**Same-object, kind-licensed scalar action.** A scalar `k₁`-quantity of object `o` scaling
a `k₂`-quantity of the *same* object at a vector carrier `V` (`QuantityVector`, ISO 80000-2
§18). This is `p = m · v` and `F = m · a`: the operation vector mechanics is built from, which
the homogeneous `mul` cannot express because its two operands share one carrier.

The object gate is the point here as much as the kind law — the mass of one particle scaling
another particle's acceleration is exactly the substitution an object-blind model cannot
refuse.

Proof for Definition 16.4.1

uses 0

The carrier's own SMul on the magnitudes, with ScalarCarrier demanded of the acting side — a vector carrier is deliberately not a ScalarCarrier, so this cannot be misread as a componentwise product of two vectors. The object gate is as much the point as the kind law: one particle's mass scaling another's acceleration is exactly the substitution an object-blind model has no way to refuse, and it is the shape of an ordinary copy-paste error. Without this operation an application has to mint an unlicensed action and attest it at the interface tier, which is where the kind stops being checked.

Definition16.4.2

Group member previews

Preview

Definition 16.3.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

The transpose of a joint quantity. The same magnitude, read as a quantity of the reversed pair — the equal-and-opposite reading, and the only re-indexing of an individual quantity the library offers. Its value is that a law becomes a type: a "reverse" that negates a magnitude and forgets to exchange the endpoints has the untransposed type and does not elaborate where a reversed quantity is expected.

Lean code for Definition16.4.2●1 definition

defdefined in PropertyKindCalculus/Composite.lean

complete

def PropertyKindCalculus.IndividualQuantity.transpose.{u, v} {O₁ : Type u}
  {O₂ : Type v} {a : O₁} {b : O₂}
  {k : PropertyKindCalculus.KindOfProperty} {R : Type}
  (q : PropertyKindCalculus.IndividualQuantity (a, b) k R) :
  PropertyKindCalculus.IndividualQuantity (b, a) k R

def PropertyKindCalculus.IndividualQuantity.transpose.{u,
    v}
  {O₁ : Type u} {O₂ : Type v} {a : O₁}
  {b : O₂}
  {k :
    PropertyKindCalculus.KindOfProperty}
  {R : Type}
  (q :
    PropertyKindCalculus.IndividualQuantity
      (a, b) k R) :
  PropertyKindCalculus.IndividualQuantity
    (b, a) k R

**The transpose of a joint quantity** — the same magnitude, read as a quantity of the
reversed pair.

This is the equal-and-opposite reading, and it is the only re-indexing of an individual
quantity this library offers. There is deliberately no general `reindex`: moving a magnitude
from one object to another is exactly what the object index exists to prevent, and an
operation that did it on request would return the layer to a naming convention. The transpose
is safe because it is not a move — the pair `(a, b)` and the pair `(b, a)` are the same
coupling read from its two ends, and which end is *source* is the whole content of a law like
Newton's third.

Its value is that the law becomes a type. A "reverse" that negates a magnitude and forgets to
exchange the endpoints has the untransposed type, so it does not elaborate where a reversed
force is expected.

Proof for Definition 16.4.2

uses 0

The magnitude, at the swapped index; the involution is rfl. There is deliberately no general re-indexing: moving a magnitude from one object to another is what the object index exists to prevent, and an operation that did it on request would return the layer to a naming convention. The transpose is safe because it is not a move — (a, b) and (b, a) are one coupling read from its two ends, and which end is the source is the content of a law like Newton's third.