Morphism Verification Protocol

assetactive

Morphism Verification Protocol

Source: morphism-verification-protocol.md (ingested 2026-03-28)

type: reference authority: canonical audience: [agents, contributors, researchers] last-verified: 2026-03-21 scope: mathematical-foundations

Morphism Verification Protocol

Version: 1.0 Authority: Mathematical foundations for governance framework Parent: Paper 1 (papers/agentic-mathematics/main.tex)

Start Here

Use this document when you are making or reviewing a mathematical morphism claim. For current repo enforcement behavior, see:

Decision Rule

Treat this document as a formal reference and proof target. Do not cite it as proof that the product runtime or CI automatically verifies every algebraic property described here unless a concrete implementation and evidence path exists for that claim.

Preamble

This document defines verification protocols for morphisms across algebraic structures. These checks describe structure-preserving properties that can guide future proofs, implementations, and mathematical review.

Scope: Group homomorphisms, ring homomorphisms, module homomorphisms, functors, natural transformations.

1. General Morphism Axioms

Every morphism φ: A → B between algebraic structures must satisfy:

Axiom M-1: Well-Definedness

∀a ∈ A: φ(a) ∈ B

Check: Verify domain and codomain membership for all inputs.

Axiom M-2: Functionality

a₁ = a₂ ⇒ φ(a₁) = φ(a₂)

Check: Equal inputs produce equal outputs (single-valued).

Axiom M-3: Structure Preservation

φ(op_A(a₁, a₂)) = op_B(φ(a₁), φ(a₂))

Check: Operation in source maps to operation in target.

2. Group Homomorphisms

Definition: φ: (G, ∗) → (H, ·) preserves group structure.

Required Checks

| ID | Property | Formula | Verification | |----|----------|---------|--------------| | G-1 | Operation Preservation | φ(a ∗ b) = φ(a) · φ(b) | Test on sample pairs | | G-2 | Identity Preservation | φ(e_G) = e_H | Explicit check | | G-3 | Inverse Preservation | φ(a⁻¹) = φ(a)⁻¹ | Test on sample elements |

Derived Properties (Auto-verify if G-1 holds)

  • Kernel: ker(φ) = {g ∈ G : φ(g) = e_H} is a normal subgroup
  • Image: im(φ) = {h ∈ H : ∃g ∈ G, φ(g) = h} is a subgroup
  • First Isomorphism Theorem: G/ker(φ) ≅ im(φ)

Test Protocol

def verify_group_homomorphism(phi, G, H):
    """Verify φ: G → H is a group homomorphism."""
    for g1, g2 in sample_pairs(G):
        assert phi(G.op(g1, g2)) == H.op(phi(g1), phi(g2))

    assert phi(G.identity) == H.identity

    for g in sample_elements(G):
        assert phi(G.inverse(g)) == H.inverse(phi(g))

    return True

3. Ring Homomorphisms

Definition: φ: (R, +, ×) → (S, +, ×) preserves ring structure.

Required Checks

| ID | Property | Formula | Verification | |----|----------|---------|--------------| | R-1 | Addition Preservation | φ(a + b) = φ(a) + φ(b) | Test on sample pairs | | R-2 | Multiplication Preservation | φ(a × b) = φ(a) × φ(b) | Test on sample pairs | | R-3 | Multiplicative Identity | φ(1_R) = 1_S (if unital) | Explicit check | | R-4 | Additive Identity | φ(0_R) = 0_S | Explicit check |

Derived Properties

  • Kernel: ker(φ) = {r ∈ R : φ(r) = 0_S} is an ideal
  • Ideal Preservation: If I ⊲ R, then φ(I) ⊲ S (for surjective φ)

Test Protocol

