other

Field.Quantilization final nodes quantile_soundness_preserves_trajectory_cci quantile_separated_from_trajectory

Lean spine source

formal/AlignmentProofSpine/Field/Quantilization.lean

Declarations: quantile_soundness_preserves_trajectory_cci, quantile_separated_from_trajectory

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

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

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