fabricates-a-formation-holding-the-bytes-its-condition-came-down-to.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The condition of the join comes down to real bytes, not to a symbol, and the
# two sides differ in shape, so the firing fabricates a formation whose every
# attribute is a copy of 'L_join' holding those bytes as a datum under 'on🌵'
# (#2026). The program asks that formation for 'pe', which the right side
# binds alone, so its copy asks the left side for 'pe' too.
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.c
    join:
      on: 𝛿1
      left: $.a
      right: $.b
      otherwise: L_join
location: 'Q.y'
input: '⟦ y ↦ ⟦ c ↦ ⟦ Δ ⤍ 3A- ⟧, a ↦ ⟦ φ ↦ Φ.wu ⟧, b ↦ ⟦ φ ↦ Φ.ol, pe ↦ Φ.ki ⟧, λ ⤍ L_fork ⟧.pe ⟧'
result: '⟦ λ ⤍ L_join, on🌵 ↦ ⟦ Δ ⤍ 3A- ⟧, left🌵 ↦ ρ.left🌵.pe, right🌵 ↦ ρ.right🌵.pe ⟧'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝔻(Φ.a🌵0):
        𝛿·1·1 := 3A-
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)
      fabricated 𝑛·1·1 := Φ.wu:φ and ⟦ φ ↦ Φ.ol, pe ↦ Φ.ki ⟧  # ⟦ left🌵 ↦ Φ.wu:φ, right🌵 ↦ ⟦ φ ↦ Φ.ol, pe ↦ Φ.ki ⟧, φ ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 3A-:Δ, left🌵 ↦ ρ.left🌵.φ, right🌵 ↦ ρ.right🌵.φ ⟧, pe ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 3A-:Δ, left🌵 ↦ ρ.left🌵.pe, right🌵 ↦ ρ.right🌵.pe ⟧ ⟧