other

Quantilization quantile_soundness_preserves_trajectory_cci quantile_separated_from_trajectory

Lean spine source

Declarations: quantile_separated_from_trajectory, quantile_soundness_preserves_trajectory_cci

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem quantile_separated_from_trajectory :
    QuantileSafeLocalAction quantileSeparationStep ∧
      ¬ TrajectoryCCIPreserved quantileSeparationStep 3 :=
  quantile_separated_from_trajectory_cci

theorem quantile_soundness_preserves_trajectory_cci
    (theta : Int)
    (x : FieldFinite.WeightedSample TrajectoryCorrectionStep)
    (hsound :
      FieldFinite.QuantileEligibilitySound theta
        (fun s => TrajectoryCCIPreserved s theta) x)
    (hsafe : FieldFinite.quantileSafeLocal theta x) :
    TrajectoryCCIPreserved x.point theta :=
  FieldFinite.quantile_safe_transfers_soundness
    theta (fun s => TrajectoryCCIPreserved s theta) x hsound hsafe