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):
      𝔻(ξ.c):
        𝛿·1·1 := 3A-
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)
      𝕄(ξ.a):
        morphed 𝑛·1·1 := Φ.wu:φ
      𝕄(ξ.b):
        morphed 𝑛·1·2 := ⟦ φ ↦ Φ.ol, pe ↦ Φ.ki ⟧
      fabricated 𝑛·1·3 := 𝑛·1·1 and 𝑛·1·2  # ⟦ left🌵 ↦ 𝑛·1·1, right🌵 ↦ 𝑛·1·2, φ ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 3A-:Δ, left🌵 ↦ ρ.left🌵.φ, right🌵 ↦ ρ.right🌵.φ ⟧, pe ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 3A-:Δ, left🌵 ↦ ρ.left🌵.pe, right🌵 ↦ ρ.right🌵.pe ⟧ ⟧
    morphed 𝑛·0·1 := ⟦ λ ⤍ L_join, on🌵 ↦ 3A-:Δ, left🌵 ↦ ρ.left🌵.pe, right🌵 ↦ ρ.right🌵.pe ⟧