def verify_ring_homomorphism(phi, R, S):
    """Verify φ: R → S is a ring homomorphism."""
    for r1, r2 in sample_pairs(R):
        assert phi(R.add(r1, r2)) == S.add(phi(r1), phi(r2))

    for r1, r2 in sample_pairs(R):
        assert phi(R.mul(r1, r2)) == S.mul(phi(r1), phi(r2))

    if R.is_unital and S.is_unital:
        assert phi(R.one) == S.one

    assert phi(R.zero) == S.zero

    return True

4. Module Homomorphisms

Definition: φ: M → N between R-modules preserves module structure.

Required Checks

| ID | Property | Formula | Verification | |----|----------|---------|--------------| | Mod-1 | Addition Preservation | φ(m₁ + m₂) = φ(m₁) + φ(m₂) | Test on sample pairs | | Mod-2 | Scalar Multiplication | φ(r · m) = r · φ(m) | Test on scalar-element pairs | | Mod-3 | Zero Preservation | φ(0_M) = 0_N | Explicit check |

Test Protocol

def verify_module_homomorphism(phi, M, N, R):
    """Verify φ: M → N is an R-module homomorphism."""
    for m1, m2 in sample_pairs(M):
        assert phi(M.add(m1, m2)) == N.add(phi(m1), phi(m2))

    for r in sample_elements(R):
        for m in sample_elements(M):
            assert phi(M.scalar_mul(r, m)) == N.scalar_mul(r, phi(m))

    assert phi(M.zero) == N.zero

    return True

5. Functors (Category Theory)

Definition: F: C → D maps objects and morphisms while preserving composition and identity.

Required Checks

| ID | Property | Formula | Verification | |----|----------|---------|--------------| | F-1 | Object Mapping | F: Ob(C) → Ob(D) | Type check | | F-2 | Morphism Mapping | F: Hom_C(A,B) → Hom_D(F(A),F(B)) | Type check | | F-3 | Identity Preservation | F(id_A) = id_{F(A)} | Test on all objects | | F-4 | Composition Preservation | F(g ∘ f) = F(g) ∘ F(f) | Test on composable pairs |

Test Protocol

def verify_functor(F, C, D):
    """Verify F: C → D is a functor."""
    for obj in C.objects:
        assert F.map_object(obj) in D.objects

    for morph in C.morphisms:
        F_morph = F.map_morphism(morph)
        assert F_morph.source == F.map_object(morph.source)
        assert F_morph.target == F.map_object(morph.target)

    for obj in C.objects:
        assert F.map_morphism(C.identity(obj)) == D.identity(F.map_object(obj))

    for f, g in sample_composable_pairs(C):
        assert F.map_morphism(C.compose(g, f)) == \
               D.compose(F.map_morphism(g), F.map_morphism(f))

    return True

6. Natural Transformations

Definition: η: F ⇒ G between functors F, G: C → D with naturality commuting diagrams.

Required Checks

| ID | Property | Formula | Verification | |----|----------|---------|--------------| | NT-1 | Component Assignment | ∀A ∈ Ob(C): η_A: F(A) → G(A) | Membership check | | NT-2 | Naturality Square | G(f) ∘ η_A = η_B ∘ F(f) | Test all morphisms |

Naturality Diagram

F(A) --η_A--> G(A)
 |             |
F(f)          G(f)
 |             |
 v             v
F(B) --η_B--> G(B)

Commutes: G(f) ∘ η_A = η_B ∘ F(f) for all f: A → B in C.

Test Protocol

def verify_natural_transformation(eta, F, G, C, D):
    """Verify η: F ⇒ G is a natural transformation."""
    for A in C.objects:
        eta_A = eta.component(A)
        assert eta_A.source == F.map_object(A)
        assert eta_A.target == G.map_object(A)
        assert eta_A in D.morphisms

    for f in C.morphisms:
        A, B = f.source, f.target
        eta_A = eta.component(A)
        eta_B = eta.component(B)
        F_f = F.map_morphism(f)
        G_f = G.map_morphism(f)

        left_path = D.compose(G_f, eta_A)
        right_path = D.compose(eta_B, F_f)
        assert left_path == right_path

    return True

7. Composition Laws

