abbrev definition def or abbrev

`ForcedArborescenceWitness`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 111abbrev ForcedArborescenceWitness {n}
 112  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=

proof body

Definition body.

 113  PeelingWitness inputs aRef φ H
 114
 115/-- Program goal (graph-theoretic equivalence to target):
 116    PC ↔ existence of a forced-implication arborescence (to be proven). -/

depends on (14)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Assignment in IndisputableMonolith.Complexity.RSatEncoding decl_use
Assignment in IndisputableMonolith.Complexity.SAT.CNF decl_use
CNF in IndisputableMonolith.Complexity.SAT.CNF decl_use
InputSet in IndisputableMonolith.Complexity.SAT.PC decl_use
PC in IndisputableMonolith.Complexity.SAT.PC decl_use
PeelingWitness in IndisputableMonolith.Complexity.SAT.PC decl_use
XORSystem in IndisputableMonolith.Complexity.SAT.XOR decl_use
H in IndisputableMonolith.Cost.FunctionalEquation 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