XORSystem — Recognition explainer

formal statement (Lean)

  15abbrev XORSystem (n : Nat) := List (XORConstraint n)

proof body

Definition body.

  16
  17/-- Compute the XOR (parity) of selected variables of assignment `a`. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

BackpropSucceeds in IndisputableMonolith.Complexity.SAT.Backprop decl_use
BPStep in IndisputableMonolith.Complexity.SAT.Backprop decl_use
bp_step_monotone in IndisputableMonolith.Complexity.SAT.Backprop decl_use
bp_step_sound in IndisputableMonolith.Complexity.SAT.Backprop decl_use
consistent in IndisputableMonolith.Complexity.SAT.Backprop decl_use
BackpropCompleteUnderInvariant in IndisputableMonolith.Complexity.SAT.Completeness decl_use
backprop_succeeds_from_PC in IndisputableMonolith.Complexity.SAT.Completeness decl_use
backprop_succeeds_of_unique in IndisputableMonolith.Complexity.SAT.Completeness decl_use
consistent_completeStateFrom in IndisputableMonolith.Complexity.SAT.Completeness decl_use
determined_values_correct in IndisputableMonolith.Complexity.SAT.Completeness decl_use
geometric_isolation_enables_propagation_hypothesis in IndisputableMonolith.Complexity.SAT.Completeness decl_use
geometric_isolation_enables_propagation_thm in IndisputableMonolith.Complexity.SAT.Completeness decl_use
IsolationInvariant in IndisputableMonolith.Complexity.SAT.Completeness decl_use
flatMap_length_bound' in IndisputableMonolith.Complexity.SAT.GeoFamily decl_use
geoFamily in IndisputableMonolith.Complexity.SAT.GeoFamily decl_use
mortonOctantFamily in IndisputableMonolith.Complexity.SAT.GeoFamily decl_use
octantsAtLevel in IndisputableMonolith.Complexity.SAT.GeoFamily decl_use
octantSystems in IndisputableMonolith.Complexity.SAT.GeoFamily decl_use
isolates in IndisputableMonolith.Complexity.SAT.Isolation decl_use
XORFamily in IndisputableMonolith.Complexity.SAT.Isolation decl_use
arborescence_implies_peeling in IndisputableMonolith.Complexity.SAT.PC decl_use
buildPeelingResult in IndisputableMonolith.Complexity.SAT.PC decl_use
constraintsOf in IndisputableMonolith.Complexity.SAT.PC decl_use
extractFromPC in IndisputableMonolith.Complexity.SAT.PC decl_use
ForcedArborescence in IndisputableMonolith.Complexity.SAT.PC decl_use
ForcedArborescenceWitness in IndisputableMonolith.Complexity.SAT.PC decl_use
PC in IndisputableMonolith.Complexity.SAT.PC decl_use
pc_implies_forcedArborescence in IndisputableMonolith.Complexity.SAT.PC decl_use
pc_implies_peeling in IndisputableMonolith.Complexity.SAT.PC decl_use
PeelingData in IndisputableMonolith.Complexity.SAT.PC decl_use

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
XORConstraint in IndisputableMonolith.Complexity.SAT.XOR decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
parity in IndisputableMonolith.LedgerPostingAdjacency decl_use