远端图式学
记录, 摘要, GAP, 纤维, FarEnd, T 的可视语法
为什么画出来
否定式远端故事可以压成一行:
forall s in ForwardSocket(C), FarEnd(s) ==_apo T.这行只有在箭头类型保持清楚时才正确. FarEnd(s) ==_apo T 不是到隐藏对象 的函数, 不是内核 equality, 也不是 hsame、psame 或 NameCert 分类器 row. 它是在闭合基底已经展示记录、分类器 表面、gap 账本、provenance 路线与 non-internalization marker 之后, 对边界作出的命名承诺.
所以这些图不是装饰. 它们是审计表面: 哪条边可被内部证明消费, 哪条 边只导出 typed 接口, 哪条边只是否定式边界 name, 哪条边是局部 铭写 readout. 如果不区分类型, 同一张图会被误读成:
records -> digest -> hidden source -> T这不是 BEDC. BEDC 的读法是:
closed records traffic socket export apophatic boundary name
---------------------- ------------- ------------------------
records -> ... -> NameCert packet -> socket FarEnd(socket) ==_apo T下面的图式语言很小, 但足够防止几个关键坍缩: 把远端变成载体, 把摘要 变成源, 把自我中心变成全局对象.
图式语法
图里有四类箭头. ASCII 上都像箭头, 类型不同.
| 箭头种类 | 形状 | 含义 | 内核状态 |
|---|---|---|---|
| internal-traffic | 基底内 x -> y |
生成、分类、延续、账本、证书流量 | 可被普通 BEDC 证明路线消费 |
| socket-export | substrate-state --> socket_i |
typed 边界包离开闭合流量区域 | 从基底侧看单向 |
| apophatic-equiv | FarEnd(s_i) ==_apo T |
因基底侧无 discriminator 而作边界同名 | 不是函数, 不是内核 equality |
| inscription-read | event --> InscriptionPoint(T,C,t) |
对局部累积事件的 aspectual 读法 | 局部读出, 不是把 T 拉入内核 |
闭合内部链是:
records -> generators -> classifiers -> Cont -> GAP -> NameCert这类箭头可以自由复合, 因为项始终留在显示基底里. 分类器行可以 接 Cont 行; Cont 行可以接 gap 账本; gap 账本可以接局部 NameCert obligation. 复合后仍是内部审计 route.
一旦某行被读成接口, 箭头类型改变:
NameCert / GAP / refusal ledger --> socket_i这不表示基底生成了 far side. 它表示基底生成了一个 typed 边界包: 这里需要的供给不由本基底生成, 而这个需求已经 被 ledgered.
远端边是第三种类型:
FarEnd(socket_i) ==_apo T这不是接口到 T 的函数. 它是边界等价 name: 从基底 侧看, 没有可接受的 discriminator 能把这个接口的远端和共同否定式位置 分开.
局部铭写边是第四种类型:
observer-event --> InscriptionPoint(T,C,t)它把一个局部事件读成铭写 aspect. 它不把 T 拉进记录侧 内核, 也不给另一个观察者直接访问这个局部自我中心的能力.
复合表
行表示左边已有箭头, 列表示下一条箭头.
| from / to | internal-traffic | socket-export | apophatic-equiv | inscription-read |
|---|---|---|---|---|
| internal-traffic | 可 | 可 | 不可 | 不可 |
| socket-export | 不可 | 不可 | 可 | 不可 |
| apophatic-equiv | 不可 | 不可 | 只可作对称命名 | 不可 |
| inscription-read | 可, 但只经由其记录侧 event | 不可 | 不可 | 不可 |
最后一行需要小心. inscription-read -> internal-traffic 只有在复合回到那个 被读的记录侧 event 时才允许. 一个事件可以记录侧地读成 ledgered observation, 也可以铭写侧地读成 InscriptionPoint(T,C,t). 内部流量消费的是 event、账本、路线、NameCert 行, 不是否定式 边界 name.
一个失败复合
最诱人的非法复合是:
ObsDigest(C,t)
-> ObsFib(ObsDigest(C,t))
-> FarEnd(ObsFib(ObsDigest(C,t))) ==_apo T
-> T : Hist前两步可以做成已入账的 digest/fiber 路线. 第三步是否定式命名. 最后一步没有类型. ==_apo 不返回载体的居住元, 也不给 BHist 值. 这个尝试失败, 因为它把否定式边界名接到了内部载体 准入上.
另一个非法复合是:
SelfCenter(C,t)
:= InscriptionPoint(T,C,t)
-> FarEnd(socket)
-> socket provenance局部铭写读出不是反向 socket. 它不能恢复来源纤维、另一个 观察者的自我中心或远侧来源. BEDC 要求这些读法经过记录侧 证据、inter-Hist 一致性行和缺口账本.
带类型的闭合基底图
Evidence
闭合流量. 内部一切都必须经过显示结构:
records -> generators -> classifiers -> Cont -> GAP -> NameCert凡是不能在这里生成、定义、证明或证书化的供应, 都变成带类型的接口包, 不是无类型的外部.
带类型的远端图是:
closed substrate C
internal-traffic region
-----------------------
records -> generators -> classifiers -> Cont -> GAP -> NameCert
| | |
| socket-export| | socket-export
v v v
socket s1 socket s2 socket s3
| | |
| apophatic-equiv |
v v v
FarEnd(s1) FarEnd(s2) FarEnd(s3)
\ | /
\ | /
+------------+-----+
|
v
T进入 T 的箭头是边界名. 它们说: 接口已经入账之后, 基底没有可接受的远侧判别器. 它们不说 T 是值、 状态、历史、摘要、源或隐藏的全局宇宙.
没有. 它们只在内部路线停止后标记否定式同名.
跟 NameCert 标准图的关系
远端图不是 NameCert 图之外的另一张图. 它是接在 NameCert 表面 输入端和边界端的 region.
papers/bedc/parts/proof_obligations/lean_scaffold_contract.tex 里的标准 scaffold 区分:
| 标准 region | 控制内容 |
|---|---|
| abstract carriers | histories、签名、packages、domains、bundles、evidence |
| relational 对象层 | 标记 introduction、hsame、签名 generation、gap membership |
| checked-shape 目标 | base reflection 与 exact globalize classify-iff 路线 |
在 concrete NameCert 包里, 常用六字段图是:
carrier -> classifier -> exactness -> ledger -> stability -> packet route这六字段完全住在 closed-substrate region 里. 它认证可见 name、分类器 行为、sameness 何时可反射的 exactness 状态、保存源 memory 的账本 行、保护输运的稳定性行, 以及 downstream consumer 可 replay 的包 route.
远端图补齐它的左边和下边:
source / record pressure
|
v
carrier -> classifier -> exactness -> ledger -> stability -> packet route
| |
| v
| provenance fiber
| |
v v
unresolved classifier socket-export
residue socket_i
|
v
FarEnd(socket_i) ==_apo T缝合规则是:
NameCert internal route
+ displayed gap/provenance row
+ typed socket-export
+ apophatic-equiv只有前两个成分是内部证明 traffic. 第三个导出边界 packet. 第四个是 边界 name. 合法复合可以说:
packet route 认证 visible name,
ledger 保存 provenance fiber,
socket 记录 non-internalized forward pressure,
socket far end 被否定式命名为 T.它不能说:
NameCert 已经把 T 证明成内部 value.这就是 fitting. 远端图和 NameCert 图是一张审计表面的两个 region, 不是两张互不相干的图. NameCert 管闭合 name; 远端 diagrammatics 管闭合 name 承认 non-internal 边界的位置.
局部读出图
对一条观察者链, 图变成:
Hist/Obs chain C_i
|
| internal-traffic
v
Obs(C_i)<=t = UniverseFor(C_i,t)
|
v
d_i(t) = ObsDigest(C_i,t)
|
| GAP / provenance packet
v
ObsFib(d_i(t))
|
| socket-export
v
FarEnd(ObsFib(d_i(t))) ==_apo T这是 hash-like 读法的核心纪律. 摘要可见. 纤维被 ledgered. 远端以 否定式命名.
Evidence
三层.
finite readout = digest / Obs / local records
hidden provenance = fiber / GAP / source rows
apophatic far end = FarEnd(...) ==_apo T这不是隐藏形而上学的图. 它显示一个证明或解释可以在哪里消费信息. 摘要 equality 是可见表面 equality. 纤维 equality 需要出处行 或 exactness certificates. 远端 sameness 是否定式承诺, 不是 源 identity.
自我中心图
自我中心在局部链点上, 不在远端上.
one local accumulation event E(C,t)
records-side reading inscription-side reading
-------------------- ------------------------
record in Obs(C) InscriptionPoint(T,C,t)
classifier / package / ledger SelfCenter(C,t)
Cont / selector witness允许的定义是:
SelfCenter(C,t) := InscriptionPoint(T,C,t)禁用的等式是:
SelfCenter(C,t) = T差别是结构性的. 第一个表达式把局部事件读作铭写 aspect. 第二个把 远端作为对象塞进观察者.
对应的 Lean 包不是神秘 subject carrier. 它是 lean4/BEDC/Derived/InscriptionPointUp/TasteGate.lean 里的有限载体 InscriptionPointUp.mk, 字段是 history、gap、supply、handoff、 event、ledger、transport、routes、provenance、nameCert. 这些 行让局部读出可审计. 没有一个行是作为 value 的 T.
多观察者图
多个观察者不共享一个全局宇宙对象. 它们共享远端承诺:
C_i: ObsDigest -> ObsFib -> FarEnd \
\
+--> T
/
C_j: ObsDigest -> ObsFib -> FarEnd /这不是摘要 equality.
d_i(t) = d_j(t') not required也不是直接进入另一个 self-center. 他心通过记录侧 evidence、 inter-Hist coherence, 以及其 observation 纤维也终止于同一个否定式远端 的承诺出现.
两者都不蕴含. 相似性是可见表面上的证据. 它不坍缩源、纤维 或 self-center.
具体 coherence site 是 lean4/BEDC/Derived/InterInscriptionCoherenceUp/TasteGate.lean, 对应 paper site 是 papers/bedc/parts/concrete_instances/9093_interinscriptioncoherence_namecert_construction.tex. 它的包行是两个铭写 endpoints、一个 inter-Hist 局部性 账本、输运、路线、provenance 和局部 naming data. 这正是图允许的 东西: 成对局部端点加显示 coherence ledger. 它不是 quotient 观察者 equality.
例子: 两个观察者报告同一个摘要
假设两条观察者链在各自 stage 报告相同可见摘要:
d_A(t) = d_B(t)口语会说: “他们看到了同一件事.” 图式把这句话拆开.
C_A records <= t C_B records <= t
| |
v v
d_A(t) ---------------- equal -------- d_B(t)
| |
| GAP/provenance | GAP/provenance
v v
ObsFib_A(d) ObsFib_B(d)
| |
| socket-export | socket-export
v v
FarEnd(ObsFib_A(d)) FarEnd(ObsFib_B(d))
\ /
\ /
+---------- ==_apo ------------+
|
v
T证明读法有三步.
第一, 摘要 equality 不推出纤维 equality:
d_A(t) = d_B(t) does not imply ObsFib_A(d) = ObsFib_B(d)摘要相等只在可见包或分类器表面上. 纤维相等 需要显示精确性证书、源行输运或更强的 反射定理. 没有这些, 共同摘要只说明两条链落在同一个可见 标记上.
第二, 不同纤维仍然可以终止于同一个否定式远端 name:
ObsFib_A(d) != ObsFib_B(d) allowed
FarEnd(ObsFib_A(d)) ==_apo T allowed
FarEnd(ObsFib_B(d)) ==_apo T allowed这里的同名不是纤维 sameness, 而是 shared 远端 commitment.
第三, 口语句子变成 BEDC 的复合陈述:
"同一件事"
= visible digest equality
+ 必要时的 displayed inter-Hist coherence
+ shared far-end commitment
- source identity claim
- self-center identity claim所以 “他们看到了同一件事” 不表示 C_A 与 C_B 有一个源历史、一个 纤维、一个自我中心或一个局部 universe. 它表示二者记录暴露同 一个可见摘要, 且它们的 observation-fiber 路线在同一个否定式 远端 name 下读取.
无穷图
无穷读法也是图式性的:
finite readouts: d1(t) d2(t') d3(t'')
| | |
v v v
Fib(d1) Fib(d2) Fib(d3)
| | |
v v v
FarEnd FarEnd FarEnd
\ | /
\ | /
+-----+-----+
|
v
T ==_apo infinity_apo读成:
T 是所有有限读出 fiber 的共同 far-end role.不要读成:
T 是无穷总体本身.这张图跟 apophatic-infinity.zh-CN.qmd 相容: 每个有限读出都有 provenance 纤维, 没有一个有限读出穷尽其 far side, 共同远端 role 只能作为边界 vocabulary 被命名为 infinity_apo.
图式不能画什么
图式有用, 也因为它拒绝一些在别的 ontology 里自然的图.
| 想画的图 | 为什么拒绝 | 硬画会引入的坍缩 |
|---|---|---|
SelfCenter(C_i,t) ?= SelfCenter(C_j,t') |
自我中心是 inscription-read endpoint, 不是带跨观察者 equality 的载体 value | quotient 观察者 equality 与 hidden shared subject |
| quantum-style 的远端 superposition | BEDC 不供应 ambient 状态 ontology 让远端 alternatives 作为 vector states | 边界 name 变成状态 space |
| 单一 meta-view 的 observer-of-observer | 每一层观察者都要重起闭合基底, 带自己的记录、账本、接口 | 全局观察者与 hidden synchronization 框架 |
| time-reversal arrows | Time(C) 是记录的 monotonic 保持 order; 反向边不是态射 |
provenance replay 变成源 recovery |
H(Omega) = T |
没有全局可读宇宙 Omega, 没有全局 hash, T 也不是摘要 value |
全局 universe 对象加 digest-as-far-end |
从 FarEnd(s) 直接读源 |
apophatic-equiv 不能反演成 provenance 纤维 | 接口变成预言机 |
这些不是缺失功能, 而是记号边界. 画出其中任何一条边, 就已经离开 BEDC 的 diagram language.
内核 site 指针
这篇里的图式词汇有具体 Lean 包和 paper site.
| 图式成分 | 内核或 paper site |
|---|---|
FarEnd(s_i) 纤维包 |
lean4/BEDC/Derived/ApophaticFiberFarEndUp/TasteGate.lean |
| 否定式接口包 | lean4/BEDC/Derived/ApophaticFarEndSocketUp/TasteGate.lean |
| 接口 export / 边界包 | lean4/BEDC/Derived/GapSocketBoundaryUp/TasteGate.lean |
| 摘要, 纤维, gap, 远端 seal | lean4/BEDC/Derived/HashApophaticSealUp/TasteGate.lean |
| 局部铭写 read | lean4/BEDC/Derived/InscriptionPointUp/TasteGate.lean |
ObsDigest -> ObsFib |
papers/bedc/parts/visions/apophatic/hash_like_apophatic_fixed_point.tex |
FarEnd(...) ==_apo T |
papers/bedc/parts/visions/apophatic/far_end_diagrammatics.tex |
| 自我中心铭写 | papers/bedc/parts/visions/apophatic/fixed_point_and_inscription.tex |
inter-Hist 铭写 coherence |
lean4/BEDC/Derived/InterInscriptionCoherenceUp/TasteGate.lean 和 papers/bedc/parts/concrete_instances/9093_interinscriptioncoherence_namecert_construction.tex |
跟 NameCert scaffold 的关系 |
papers/bedc/parts/proof_obligations/lean_scaffold_contract.tex |
这些 Lean 文件是 BHist 行上的包 carriers, 带 encode/decode 与 field-faithfulness gates. 这正是这些图应有的形式化层级: 内核检查有限行 discipline, 不检查一个叫 T 的隐藏对象.
压缩图
整张图可以压成一条 typed 链:
Obs(C_i)<=t
-> ObsDigest(C_i,t) internal-traffic
-> ObsFib(ObsDigest(C_i,t)) GAP/provenance
--> socket / fiber boundary socket-export
-> FarEnd(ObsFib(ObsDigest(C_i,t))) ==_apo T apophatic-equiv以及一个局部读法:
SelfCenter(C_i,t) := InscriptionPoint(T,C_i,t).图式学不添加理论. 它让既有理论保持 typed: 内部路线可复合, 接口 exports 不可反演, 否定式 sameness 不变成 equality, 局部铭写不变 成全局 subject.
T ≡_apo infinity_apo 记号背后的 far-end role. 从 digest 到局部宇宙 →
universe-for-observer、time、space 如何从同一张图读出.
相关阅读
同一结构的 digest/fiber 读法. 所有 socket 的统一远端
所有 forward-binding 远端共享同一个否定式名字的原则. 形式化路线
为什么可见名字需要 source rows、packet routes 和 audit fields.
— The Omega Institute newmath / BEDC, May 2026