Horizontal Composition (Natural Transformations)

Given η: F ⇒ G and ε: G ⇒ H:

(ε ∗ η)_A = ε_A ∘ η_A

Check:

def verify_vertical_composition(epsilon, eta, F, G, H, C, D):
    """Verify (ε ∗ η): F ⇒ H."""
    comp = vertical_compose(epsilon, eta)
    for A in C.objects:
        assert comp.component(A) == D.compose(epsilon.component(A), eta.component(A))
    return verify_natural_transformation(comp, F, H, C, D)

Whiskering

Given functor K: D → E and η: F ⇒ G where F, G: C → D:

(K ∗ η)_A = K(η_A)

8. Governance Application

Mapping to Morphism Governance Framework

| Algebraic Check | Governance Invariant | Interpretation | |----------------|---------------------|----------------| | G-1 (Operation Preservation) | I-1 (One Truth) | A transformation should preserve the declared source structure | | F-3 (Identity Preservation) | I-4 (Scope Binding) | A no-op governance action should remain a no-op | | F-4 (Composition Preservation) | I-2 (Drift Is Debt) | Composed governance actions should not contradict each other | | NT-2 (Naturality Square) | I-6 (Refusal as Structure) | Ordering and scope should not silently change the intended result |

These are conceptual mappings. Current CI and runtime enforcement are described in Paper 2 (papers/morphism-system/main.tex), not by this document alone.

9. Verification Checklist

Use this checklist when validating a morphism claim:

  • [ ] Domain/Codomain: Well-defined on all elements
  • [ ] Functionality: Single-valued (equal inputs -> equal outputs)
  • [ ] Identity: Preserves identity elements
  • [ ] Operation: Preserves the structure's operation(s)
  • [ ] Composition: If applicable, preserves composition
  • [ ] Inverse: If applicable, preserves inverses
  • [ ] Naturality: If natural transformation, all squares commute
  • [ ] Sample Tests: Passes on random sample (>=100 cases)
  • [ ] Edge Cases: Handles identity, zero, absorbing elements
  • [ ] Type Safety: Source/target types match declared signatures

10. Failure Modes

| Failure | Symptom | Example | |---------|---------|---------| | Not well-defined | φ(a) ∉ B | Division by zero in target | | Not functional | a = b but φ(a) ≠ φ(b) | Multi-valued "function" | | Operation broken | φ(a ∗ b) ≠ φ(a) · φ(b) | Transformation that breaks source semantics | | Identity broken | φ(e) ≠ e' | Map that shifts the identity | | Composition broken | F(g ∘ f) ≠ F(g) ∘ F(f) | "Functor" that doesn't respect composition | | Naturality broken | Square doesn't commute | Policy that depends on application order |

11. Code Annotation Standard

Verified (or rejected) morphism claims SHOULD be annotated in the source code when they materially affect mathematical reasoning or proofs.

Passed Verification

# MORPHISM VERIFIED: <YYYY-MM-DD>
# Type: <structure type> (e.g., Group homomorphism, Functor)
# Checks: <check IDs with results> (e.g., G-1 ✓ (100 samples), G-2 ✓, G-3 ✓)
# Protocol: morphism-verification-protocol v<version>

Failed Verification

# MORPHISM CLAIM REJECTED: <YYYY-MM-DD>
# Type: <structure type> (claimed)
# Check FAILED: <check ID>
# Evidence: <counterexample or proof of failure>
# Action: Documented as NOT a morphism. Do not use in composition.
# Protocol: morphism-verification-protocol v<version>

12. References

  • Category Theory: Mac Lane, "Categories for the Working Mathematician"
  • Abstract Algebra: Dummit & Foote, "Abstract Algebra"
  • Governance context: Paper 1 (papers/agentic-mathematics/main.tex)
  • Current enforcement surface: Paper 2 (papers/morphism-system/main.tex)

This document defines formal targets and review criteria. Current product or CI claims must still point to concrete implementations and evidence paths.