src/kernel/Anytype/Grade/ has Affine.idr + Exact.idr. The README's discipline table also names cost accounting, information flow, and composite (product) grades. systemet PR #17 now carries proven Lean statements to port: tropical Cost (min/+), the generic bounded-distributive-lattice⇒grade-algebra theorem instantiated at Level (Low≤High), and the componentwise product R × S (verification/proofs/lean4/Systemet/L2/Instances/). Cites: ET-5 (with ET-4 as the law set already discharged in Grade/Algebra.idr).
🤖 Generated with Claude Code
src/kernel/Anytype/Grade/hasAffine.idr+Exact.idr. The README's discipline table also names cost accounting, information flow, and composite (product) grades. systemet PR #17 now carries proven Lean statements to port: tropicalCost(min/+), the generic bounded-distributive-lattice⇒grade-algebra theorem instantiated atLevel(Low≤High), and the componentwise productR × S(verification/proofs/lean4/Systemet/L2/Instances/). Cites: ET-5 (with ET-4 as the law set already discharged inGrade/Algebra.idr).🤖 Generated with Claude Code