H0mework

低能系列 1 · 2026-10-11

电流出庭

从耦合传播到实际电子、Coulomb 返回与 Born 修饰

The Current Takes the Stand: From Coupled Propagation to Actual Electrons, Coulomb Response, and Born Dressing

正文 PDFDOI 10.5281/zenodo.23299174
  • 28条主张
  • 60个 Lean 模块
  • 147个声明
  • ✓ 内核检查全部通过

摘要

本文从共同源 Spin×SU(7) 理论的原九场作用出发，把耦合传播接到实际电子的电磁读数、Newton 空间返回与 Born 修饰。该理论的群结构、物质载体、唯一真空与背景常数都由同一源数据生成，没有拟合参数；下列系数均为这一源下的精确输出。同一个源生电子态认回原静止腿，原时间电流为 −1-1、电磁荷为 +1+1；一次 Coulomb 标量和 ordinary photon 响应保留全部64权、两端修正、独立年龄窗及原源振幅，photon 公式在原极点支的充分小尺度上成立。完整289场的混合电磁载体由真实作用 Hessian 生成；任意正时钟重表达同时变换频率留数与 Jacobi 导数，保持原通量恒等式。对 Schwartz 输入，原全方向 Green 与实际移动两端自产共同红外范围及可积控制，使同一次、相反动量转移的真实 Fourier 积分返回 Newton 卷积。完整 N3 复合响应的单位归一进一步产生四个 Born 重叠：每一对至少有一端为独立 sharp 时，其乘积 ZZ 精确给出 Cfull=ZCbaseC_{\mathrm{full}}=ZC_{\mathrm{base}}，两者之差的模为 (1−Z)∣Cbase∣(1-Z)|C_{\mathrm{base}}|。这条链建立在同一基础上：共同局部九场发展及其初值导数、全三动量 Jacobi 传播与原场恢复、两相位四阶导数作用、按原留数归一的非零在壳树交换，以及固定背景上 L2(R3,C12)L^2(\mathbb R^3,\mathbb C^{12}) 的全部有限 CAR 词；范数连续的有界自伴规范控制生成全实时间、全实幅度的幺正发展，零幅度的算子范数导数同时读回 Duhamel、Kubo 与原电流。Thomson／full-light／contact 匹配只作为条件消费者出现。

主张与证明

每条主张都登记在逐主张映射中。展开一条，可以看到它的陈述、在论文中的位置，以及证明它的 Lean 模块与复现程序。L18–L25 的登记原文为英文，这里是中文译文。

1
2
3
4
5
6
7
9
10
11
12
13

