proof: generate Lean-to-Zig finite-matrix differential fixtures

[SMC17]

Objective

Turn the initial Lean finite-matrix oracle into a machine-checked cross-language conformance gate rather than two implementations that merely look similar.

Scope

• K3, LP, FDE, and Ł3 truth tables and designated values.
• Canonical validity and countervaluation claims in src/logic/manyvalued.zig.
• Generated, deterministic fixture format consumed by Zig tests.
• Lean theorem statements remain stable during automated proof generation.

Acceptance gates

• Lean exports or checks every operation table used by Zig.
• A deterministic tool produces a checked fixture with provenance and schema version.
• Zig replays every fixture and rejects at least one mutated table/value/designation fixture.
• lake build passes under the pinned toolchain.
• CI nanoda check passes with sorryAx forbidden.
• zig build test and TRUST_OK pass.
• Documentation distinguishes kernel proof from Lean-to-Zig translation assurance.

Aristotle boundary

Aristotle may propose proofs and general lemmas. Raw generated output is not accepted until statement diff review, kernel compilation, independent checking, and Zig differential replay all pass.