Core

The heart of the framework: the laws behind the Causal Monad, the Causaloid, the Context hypergraph, Causal Flow, and the Effect Propagation Process. Proved in lean/DeepCausalityFormal/Core/.

This is the one layer with a Kani column: several laws are checked twice on the Rust side, by a law-test and a bounded model check. A n/a in that column means the law is witnessed by its law-test alone.

Witnesses live in two crates. deep_causality_core/tests/ carries the monad, arrow, effect-log, effect, command, consistency, alternatable, flow, and CSV laws; deep_causality/tests/ carries the causaloid-fixpoint, verdict, graph-fold, catamorphism, and context-graph laws, where the engine itself is the witness. Kani harnesses are in deep_causality_core/tests/kani_proofs.rs. Statements are condensed here; the full annotations are in THEOREM_MAP.md.

id	statement	Lean proof	Rust witness	Test	Kani
core.causal_monad.left_id	pure a >>= f = f a	CausalMonad.lean :: bind_left_id	kani_proofs.rs :: causal_monad_left_identity	n/a	✓
core.causal_monad.right_id	m >>= pure = m (unconditional; holds on errored carriers)	CausalMonad.lean :: bind_right_id	causal_monad_tests.rs :: test_right_identity_unconditional	✓	✓
core.causal_monad.assoc	(m >>= f) >>= g = m >>= (λx. f x >>= g)	CausalMonad.lean :: bind_assoc	causal_monad_tests.rs :: test_associativity_across_erroring_continuation	✓	✓
core.causal_monad.left_zero	raise e >>= f = raise e (error short-circuit)	CausalMonad.lean :: bind_raise_left_zero	kani_proofs.rs :: causal_monad_short_circuit	n/a	✓
core.causal_monad.lawful	LawfulMonad-with-effect: left/right identity + associativity co-hold on one carrier	CausalMonad.lean :: causal_monad_lawful	causal_monad_tests.rs :: test_causal_monad_lawful	✓	n/a
core.causal_arrow.category_laws	Kleisli category laws threading state/context over arbitrary S, C	CausalArrow.lean :: kcomp_left_id / kcomp_right_id / kcomp_assoc	causal_arrow_tests.rs :: arrow_threads_accumulated_state	✓	✓
core.causal_arrow.left_zero	errored stage short-circuits composition; state preserved, downstream not run	CausalArrow.lean :: kcomp_left_zero	causal_arrow_tests.rs :: arrow_error_short_circuit_preserves_state	✓	n/a
core.effect_log.left_id	append empty x = x (free monoid / Writer output)	EffectLog.lean :: append_left_id	effect_log_tests.rs :: test_effect_log_left_identity	✓	n/a
core.effect_log.right_id	append x empty = x	EffectLog.lean :: append_right_id	effect_log_tests.rs :: test_effect_log_right_identity	✓	n/a
core.effect_log.assoc	append (append x y) z = append x (append y z)	EffectLog.lean :: append_assoc	effect_log_tests.rs :: test_effect_log_associativity	✓	n/a
core.effect_log.monotone	incoming log is a prefix of the combined log (append-only)	EffectLog.lean :: append_monotone	effect_log_tests.rs :: test_effect_log_monotone_prefix	✓	n/a
core.causal_effect.into_value	into_value is the honest Maybe projection; value functor = Option	CausalEffect.lean :: into_value_value / into_value_none / into_value_command	causal_effect_tests.rs :: test_causal_effect_into_value	✓	n/a
core.causal_effect.transformer_stack	Except E (Free CausalCommand (Maybe V)) is a lawful monad: identity, associativity, Err global zero, None local zero, relay threading with error hoisting	CausalEffect.lean :: obind_left_id / obind_right_id / obind_assoc / obind_err_zero / obind_none_zero	causal_effect_tests.rs :: test_transformer_stack_monad_laws	✓	n/a
core.causal_effect.fold_universal	CausalEffect::fold satisfies the two handler equations and is the UNIQUE such interpreter (initiality of the free monad)	CausalEffect.lean :: fold_pure / fold_relay / fold_unique	causal_effect_tests.rs :: test_fold_universal	✓	n/a
core.causal_effect.relay_termination	the fuel-bounded relay handler is total: a value answers, answers are fuel-monotone, a self-relay cycle exhausts instead of looping (bound MAX_RELAY_ROUNDS)	CausalEffect.lean :: run_pure / run_fuel_monotone / run_self_relay_none	causal_effect_tests.rs :: test_relay_termination_fuel_bound	✓	n/a
core.causal_effect.relay_round_composition	multi-round adaptive evaluation is the sequential (Kleisli) composition of its rounds; the fuel-bounded run splits at any round boundary	CausalEffect.lean :: rounds_add / run_rounds_compose / run_monotone_add / run_relay_peel	relay_round_composition_tests.rs :: test_relay_round_composition	✓	n/a
core.causaloid.fixpoint	Causaloid ≅ μX.F(X) with F(X) = Atom + Coll(Bag X, AggLogic) + Graph(Hyper X, Λ-edges): the roll/unroll Lambek isomorphism, well-founded (μ, not ν)	Causaloid.lean :: roll_unroll / unroll_roll / size_pos	causaloid_tests.rs :: test_fixpoint_three_forms_and_roll_unroll	✓	n/a
core.causaloid.inversion	the Hardy inversion, formal: eval = wiring ∘ element-map, the element map is pointwise and bag-symmetric (mapL_perm); Λ-edges are identity-keyed	Causaloid.lean :: eval_factors / mapL_perm	causaloid_tests.rs :: test_inversion_element_is_symmetric	✓	n/a
core.verdict.closure	All/Any/None/Some(k) are closed operations in the Verdict algebra ⇒ Coll : Causaloid → Causaloid	VerdictClosure.lean :: closure_fold_step / none_is_any_complement / someK_decides / coll_closure	verdict_closure_tests.rs :: test_verdict_closure_aggregation_modes	✓	n/a
core.verdict.carriers	the named carriers behind the one trait: bool Boolean (distributive) and Prob/f64 MV on [0,1] (min/max/1−p, excluded middle fails)	VerdictClosure.lean :: bool_carrier_characterization / bool_distributive	verdict_closure_tests.rs :: test_verdict_carriers	✓	n/a
core.verdict.perm_invariance	collection aggregation is a BAG operation: for every AggregateLogic mode the aggregate value is invariant under permutation of the member bag, lifted to the Coll node	VerdictClosure.lean :: aggregate_perm / coll_perm	verdict_closure_tests.rs :: test_verdict_perm_invariance	✓	n/a
core.causaloid.graph_fold_order_invariant	the topological fold with ∇ ∘ (Λ₁ ⊗ Λ₂) at reconvergent joins is invariant under every schedule consistent with the causal order	GraphAlgebra.lean :: fuse_perm / exec_computes_val / schedule_invariant	graph_algebra_tests.rs :: test_graph_fold_order_invariant	✓	n/a
core.causaloid.catamorphism_unique	initiality of the fixpoint, per fixed carrier: any interpreter satisfying the three case equations of (V, elemSem, ∇) is pointwise equal to eval	Catamorphism.lean :: catamorphism_unique / catamorphism_unique_list	catamorphism_tests.rs :: test_catamorphism_unique	✓	n/a
core.causaloid.encapsulation_flat	nested fold = flat fold (catamorphism fusion): wrapping a subgraph in a causaloid does not change the semantics	Catamorphism.lean :: encapsulation_flat / evalL_append	catamorphism_tests.rs :: test_encapsulation_flat	✓	n/a
core.causaloid.arrow_fragment	the Atom/compose fragment ≅ the reified ArrowTerm language; the interpretation factors through T/≈ (category laws)	Catamorphism.lean :: arrow_fragment / interp_respects_category_laws	catamorphism_tests.rs :: test_arrow_fragment	✓	n/a
core.causaloid.command_input	a command (RelayTo) on a singleton’s INPUT channel yields a specific, named error, never a silent None and never a dropped signal; the dispatch is total	CommandInput.lean :: command_yields_cmd_err / command_never_ok / command_err_distinct_from_absent	command_input_tests.rs :: test_command_input_yields_command_error	✓	n/a
core.context_graph.threading_bind	hyperedge threading of a node’s parents IS the causal monad bind; nested threading = flat; encapsulation = flat is bind associativity	ContextGraph.lean :: thread_is_bind / thread_append / evalParents_split / encapsulation_flat	context_graph_tests.rs :: test_context_parent_set_keyed_by_identity	✓	n/a
core.context_graph.acyclicity_separable	acyclicity is a separable, freeze-enforceable parameter: a self-parent has no rank certificate and is rejected at freeze; the threading apparatus never consults it	ContextGraph.lean :: Acyclic / self_parent_not_acyclic / acyclic_iff_rank / apparatus_acyclicity_agnostic	context_graph_tests.rs :: test_context_acyclicity_freeze_gate	✓	n/a
core.causal_command.functor_laws	single-hole CausalCommand functor laws (fmap id = id, fmap (g∘f) = fmap g ∘ fmap f)	CausalCommand.lean :: cmap_id / cmap_comp	causal_command_tests.rs :: test_causal_command_functor_laws	✓	n/a
core.witness.agree	every law-bearing HKT surface computes the SAME total success-channel functor/applicative; command preserved not collapsed, no panic	Consistency.lean :: witness_agree / fmap_preserves_command / apply_none_yields_none / apply_command_yields_none	consistency_tests.rs :: test_witness_agrees_with_inherent_fmap	✓	n/a
core.alternatable.set_get	lens set-get on the log-erasing projection (value/state/context)	Alternatable.lean :: set_get_value / set_get_state / set_get_context	alternatable_tests.rs :: test_alternatable_set_get	✓	n/a
core.alternatable.set_set_proj	lens set-set idempotence up-to-log (proj); the full carrier grows the log	Alternatable.lean :: set_set_value_proj / set_set_state_proj / set_set_context_proj / set_set_grows_log	alternatable_tests.rs :: test_alternatable_set_set_up_to_log	✓	n/a
core.alternatable.channel_independence	each setter touches only its own channel	Alternatable.lean :: value_preserves_state_ctx / state_preserves_value_ctx / context_preserves_value_state	alternatable_tests.rs :: test_alternatable_channel_independence	✓	n/a
core.alternatable.error_noop	every setter (and clear_context) is a no-op on an errored carrier	Alternatable.lean :: value_error_noop / state_error_noop / context_error_noop / clear_context_error_noop	alternatable_tests.rs :: test_alternatable_error_noop	✓	n/a
core.causal_flow.flow_iso	CausalFlow ≅ Process (newtype wrap/unwrap, rfl)	CausalFlow.lean :: flow_iso	causal_flow_tests.rs :: test_causal_flow_iso	✓	n/a
core.causal_flow.map_id	map id = id (facade functor identity)	CausalFlow.lean :: map_id	causal_flow_tests.rs :: test_causal_flow_map_id	✓	n/a
core.causal_flow.map_comp	map (g∘f) = map g ∘ map f	CausalFlow.lean :: map_comp	causal_flow_tests.rs :: test_causal_flow_map_comp	✓	n/a
core.causal_flow.map_eq_andThen	map f = and_then (pure∘f), which holds on the None effect as well as a value	CausalFlow.lean :: map_eq_andThen	causal_flow_tests.rs :: test_causal_flow_map_eq_and_then	✓	n/a
core.causal_flow.recover	MonadError.catch: no-op on success, raise ↦ handler value	CausalFlow.lean :: recover_catch	causal_flow_tests.rs :: test_causal_flow_recover	✓	n/a
core.causal_flow.iterate	bounded search terminates; budget exhaustion injects MaxStepsExceeded, state/context/log preserved	CausalFlow.lean :: iterate_contract	causal_flow_tests.rs :: test_causal_flow_iterate	✓	n/a
core.causal_flow.finish	terminal value-observation drops state/context/log	CausalFlow.lean :: finish_drops_state_ctx_log	causal_flow_tests.rs :: test_causal_flow_finish	✓	n/a
core.io.csv_roundtrip	parse (render header rows) = header :: rows under the no-',' / no-'\n' precondition	Csv.lean :: csv_roundtrip	csv_tests.rs :: test_csv_roundtrip	✓	n/a