Acyclic Source-Formula Correctness

Abstract

Acyclic source formulas hold exactly when a source-supported proof exists.

Theorem 1.1 (Source formulas are correct for valid proofs).

$$\begin{array}{r}\forall S:\mathrm{Type},[\mathrm{DecidableEq}(S)],n:\mathbb{N},\\ G:\mathrm{SourceProofGraph}(S,n),A:\mathrm{Finset}(S),c:\mathrm{Fin}(n),\\ \mathrm{sourceFormulaHolds}(G,A,c)⟺\mathrm{ValidSourceProof}(G,A,c).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Provenance/AcyclicSourceFormulaCorrectness.source_formula_iff_valid_source_proof (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source proof graph extends the existing finite acyclic rank carrier. Each conclusion has an optional direct source and finitely many alternative rules whose premises carry incoming-edge certificates.

The Boolean semantics is constructed recursively along the inherited rank. A direct enabled source is one disjunct; each alternative rule is another disjunct whose premises form a conjunction.

ValidSourceProof is an independent inductive relation. Well-founded induction proves that the recursive formula holds exactly when a proof uses only the available sources.

References

• Truth anchor: D5/S3/ConceptDynamics/Provenance/AcyclicSourceFormulaCorrectness.source_formula_iff_valid_source_proof
• Dependency: D5/S3/ConceptDynamics/Provenance/FiniteProofGraphSourceSemantics