Struct TimeLoweringProof
pub struct TimeLoweringProof { /* private fields */ }Description
Backend-neutral witness for canonical Relation → first-order lowering.
The witness records facts proven from Operator IR, not solver output. Its constructor derives the admitted equation class. A full monomial Jacobian normalizes to an explicit ODE; every other non-zero-rank constant matrix remains a full or rank-deficient mass matrix.
Implementations§
§impl TimeLoweringProof
impl TimeLoweringProof
pub fn new(
relation: Id<Relation>,
state_fields: Vec<Id<Field>>,
derivative_matrix: ConstantDerivativeMatrixProof,
) -> Result<TimeLoweringProof, Diagnostic>
pub fn new( relation: Id<Relation>, state_fields: Vec<Id<Field>>, derivative_matrix: ConstantDerivativeMatrixProof, ) -> Result<TimeLoweringProof, Diagnostic>
Construct and validate one exact constant-derivative-matrix witness.
§Errors
Returns EQ0705 for empty/repeated state Fields, a dimension mismatch,
or a system with an identically zero derivative matrix.
pub const fn relation(&self) -> Id<Relation>
pub const fn relation(&self) -> Id<Relation>
Canonical Relation whose derivative structure was proven.
pub fn state_fields(&self) -> &[Id<Field>]
pub fn state_fields(&self) -> &[Id<Field>]
Deterministic state coordinate order.
pub const fn derivative_matrix(&self) -> &ConstantDerivativeMatrixProof
pub const fn derivative_matrix(&self) -> &ConstantDerivativeMatrixProof
Residual-ordered constant derivative matrix witness.
pub const fn equation_class(&self) -> TimeEquationClass
pub const fn equation_class(&self) -> TimeEquationClass
Equation class derived from this witness.
pub const fn initial_condition_policy(&self) -> InitialConditionPolicy
pub const fn initial_condition_policy(&self) -> InitialConditionPolicy
Initial-condition policy implied by this witness.
Trait Implementations§
§impl Clone for TimeLoweringProof
impl Clone for TimeLoweringProof
§impl Debug for TimeLoweringProof
impl Debug for TimeLoweringProof
§impl PartialEq for TimeLoweringProof
impl PartialEq for TimeLoweringProof
§fn eq(&self, other: &TimeLoweringProof) -> bool
fn eq(&self, other: &TimeLoweringProof) -> bool
self and other values to be equal, and is used by ==.impl StructuralPartialEq for TimeLoweringProof
Auto Trait Implementations§
impl Freeze for TimeLoweringProof
impl RefUnwindSafe for TimeLoweringProof
impl Send for TimeLoweringProof
impl Sync for TimeLoweringProof
impl Unpin for TimeLoweringProof
impl UnsafeUnpin for TimeLoweringProof
impl UnwindSafe for TimeLoweringProof
Blanket Implementations§
Source§impl<T> Any for Twhere
T: 'static + ?Sized,
impl<T> Any for Twhere
T: 'static + ?Sized,
§impl<Src, Scheme> ApproxFrom<Src, Scheme> for Srcwhere
Scheme: ApproxScheme,
impl<Src, Scheme> ApproxFrom<Src, Scheme> for Srcwhere
Scheme: ApproxScheme,
§fn approx_from(src: Src) -> Result<Src, <Src as ApproxFrom<Src, Scheme>>::Err>
fn approx_from(src: Src) -> Result<Src, <Src as ApproxFrom<Src, Scheme>>::Err>
§impl<Dst, Src, Scheme> ApproxInto<Dst, Scheme> for Srcwhere
Dst: ApproxFrom<Src, Scheme>,
Scheme: ApproxScheme,
impl<Dst, Src, Scheme> ApproxInto<Dst, Scheme> for Srcwhere
Dst: ApproxFrom<Src, Scheme>,
Scheme: ApproxScheme,
§type Err = <Dst as ApproxFrom<Src, Scheme>>::Err
type Err = <Dst as ApproxFrom<Src, Scheme>>::Err
§fn approx_into(self) -> Result<Dst, <Src as ApproxInto<Dst, Scheme>>::Err>
fn approx_into(self) -> Result<Dst, <Src as ApproxInto<Dst, Scheme>>::Err>
Source§impl<T> Borrow<T> for Twhere
T: ?Sized,
impl<T> Borrow<T> for Twhere
T: ?Sized,
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
§impl<T, Dst> ConvAsUtil<Dst> for T
impl<T, Dst> ConvAsUtil<Dst> for T
§fn approx(self) -> Result<Dst, Self::Err>where
Self: Sized + ApproxInto<Dst>,
fn approx(self) -> Result<Dst, Self::Err>where
Self: Sized + ApproxInto<Dst>,
§impl<T> ConvUtil for T
impl<T> ConvUtil for T
§fn approx_as<Dst>(self) -> Result<Dst, Self::Err>where
Self: Sized + ApproxInto<Dst>,
fn approx_as<Dst>(self) -> Result<Dst, Self::Err>where
Self: Sized + ApproxInto<Dst>,
§fn approx_as_by<Dst, Scheme>(self) -> Result<Dst, Self::Err>where
Self: Sized + ApproxInto<Dst, Scheme>,
Scheme: ApproxScheme,
fn approx_as_by<Dst, Scheme>(self) -> Result<Dst, Self::Err>where
Self: Sized + ApproxInto<Dst, Scheme>,
Scheme: ApproxScheme,
§fn into_as<Dst>(self) -> Dstwhere
Self: Sized + Into<Dst>,
fn into_as<Dst>(self) -> Dstwhere
Self: Sized + Into<Dst>,
§fn try_as<Dst>(self) -> Result<Dst, Self::Err>where
Self: Sized + TryInto<Dst>,
fn try_as<Dst>(self) -> Result<Dst, Self::Err>where
Self: Sized + TryInto<Dst>,
§impl<T> DistributionExt for Twhere
T: ?Sized,
impl<T> DistributionExt for Twhere
T: ?Sized,
fn rand<T>(&self, rng: &mut (impl Rng + ?Sized)) -> Twhere
Self: Distribution<T>,
Source§impl<T> From<T> for T
impl<T> From<T> for T
Source§impl<T, U> Into<U> for Twhere
U: From<T>,
impl<T, U> Into<U> for Twhere
U: From<T>,
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>where
F: FnOnce(&Self) -> bool,
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>where
F: FnOnce(&Self) -> bool,
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more§impl<T> Pointable for T
impl<T> Pointable for T
Source§impl<T> Same for T
impl<T> Same for T
§impl<SS, SP> SupersetOf<SS> for SPwhere
SS: SubsetOf<SP>,
impl<SS, SP> SupersetOf<SS> for SPwhere
SS: SubsetOf<SP>,
§fn to_subset(&self) -> Option<SS>
fn to_subset(&self) -> Option<SS>
self from the equivalent element of its
superset. Read more§fn is_in_subset(&self) -> bool
fn is_in_subset(&self) -> bool
self is actually part of its subset T (and can be converted to it).§fn to_subset_unchecked(&self) -> SS
fn to_subset_unchecked(&self) -> SS
self.to_subset but without any property checks. Always succeeds.§fn from_subset(element: &SS) -> SP
fn from_subset(element: &SS) -> SP
self to the equivalent element of its superset.