Struct OrbitRecord 

pub struct OrbitRecord {

    pub n: usize,
    pub rep: Cover,
    pub num_clauses: usize,
    pub orbit_size: usize,
    pub stabilizer_order: usize,
    pub face_vector: BTreeMap<usize, usize>,
    pub min_res_width: usize,
    pub rung: ProofRung,
    pub shadow: Option<Shadow>,
    pub route: Route,
    pub discovered_rule_orbits: usize,
    pub full_rule_orbits: usize,
    pub affine_explained: bool,
    pub modp_routed: bool,
}

One Bₙ-orbit of minimal UNSAT formulas over n variables, with every invariant the solver can compute about it. The raw measurements; the audit flags (OrbitRecord::router_beats_ladder, OrbitRecord::finder_is_incomplete) are derived from them.

Fields

n: usize

rep: Cover

A canonical representative cover of the orbit.

num_clauses: usize

orbit_size: usize

Number of distinct covers in the Bₙ orbit.

stabilizer_order: usize

|Stab| = |Bₙ| / orbit_size — how symmetric this formula is.

face_vector: BTreeMap<usize, usize>

Blockers per face dimension — a geometric invariant of the cover.

min_res_width: usize

Minimum width of any resolution refutation.

rung: ProofRung

The weakest certified cut on the proof-complexity ladder (GF(2) Nullstellensatz at the top).

shadow: Option<Shadow>

The single-label certified shadow the diagnoser reads off (Counting/Parity/CuttingPlanes).

route: Route

Which engine the full structured router actually decides it with.

discovered_rule_orbits: usize

Self-driving rule-symmetry: how many essentially-distinct clauses the discovered automorphisms leave (the production symmetry breaker, symmetry_detect::find_generators, used in the cascade).

full_rule_orbits: usize

The same count under the cover’s full Bₙ stabilizer (every geometric automorphism, computed exhaustively from the group). This is the strongest symmetry break achievable. When discovered_rule_orbits > full_rule_orbits, the production breaker is leaving symmetry unbroken — a case the solver could collapse further but currently does not.

affine_explained: bool

Is the UNSAT explained by an inconsistent GF(2) linear system (the parity shadow)?

modp_routed: bool

Did the structured router crush it with the polynomial mod-p (GF(p)) engine?

Implementations

impl OrbitRecord

pub fn router_beats_ladder(&self) -> bool

Gap signal. The full router crushed this cover with a polynomial specialist the certified proof-complexity ladder has no rung for — the router sees structure the certified cascade can only reach by an expensive general proof. The clearest case: a mod-p germ routed to ModP while the ladder reports a (GF(2)) Nullstellensatz height. This is the unification gap, per orbit.

pub fn symmetry_underbroken(&self) -> bool

Symmetry left on the table. The production breaker discovered strictly fewer rule-merges than the cover’s full geometric stabilizer admits — so the symmetry-breaking predicate it injects is weaker than achievable, and a scaled-up member of this family will cost the solver search it could have avoided. Every such orbit is a concrete “break more symmetry → solve more cases” target.

Trait Implementations

impl Clone for OrbitRecord

fn clone(&self) -> OrbitRecord

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for OrbitRecord

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.