Documentation

SE.Transformation.Reference.Orthogonality

Orthogonality Reference #

Canonical known orthogonality rules for transformation operators.

The lookup is intentionally partial. none means that this theory does not currently specify a canonical orthogonality relation for the pair.

The lookup itself enforces symmetry, so reversing the two operators cannot produce a different orthogonality relation.

Composition and orthogonality remain independent axes: a pair may have both a composition relation and an orthogonality relation without contradiction.

source
def SE.Transformation.orthogonality? :
OperatorCode → OperatorCode → Option OrthogonalityRelation

Return the canonical orthogonality relation for an operator pair when one is specified by this theory.

Equations
Instances For
    source
    @[simp]
    theorem SE.Transformation.authorizeAndAttest :
    orthogonality? OperatorCode.AZ OperatorCode.AT = some OrthogonalityRelation.orthogonal

    Authorization and attestation have canonically orthogonal effect domains.

    source
    @[simp]
    theorem SE.Transformation.projectAndCollapse :
    orthogonality? OperatorCode.PR OperatorCode.CL = some OrthogonalityRelation.overlapping

    Projection and collapse have canonically overlapping effect domains.

    source
    @[simp]
    theorem SE.Transformation.splitAndMerge :
    orthogonality? OperatorCode.SP OperatorCode.MG = some OrthogonalityRelation.overlapping

    Split and merge have canonically overlapping effect domains.

    source
    theorem SE.Transformation.orthogonality_symm (left right : OperatorCode) :
    orthogonality? left right = orthogonality? right left

    The canonical orthogonality lookup is symmetric.

    source
    theorem SE.Transformation.orthogonality_defined_iff (left right : OperatorCode) :
    (∃ (relation : OrthogonalityRelation), orthogonality? left right = some relation) ↔ left = OperatorCode.AZ ∧ right = OperatorCode.AT ∨ left = OperatorCode.AT ∧ right = OperatorCode.AZ ∨ left = OperatorCode.PR ∧ right = OperatorCode.CL ∨ left = OperatorCode.CL ∧ right = OperatorCode.PR ∨ left = OperatorCode.SP ∧ right = OperatorCode.MG ∨ left = OperatorCode.MG ∧ right = OperatorCode.SP

    An orthogonality relation is specified exactly for the three canonical unordered pairs currently declared by this theory.