Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Sparse laws on the original causal response carrier

Abstract

A law-specific Caratheodory witness can be pushed back to the unchanged causal response carrier. The resulting sparse original-carrier law satisfies the same finite linear constraints and attains exactly the same linear query value.

Theorem 1.1 (Deterministic pushforward preserves pulled-back expectations).

Lean statement: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.pushforward_linearObjective

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.pushforward_linearObjective (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every rational coefficient on the response carrier, expectation under deterministic pushforward equals expectation of the pulled-back coefficient on the source carrier.

Theorem 1.2 (Rank-controlled attaining law on the original carrier).

Lean statement: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.finite_linear_problem_sparse_original_witness

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.finite_linear_problem_sparse_original_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every feasible query point has a feasible sparse law on the original response carrier generated by at most one plus the affine rank of the joint constraint-row and query profile.

Theorem 1.3 (Coarse row-count support bound).

Lean statement: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.finite_linear_problem_sparse_original_witness_card_le

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.finite_linear_problem_sparse_original_witness_card_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

Ignoring affine redundancy gives the universal coarser bound of the number of LP rows plus two selected latent atoms.

References

  • Truth anchor: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.finite_linear_problem_sparse_original_witness
  • Truth anchor: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.finite_linear_problem_sparse_original_witness_card_le
  • Truth anchor: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSparseLaw.pushforward_linearObjective
  • Dependency: D5/S3/ConceptDynamics/CausalMoments/FiniteMomentSupportReduction