Inter-Layer V&V Propagation (F5 generalized)

Layer.supports (inclusion relation between layers) と LayerPropagation (transitive propagation from lower-layer V&V to upper-layer V&V) を定義する。

F5 での一般化

旧版は 3 階層 (.component / .subsystem / .system) の pattern match で supports を定義していたため、新しい階層（.assembly, .unit, .part 等）を 追加するたびにケースを増やす必要があった。

F5 で Layer が depth を持つようになったため、supports を

Layer.supports l1 l2 ⟺ l1.depth > l2.depth

という depth 比較ベースに一般化した。これにより 8 階層すべてに対して supports / supports_trans / supports_irrefl が 同一の証明で成立 する。

後方互換: 旧コードが期待する supports .component .system などの判定結果は そのまま成立する（.component.depth = 6 > 1 = .system.depth）。

def VerifiedMBSE.VV.Layer.supports (l1 l2 : Layer) : Prop

Layer inclusion: a lower layer 'supports' an upper layer.

depth ベースで判定: l1 の depth が l2 より大きければ l1 は下層 （分解が進んだ側）であり、上層 l2 の V&V を支える。

Equations

• l1.supports l2 = (l1.depth > l2.depth)

@[implicit_reducible]

instance VerifiedMBSE.VV.instDecidableSupports (l1 l2 : Layer) : Decidable (l1.supports l2)

supports は Nat.lt 経由で決定可能 (Bool 化できる)。

Equations

• VerifiedMBSE.VV.instDecidableSupports l1 l2 = l2.depth.decLt l1.depth

theorem VerifiedMBSE.VV.Layer.supports_trans {l1 l2 l3 : Layer} (h12 : l1.supports l2) (h23 : l2.supports l3) : l1.supports l3

supports は推移的 (Nat.lt の推移性から直接導出)。

theorem VerifiedMBSE.VV.Layer.supports_irrefl (l : Layer) : ¬l.supports l

supports は反反射的 (Nat.lt の反反射性から直接導出)。

structure VerifiedMBSE.VV.LayerPropagation : Type

LayerPropagation: relation where lower-layer V&V implies upper-layer V&V.

• lower_layer : Layer
• upper_layer : Layer
• supports : self.lower_layer.supports self.upper_layer
• lower_prop : Prop
• upper_prop : Prop
• propagates : self.lower_prop → self.upper_prop

def VerifiedMBSE.VV.LayerPropagation.compose (lp1 lp2 : LayerPropagation) (hchain : lp1.upper_prop → lp2.lower_prop) (hsup : lp1.lower_layer.supports lp2.upper_layer) : LayerPropagation

Composition of transitive propagation.

Equations

• lp1.compose lp2 hchain hsup = { lower_layer := lp1.lower_layer, upper_layer := lp2.upper_layer, supports := hsup, lower_prop := lp1.lower_prop, upper_prop := lp2.upper_prop, propagates := ⋯ }

theorem VerifiedMBSE.VV.trusted_gives_full_confidence (r : VVRecord) (h : r.validation.current = ValidationEvidence.trusted ⋯) : r.validation.currentLevel = 1.0

If all VVRecord validations are trusted, then currentLevel = 1.0.