按阅读顺序排列。黑孔：Lean 证明，内核检查已通过；灰孔：由复现程序支撑，不含 Lean 声明。

  1. L17对范数连续的有界自伴算子历史R（每个紧时间区间有界即可），对任意实ε、任意起止时刻和任意L²初态，生成真实发展、唯一性、范数守恒、双时刻幺正传播及原弱方程。§1

    对范数连续的有界自伴算子历史R（每个紧时间区间有界即可），对任意实ε、任意起止时刻和任意L²初态，生成真实发展、唯一性、范数守恒、双时刻幺正传播及原弱方程。每个固定实时间上的真实传播在ε=0有算子范数导数D(t)；原字段导数是原时间Duhamel积分，原电流导数是同一Kubo核与Stage10响应。零过去控制保持自由过去，准备相位保持。

    位置：§1；§8；D.2；D.4；图 3✓ 内核检查已通过

    Lean 模块 · 4

  2. L1单份原 Weyl 库存加复 Λ⁴ 标量，代入既有一圈代数公式得 b₀ 为 (56/3,4,1/3,−28)。§2

    单份原 Weyl 库存加复 Λ⁴ 标量，代入既有一圈代数公式得 b₀ 为 (56/3,4,1/3,−28)。原三个本构参数均为1/2；母 U(1) 迹配对为原生配对的两倍。指定坐标的 I₃=1+4t、I₂=1+t/3、I₁=1/2−7t 在 −1/4<t<1/14 同时为正，三条曲线无共同交点。

    位置：§2；A.1✓ 内核检查已通过

    Lean 模块 · 3

  3. L2原四项真空的完整 7×21 Yukawa 矩阵满足 YY†=diag(2,2,2,4,2,0,0)，秩5、输入核16。§2

    原四项真空的完整 7×21 Yukawa 矩阵满足 YY†=diag(2,2,2,4,2,0,0)，秩5、输入核16。原 P286 标量—规范二次块秩9，谱为 0[3],1[6] 及 6x³−26x²+27x−8 的三根。裸标量母紧稳定子为 (SU(2)×USp(4)×U(1))/Z₂，与 P286 相交为指定嵌入 SU(2)。

    位置：§2；A.2–A.3✓ 内核检查已通过

    Lean 模块 · 1

    复现程序与证据 · 1

  4. L4原外幂基与四个 Dirac 分量生成252复坐标及完整算子代数；压缩保留返回项 C(AB)=C(A)C(B)+C(AQB)。§2

    原外幂基与四个 Dirac 分量生成252复坐标及完整算子代数；压缩保留返回项 C(AB)=C(A)C(B)+C(AQB)。同一已生成九场配置上，独立对偶响应为 χ(Aψ)=4s a⁻³⟨ψ̂θ,SAψ̂θ⟩，实际密度满足 a³ρ=4s。

    位置：§2；§3.4；D.3✓ 内核检查已通过

    Lean 模块 · 3

  5. L7完整252上的 Q=γ⁵+2P₆ 相位变换常化原算子，原时间由同一相位恢复。§2.5

    完整252上的 Q=γ⁵+2P₆ 相位变换常化原算子，原时间由同一相位恢复。既有 canonical 制备切向满足 K₈₈=CᵀH₁₁₂C、H₁₁₂C=RK₈₈、CᵀR=I；九条对称方向生成79维商，103系统保真分成79＋24。外围 canonical 最大发展纤维为一般522、原点524、|k|²=5929/1800 球上530维，全部原1078行回写。

    另由原70实标量的Yukawa混合核与实规范轨道正交条件生成43维背景不变空间，适配为23实单态及5个四实维块。程序给源矩阵及适配基，正式Lean给四维块行列式、逆及原参数代入。

    位置：§2.5；§4.4–4.5；B.2✓ 内核检查已通过

    Lean 模块 · 2

    复现程序与证据 · 4

  6. L3每个允许的七维空间齐次初值附近，存在同一正初值半径、双向时间条带和统一 Lipschitz 解族，整个闭初值球都生成完整九场联合零残差。§3.1–3.2

    每个允许的七维空间齐次初值附近，存在同一正初值半径、双向时间条带和统一 Lipschitz 解族，整个闭初值球都生成完整九场联合零残差。原背景 seed 处的初值 Fréchet 导数是 exp(tJ)，并满足同一 Jacobi 方程；导数基点保持为原 seed。

    位置：§3.1–3.2；B.1✓ 内核检查已通过

    Lean 模块 · 2

  7. L5原径向方程是 ∂t²f/N²−Δf−2f=0。§3.3

    原径向方程是 ∂t²f/N²−Δf−2f=0。任意实三动量的基本解分别由 sinh、临界线性函数、sin 给出，初值为零、初速度为 cos(k·x)。代回原九场后八类残差精确为零，完整余标架残差为 ε² 乘原二阶负载，故九场第一变分为零。

    位置：§3.3✓ 内核检查已通过

    Lean 模块 · 1

  8. L6原289实字段一阶 jet 的二次作用逐次消元为217、145、121变量；Ward 行变换保留112个等价方程。§4.1–4.3

    原289实字段一阶 jet 的二次作用逐次消元为217、145、121变量；Ward 行变换保留112个等价方程。九个源对称方向的常数可逆 minor 生成103维截面；原点秩98，额外五维核保留。轴向十块产生22个不同有理因子、总时间次数126；同步空间／spin／color 旋转将完整原字段及方程运输到所有实三动量，径向目录有14个因子乘积块。

    位置：§4.1–4.3；B.2

    复现程序与证据 · 5

  9. L8从原canonical79算子消去原点可逆的77方向，得到原向量相位ϕ与轴向相位θ的二次幅度、四阶导数有效作用。§5

    从原canonical79算子消去原点可逆的77方向，得到原向量相位ϕ与轴向相位θ的二次幅度、四阶导数有效作用。低动量支为

    λφ2=−5941675∣k∣2−10152864939884375∣k∣4+O(∣k∣6),λθ2=13∣k∣2−305329160∣k∣4+O(∣k∣6).\lambda_\varphi^2=-\frac{594}{1675}|k|^2-\frac{10152864}{939884375}|k|^4+O(|k|^6),\qquad \lambda_\theta^2=\frac13|k|^2-\frac{3053}{29160}|k|^4+O(|k|^6).

    位置：§5；B.3；图 2

    复现程序与证据 · 2

  10. L9完整252物质载体产生158个顶点：48规范、24 Lorentz、16余标架、70标量。§6.1–6.3

    完整252物质载体产生158个顶点：48规范、24 Lorentz、16余标架、70标量。97个活跃源进入79＋24动态块、辅助接触与九行源相容条件；prepared 实源的24补块顶点消去。连接逆给出 3N/16 η_ab AᵃAᵇ 轴向四费米项。外围61标量源由实际投影逆消费，非零Yukawa返回及独立对偶方程保持。

    位置：§6.1–6.3；C.2✓ 内核检查已通过

    Lean 模块 · 2

    复现程序与证据 · 3

  11. L10原自由投影生成216复维全动量 Hermitian 谱、原／共转频率及252字段外腿。§6.4–6.6

    原自由投影生成216复维全动量 Hermitian 谱、原／共转频率及252字段外腿。两条实际Dirac方程支付18项源条件；真实守恒四外腿的两种排列均消费完整79动态块并回写289行。原作用动能及留数确定归一；已核右手尺度 2^(−1/4)，相应四腿树系数精确减半。

    位置：§6.4–6.6；C.1；C.3✓ 内核检查已通过

    Lean 模块 · 2

    复现程序与证据 · 6

  12. L11原Hodge消元得到 L=N/(2σ)κ(E,E)−1/(2σN)κ(B,B)。§6.7

    原Hodge消元得到 L=N/(2σ)κ(E,E)−1/(2σN)κ(B,B)。共同转换固有钟、连接一形式和密度后，native配对中的电／磁逆系数为 108/125、125/27；横向规范波相对于原物质／标量的特征速度比为 125/54（原坐标速度分别为 1/N 与 N）。12静态电荷源回写289行，144电荷响应在零动量正则，全方向零动量Coulomb留数为零。

    位置：§6.7；C.3；§14.1

    复现程序与证据 · 3

  13. L12原 H₁₂=spin₄⊗span{e₀₅,e₁₅,e₂₅} 对全部48规范力封闭。§7.1

    原 H₁₂=spin₄⊗span{e₀₅,e₁₅,e₂₅} 对全部48规范力封闭。两侧物质方程生成48×48响应，等于原289作用的物质Schur消元；三处非空逆点的2304条目逐项核对。零空间动量下由正时间方程、delta jump及正阻尼半轴积分恢复同一响应，保留原零模。

    位置：§7.1

    复现程序与证据 · 2

  14. L13原12维占据系数生成 L²(ℝ³,ℂ¹²) 上强连续幺正发展、零过去Bochner受迫解及同初值mild唯一性。§7.2–7.3

    原12维占据系数生成 L²(ℝ³,ℂ¹²) 上强连续幺正发展、零过去Bochner受迫解及同初值mild唯一性。实际自伴生成元满足 f∈Dom(H) ↔ h(2πξ)f̂∈L²，Schwartz测试读回原偏导算子。真实holonomic原场在同一系数中给出 H_original(0)=h₀+ωQ；原独立对偶弱式保持。

    位置：§7.2–7.3；D.1✓ 内核检查已通过

    Lean 模块 · 3

  15. L14连续L²规范控制历史由真实Duhamel产生有界准备映射K；对任意实时间t，范数界为 ∥Kt∥≤∣∫0t∥F(τ)∥ dτ∣\|K_t\|\leq|\int_0^t\|F(\tau)\|\,d\tau|。§7.3

    连续L²规范控制历史由真实Duhamel产生有界准备映射K；对任意实时间t，范数界为 ∥Kt∥≤∣∫0t∥F(τ)∥ dτ∣\|K_t\|\leq|\int_0^t\|F(\tau)\|\,d\tau|。原占据向量给出 Kρ₀K†。真实非零控制生成某个正时间非零准备，归一后为单位正泛函。完整空间观测A先拉回 K†AK，再形成252维母作用；pairedMother 1 在完整算子之后施加原自旋交换S，独立对偶读回的因子 4 spinScale 保持，见正文(7.13a)及(D.2)。

    位置：§7.3；D.3✓ 内核检查已通过

    Lean 模块 · 2

  16. L15任意有限L²测试族与准备向量的共同span提供真实有限Fock载体；CAR递推产生全部有限词矩、伴随正性与测试族扩张一致性。§7.4

    任意有限L²测试族与准备向量的共同span提供真实有限Fock载体；CAR递推产生全部有限词矩、伴随正性与测试族扩张一致性。测试可不正交、相关或重复。完整词先在Fock中组合，再经 J†WJ 与同一准备映射进入母作用读数。

    位置：§7.4；D.3✓ 内核检查已通过

    Lean 模块 · 2

  17. L16原P286作用生成局域有界自伴力T与电流B，B=−spinScale QT；真实 L∞×L² 乘法使电流密度可积。§7.5

    原P286作用生成局域有界自伴力T与电流B，B=−spinScale QT；真实 L∞×L² 乘法使电流密度可积。Duhamel给出双侧响应 i∫⟨u,[R_H(s),B_H(t)]u⟩ds，完整CAR四点及原Stage10共同消费。原时间由 U_original 与准备总相位 P(t+preparedAt) 恢复，多时CAR逐腿保留相位。

    位置：§7.5；§8.3；D.4✓ 内核检查已通过

    Lean 模块 · 2

  18. L18完整外幂／标量／物质／独立对偶的联合 EM 作用生成 +/-1/2 的相对实 CAR 增量，并保留输入／标量荷余项。§9.1–9.4

    完整外幂／标量／物质／独立对偶的联合 EM 作用生成 +/-1/2 的相对实 CAR 增量，并保留输入／标量荷余项。实际复合电流满足 J_i=0（i>=73）与 F0^T J=(e0+e1)w_J，保留 native／coframe／体积密度／物质／互补／retained 的完整配置积分及原两份逆价格。每个单位实空间方向给出完整静态 Schur／contact／complement 返回、-kappa^2 留数及原 O(kappa) 有限因子界。

    位置：§9.1–9.4；§9.5；附录 F.2✓ 内核检查已通过

    Lean 模块 · 6

  19. L22同一个源生 SourcePreparation 提供 sourceProfile、其配置背景单位态、nativeY=-1 及完成的源腿。§9.2

    同一个源生 SourcePreparation 提供 sourceProfile、其配置背景单位态、nativeY=-1 及完成的源腿。完整光子振幅 A 与 A/(h_source*c_source)，连同完整极化／双预解界和全 Y 定义域／截断，组成已生成的 typed ordinary 输入。

    位置：§9.2；§9.5；附录 F.1✓ 内核检查已通过

    Lean 模块 · 2

  20. L20字面 EM 方向生成外幂权重与 dressed 联合荷单位 1/2。§9.3

    字面 EM 方向生成外幂权重与 dressed 联合荷单位 1/2。创建与湮灭的 character 分别为 +i/2 与 -i/2。完整准备余向量是同一完成轮廓上的 (conj(c_left)+c_right)J。GT 的 character／完成腿／电流读数均为同一实倍数 -10/11，但不主张完整生成元相等。

    位置：§9.3✓ 内核检查已通过

    Lean 模块 · 2

  21. L21实际 edge0 的 electronUnit=1；其独立对偶 Noether 电流等于 h_source，滤波电流保留电荷对易余项。§9.3–9.5

    实际 edge0 的 electronUnit=1；其独立对偶 Noether 电流等于 h_source，滤波电流保留电荷对易余项。完整静态留数 C_T、有限极点／contact／complement Schur 及 C_T/(h_source*c_source) 均已生成；源匹配返回以 ordinaryFull-lightResponse=sourceCEM+contactResponse 为条件。

    位置：§9.3–9.5；§10.1；附录 F.2✓ 内核检查已通过

    Lean 模块 · 4

  22. L19K*=(9023/9000)sqrt(30) 由实际静态逆生成。§9.4

    K*=(9023/9000)sqrt(30) 由实际静态逆生成。对独立准备，C_comp=K*w_D*w_S；其完整原静态留数收缩为 -C_comp，而 +kappa^2 乘全方向完整相互作用趋于 +C_comp。约化标量只除一次 h_source*c_source(0)。

    位置：§9.4；附录 F.2✓ 内核检查已通过

    Lean 模块 · 1

  23. L23修复后的 owner 按原作用单位绑定 ordinaryFull：ordinaryFull = (h_source*c_source)*beta*input.normalizedAmplitude = beta*input.amplitude，其中 beta 是同一准备余向量的源端光子左读取器。§9.5

    修复后的 owner 按原作用单位绑定 ordinaryFull：ordinaryFull = (h_source*c_source)*beta*input.normalizedAmplitude = beta*input.amplitude，其中 beta 是同一准备余向量的源端光子左读取器。保留原 full-light／contact 方程 ordinaryFull-lightResponse=sourceCEM+contactResponse 时，只施加一次 (h_source*c_source)^-1 的读数等于 sourceCEM/(h_source*c_source)。转接到早先的匹配消费者时保持相同的值与方程；full-light 返回消费这一 owner。

    位置：§9.5✓ 内核检查已通过

    Lean 模块 · 1

  24. L25对同一组实际 edge0 电子，原完整 ordinary photon 响应在原 pole sheet 上、尺度充分小时为 N_D/(h_source*c_source(branch))*[beta_source(e)*D_D(polarization(e))-c_D(A_D(P_omega(e)J_source;lambda,T))]。§9.5

    对同一组实际 edge0 电子，原完整 ordinary photon 响应在原 pole sheet 上、尺度充分小时为 N_D/(h_source*c_source(branch))*[beta_source(e)*D_D(polarization(e))-c_D(A_D(P_omega(e)J_source;lambda,T))]。beta_source 是完整源电流上的实际 sourcePhotonLeftReader，不被除去。两端各自独立的复／实年龄窗及全部原参数都保留。

    位置：§9.5；§10.5✓ 内核检查已通过

    Lean 模块 · 1

  25. L24同一实际 charged edge0 静止腿 (side,1) 的 native 时间期望为 -1，字面 EM 本征值为 +1，所用的是原 actionScale*phaseMomentum=1。§10.1–10.4

    同一实际 charged edge0 静止腿 (side,1) 的 native 时间期望为 -1，字面 EM 本征值为 +1，所用的是原 actionScale*phaseMomentum=1。原一次 Coulomb 标量为 N_D[K*D_actual*W_cf-c_D(A_D(V_C))]。两端完整 64 权、完整静态读取器、有向 physicalTime／jointResolvent 年龄窗、coframe false／true 交换及每一项单腿／交叉腿修正均保留；源端单独归一化给出精确的双端修正公式。

    位置：§10.1–10.4；附录 F.3✓ 内核检查已通过

    Lean 模块 · 5

  26. L26原E=−color2−Y/2进入四原gauge slots，先保全部289输出／constraints再生成EᵀG_wholeE与EᵀR E。§11.1–11.3

    原E=−color2−Y/2进入四原gauge slots，先保全部289输出／constraints再生成EᵀG_wholeE与EᵀR E。真实原repaired density在nativeLocalPoint上的二阶变分恰为同K；原carrier解全289齐次方程，物理频率residue消费同作用K′并返回自身flux。任正clock scale，重表达的实际Green在移动pole生成R_clock=Rω/scale，实际Jacobi导数为scale·K′，完整flux归一恒等式保持；两边的原留数张量同缩为原值的1/scale，R K′投影不变。actual rest电流的pole factor与visibility由同source left reader返回；原E背景两非零color导数及全混合行保留。

    位置：§11.1–11.3；附录 G.1–G.2；图 4✓ 内核检查已通过

    Lean 模块 · 3

  27. L27同源全方向static operator-norm极限与原Schwartz/Newton可积价生成真实Bochner矩阵Fourier积分；actual双unit current保64权、全leg corrections与独立两窗，极限系数为K·W_DW_S/(h c)。§12.1–12.3

    同源全方向static operator-norm极限与原Schwartz/Newton可积价生成真实Bochner矩阵Fourier积分；actual双unit current保64权、全leg corrections与独立两窗，极限系数为K·W_DW_S/(h c)。profile／position／三维Jacobian共同伸缩给−1次，原Fourier仅一次4π。实际source-created unit减background的两connected currents再以相反转移进入同一个whole289积分，连续性自产共同IR半径与domination价；极限是原Newton convolution乘−dot(F0ᵀJ_D(0),staticInverse(F0ᵀJ_S(0)))，joint cross及return-return同在。

    位置：§12.1–12.3；附录 G.3–G.5；图 5✓ 内核检查已通过

    Lean 模块 · 3

  28. L28每个完整N3 fullY／独sharp腿自产非零response与唯一norm1；原bottom overlap=‖base‖/‖full response‖严格在(0,1]，其平方就是原(3,0)的unit Born值，sharp恰为1。§13.1–13.3

    每个完整N3 fullY／独sharp腿自产非零response与唯一norm1；原bottom overlap=‖base‖/‖full response‖严格在(0,1]，其平方就是原(3,0)的unit Born值，sharp恰为1。detector pair及source pair各至少一端为independent sharp时，四actual overlaps之积乘原normalized base coefficient精确等于complete Coulomb coefficient；差范数恰为(1−product)乘原base coefficient范数。它直接进入原whole289 Newton空间观测，没有外供Z或matching scale。

    位置：§13.1–13.3；附录 G.6；图 6✓ 内核检查已通过

    Lean 模块 · 3

亲手检验

在仓库根目录运行入口检查：

python3 tools/edition_release.py --edition low-energy verify-map

构建 Lean 证明与完整验收的步骤见复现指南