---
title: "Lean port-binding proof"
description: "Lean port-binding proof This is a dependency-free Lean 4 example of: - semantically typed local UI ports; - identity-link declarations and their reflexive/symmetric/transitive closure; - bindings as q…"
doc_version: 1
last_updated: 2026-10-15
canonical_url: "http://parc.yolo.scapegoat.dev/note/transcripts/2026/08/06/branch-branch-branch-clim-ui-in-react/readme"
---

# Lean port-binding proof

Lean port-binding proof This is a dependency-free Lean 4 example of: - semantically typed local UI ports; - identity-link declarations and their reflexive/symmetric/transitive closure; - bindings as q…

## Content

# Lean port-binding proof

This is a dependency-free Lean 4 example of:

- semantically typed local UI ports;
- identity-link declarations and their reflexive/symmetric/transitive closure;
- bindings as quotient classes of linked ports;
- the quotient projection `project : Port t -> Binding t`;
- the existence and uniqueness factorization property for maps out of a binding;
- a concrete `f : Binding .document -> Widget`;
- proofs that linked chart, pipeline, and table ports share a binding and widget;
- a tiny executable renderer.

## Run

With `elan` installed, enter this directory and run:

```sh
lean --run Main.lean
```

Expected output:

```text
chart:    <select aria-label="Shared document">Document</select>
pipeline: <select aria-label="Shared document">Document</select>
table:    <select aria-label="Shared document">Document</select>
```

The file uses only Lean's `Init` library and pins Lean 4.32.2 in
`lean-toolchain`.

## Backlinks

- [transcripts/research/01-markdown-thesis-and-pdf-inventory](http://parc.yolo.scapegoat.dev/note/transcripts/research/01-markdown-thesis-and-pdf-inventory)

## Sitemap

- [Home](http://parc.yolo.scapegoat.dev/)
- [Home markdown mirror](http://parc.yolo.scapegoat.dev/index.md)
- [Markdown sitemap](http://parc.yolo.scapegoat.dev/sitemap.md)