Machine-checked evidence：第70轮 `fix_c_eq_decided` · 第72轮 `isClosure_leastAbove` ＋三实例 · 第73轮 偏序↔范畴字典（EM 代数 ⇔ 不动点）· 第61轮 `FixV_eq_range`：不动点＝右伴随的像（显式描述）
`Fix(c)` is the boundary; and three apparently different closure operators are three instances of the same construction (the `leastAbove` map) — the poset case and the category case have a correspondence dictionary.
Machine-checked evidence：第62轮 `V_global_min` / `V_gt_near_zero` / `V_gt_atTop` · 专题「靶心3」`value_layer_form_forced` · P4 达成：值层代数核 Lean 编译通过
The entropy term is a theorem: `H(κ) = C_F/κ`, monotone decreasing in κ (weight-(−1) equivariance of the rescaling law). κ★ is the unique global minimum of V, with ε–δ limits at both ends. `value_layer_form_forced` is machine-checked.
Machine-checked evidence：第63轮 `pU_le_b` / `b_sub_pU_eq_two_min` / `b_eq_pU_iff` / `core_b_eq`（Lean exit 0）
The three-component field has been separated: `p_U ≤ b`, and `b − p_U = 2·min(p_S, p_N)`; `b = p_U` iff p_S or p_N is zero. b is a balance measure, not an uncertainty measure.
Machine-checked evidence：第77轮 `anchoring_fixes_one_degree` · 第78轮 `fix_rescale_image` / `anchoring_freedom_done_both_sides`
The value-layer scaling structure is machine-checked: anchoring fixes exactly one overall scale, one degree of freedom; the closure-side equivariance has also been supplied — `anchoring_freedom_done_both_sides`.
Machine-checked evidence：第107轮 `R_fixed_exists` / `R_fixed_unique` / `R_indep_of_F` · 第109轮 `n1_n2_n3_certificate` · 第111轮 `unitRead_scale_center_invariant` / `unitRead_agrees_reciprocal` / `unitRead_unique`
Reading one's own kernel in one's own unit scale gives `2/(1+e)`: independent of the scale center, equal to the reciprocal route's value, unique. Existence, uniqueness and independence of F for R(w)=1/w are all machine-checked; the N1/N2/N3 certificates are packaged.
Machine-checked evidence：第116轮 `gaugeInvPrinciple_notSelects` / `selfConsistency_selects` · 第120轮 `no_gaugeInv_identification`（主结果）· 第114轮 `unitRead_gaugeInv_level_blind`
This is one of this line's own main theorems, and it is negative: no gauge-invariant selection principle can pick a level; anything that can pick one must break gauge invariance. The four T-θ‴ items are concluded, two of them negative theorems.
Machine-checked evidence：第86轮 `witness_iff_b_crosses` / `protocol_core` · 第119轮 `level_geometric` ＋ `falsifier_overshoot` / `falsifier_nonmonotone` / `falsifier_stalls`
The S4 failure condition has been formalized: an exponential-approach prediction plus three named refutations — overshoot / fall-back / stall. The criterion is lowered from "a statement about an operator" to "a statement about a measurable scalar": witness ⇔ there exists a b-crossing state.