CRDTJoin-Semilattice Basics
Order, join, inflationary updates, and merge law.
CRDTDelta-CRDTs
Delta mutation semantics and bounded joins.
CRDTOp-Based CRDTs
Commutative monoids and causal delivery.
CRDTCounterexample: Non-Idempotence
Why repeated delivery breaks convergence.
LOGVector Clocks
Causality as a partial order of events.
LOGVersion Vectors
Compact causality with mergeable summaries.
LOGCausal Delivery
When ops are safe to apply without divergence.
LOGLog as Boundary Object
Certificates of application order and visibility.
LAMBDAMerge as Lambda Term
Executable proof of merge law.
LAMBDAChurch Encodings
Representing state and merge functionally.
LAMBDABeta/Eta as Contract Proof
Reduction as verification of API promises.
LAMBDASubstitution Hazards
Counterexamples for mistaken equivalences.
CATEGORYAdjunctions as UI Switch
Expand vs filter as left/right adjoints.
CATEGORYUnits and Counits
Explicit promises between abstraction layers.
CATEGORYFunctorial Logs
Log folding as a functor into state.
CATEGORYLimits and Colimits
Join as colimit and merge as universal property.
APIState vs Delta Boundary
Input contracts and server obligations.
APIConflict-Free Promise
When convergence is guaranteed and when not.
APICounterexample: Non-Inflationary Delta
How a bad delta violates monotonicity.
APIAPI Surface Compression
Minimal exposed operations without losing invariants.
TYPEDependent Type: Inflationary Delta
Delta(s) = { d | s ⊑ merge(s,d) }.
TYPERefinement Types for Merge
Type-level monotonicity and idempotence.
TYPEProof-Carrying Deltas
Certificates attached to updates.
TYPEType-Directed API Boundaries
Interface design driven by invariants.
INVARIANTJoin Monotonicity
x ⊑ merge(x,y), y ⊑ merge(x,y).
INVARIANTEventual Convergence
Convergence definitions and operational tests.
INVARIANTCommutativity Tests
Minimal checks to validate merges.
INVARIANTIdempotence Tests
Repeated delivery and duplicate ops.
UXLayered Annotation Grammar
Surface/deep/meta with tag filters.
UXInspector as Proof Oracle
Contextual proof + counterexample view.
UXAttention Budget
Controls for showing only what is stable.
UXSemantic Styling Map
Visual class semantics across plates.
TRACETrace Grammar
Def/OpenGoal/Check/Solve as log events.
TRACEReplayable Plate Artifacts
Content-addressed, reproducible runs.
TRACECounterexample Registry
Catalog and index of failure cases.
TRACEExecution vs Narrative
Keep provenance for every narrative step.